Pairwise relations on a list

This file provides basic results about List.Pairwise and List.pwFilter (definitions are in Data.List.Defs). Pairwise R [a 0, ..., a (n - 1)] means ∀ i j, i < j → R (a i) (a j). For example, Pairwise (≠) l means that all elements of l are distinct, and Pairwise (<) l means that l is strictly increasing. pwFilter R l is the list obtained by iteratively adding each element of l that doesn't break the pairwise property of the list we have so far. It thus yields l' as a maximal sublist of l such that Pairwise R l'.

Tags

sorted, nodup

theorem List.pairwise_iff {α : Type u} (R : α → α → Prop) (a✝ : List α) : Pairwise R a✝ ↔ a✝ = [] ∨ ∃ (a : α), ∃ (l : List α), (∀ (a' : α), a' ∈ l → R a a') ∧ Pairwise R l ∧ a✝ = a :: l

Pairwise

theorem List.pairwise_iff_forall_infix {α : Type u_2} {l : List α} {R : α → α → Prop} : Pairwise R l ↔ ∀ (l' : List α) (h : 1 < l'.length), l' <:+: l → R (l'.head ⋯) (l'.getLast ⋯)

theorem List.Pairwise.forall_of_forall {α : Type u_1} {R : α → α → Prop} {l : List α} [Std.Symm R] (H₁ : ∀ (x : α), x ∈ l → R x x) (H₂ : Pairwise R l) ⦃x : α⦄ : x ∈ l → ∀ ⦃y : α⦄, y ∈ l → R x y

theorem List.Pairwise.forall {α : Type u_1} {R : α → α → Prop} {l : List α} [Std.Symm R] (hl : Pairwise R l) ⦃a : α⦄ : a ∈ l → ∀ ⦃b : α⦄, b ∈ l → a ≠ b → R a b

theorem List.Pairwise.set_pairwise {α : Type u_1} {R : α → α → Prop} {l : List α} (hl : Pairwise R l) [Std.Symm R] : {x : α | x ∈ l}.Pairwise R

theorem List.pairwise_of_reflexive_of_forall_ne {α : Type u_1} {R : α → α → Prop} {l : List α} [Std.Refl R] (h : ∀ (a : α), a ∈ l → ∀ (b : α), b ∈ l → a ≠ b → R a b) : Pairwise R l

theorem List.pairwise_append_of_mem {α : Type u_1} {R : α → α → Prop} {l₁ l₂ : List α} {a b : α} [Std.Symm R] [IsTrans α R] (ha : a ∈ l₁) (hb : b ∈ l₂) : Pairwise R (l₁ ++ l₂) ↔ R a b ∧ Pairwise R l₁ ∧ Pairwise R l₂

theorem List.pairwise_cons_of_mem {α : Type u_1} {R : α → α → Prop} {l : List α} {a b : α} [Std.Symm R] [IsTrans α R] (h : b ∈ l) : Pairwise R (a :: l) ↔ R a b ∧ Pairwise R l

theorem List.Pairwise.rel_head_tail {α : Type u_1} {R : α → α → Prop} {l : List α} {a : α} (h₁ : Pairwise R l) (ha : a ∈ l.tail) : R (l.head ⋯) a

theorem List.Pairwise.rel_head_of_rel_head_head {α : Type u_1} {R : α → α → Prop} {l : List α} {a : α} (h₁ : Pairwise R l) (ha : a ∈ l) (hhead : R (l.head ⋯) (l.head ⋯)) : R (l.head ⋯) a

theorem List.Pairwise.rel_head {α : Type u_1} {R : α → α → Prop} {l : List α} {a : α} [Std.Refl R] (h₁ : Pairwise R l) (ha : a ∈ l) : R (l.head ⋯) a

theorem List.Pairwise.rel_dropLast_getLast {α : Type u_1} {R : α → α → Prop} {l : List α} {a : α} (h : Pairwise R l) (ha : a ∈ l.dropLast) : R a (l.getLast ⋯)

theorem List.Pairwise.rel_getLast_of_rel_getLast_getLast {α : Type u_1} {R : α → α → Prop} {l : List α} {a : α} (h₁ : Pairwise R l) (ha : a ∈ l) (hlast : R (l.getLast ⋯) (l.getLast ⋯)) : R a (l.getLast ⋯)

theorem List.Pairwise.rel_getLast {α : Type u_1} {R : α → α → Prop} {l : List α} {a : α} [Std.Refl R] (h₁ : Pairwise R l) (ha : a ∈ l) : R a (l.getLast ⋯)

theorem List.Pairwise.of_reverse {α : Type u_1} {R : α → α → Prop} {l : List α} : Pairwise R l.reverse → Pairwise (fun (a b : α) => R b a) l

Alias of the forward direction of List.pairwise_reverse.

theorem List.Pairwise.reverse {α : Type u_1} {R : α → α → Prop} {l : List α} : Pairwise (fun (a b : α) => R b a) l → Pairwise R l.reverse

Alias of the reverse direction of List.pairwise_reverse.

theorem List.Pairwise.head!_le {α : Type u_1} {R : α → α → Prop} {l : List α} {a : α} [Inhabited α] [Std.Refl R] (h : Pairwise R l) (ha : a ∈ l) : R l.head! a

theorem List.pairwise_replicate_of_refl {α : Type u_1} {R : α → α → Prop} {a : α} {n : ℕ} [Std.Refl R] : Pairwise R (replicate n a)

Pairwise filtering

theorem List.Pairwise.pwFilter {α : Type u_1} {R : α → α → Prop} [DecidableRel R] {l : List α} : Pairwise R l → pwFilter R l = l

Alias of the reverse direction of List.pwFilter_eq_self.

theorem List.pairwise_cons_cons_iff_of_trans {α : Type u_1} {R : α → α → Prop} [IsTrans α R] {l : List α} {a b : α} : Pairwise R (a :: b :: l) ↔ R a b ∧ Pairwise R (b :: l)

theorem List.Pairwise.cons_cons_of_trans {α : Type u_1} {R : α → α → Prop} [IsTrans α R] {l : List α} {a b : α} : R a b → Pairwise R (b :: l) → Pairwise R (a :: b :: l)

theorem List.Pairwise.rel_get_of_lt {α : Type u_1} {R : α → α → Prop} {l : List α} (h : Pairwise R l) {a b : Fin l.length} (hab : a < b) : R (l.get a) (l.get b)

theorem List.Pairwise.rel_get_of_le {α : Type u_1} {R : α → α → Prop} [Std.Refl R] {l : List α} (h : Pairwise R l) {a b : Fin l.length} (hab : a ≤ b) : R (l.get a) (l.get b)

theorem List.Pairwise.decide {α : Type u_1} {R : α → α → Prop} [DecidableRel R] (l : List α) (h : Pairwise R l) : Pairwise (fun (a b : α) => Decidable.decide (R a b) = true) l

TFAE

theorem List.tfae_iff_pairwise {l : List Prop} : l.TFAE ↔ Pairwise (fun (x1 x2 : Prop) => x1 ↔ x2) l

theorem List.tfae_append {l₁ l₂ : List Prop} : (l₁ ++ l₂).TFAE ↔ l₁.TFAE ∧ l₂.TFAE ∧ ∀ (a : Prop), a ∈ l₁ → ∀ (b : Prop), b ∈ l₂ → (a ↔ b)

theorem List.tfae_append_of_mem {a b : Prop} {l₁ l₂ : List Prop} (ha : a ∈ l₁) (hb : b ∈ l₂) : (l₁ ++ l₂).TFAE ↔ (a ↔ b) ∧ l₁.TFAE ∧ l₂.TFAE

theorem List.tfae_cons {a b : Prop} {l : List Prop} (h : b ∈ l) : (a :: l).TFAE ↔ (a ↔ b) ∧ l.TFAE

@[simp]

theorem List.tfae_cons_of_mem {a : Prop} {l : List Prop} (h : a ∈ l) : (a :: l).TFAE ↔ l.TFAE

theorem List.tfae_concat {a b : Prop} {l : List Prop} (h : b ∈ l) : (l ++ [a]).TFAE ↔ (a ↔ b) ∧ l.TFAE

@[simp]

theorem List.tfae_concat_of_mem {a : Prop} {l : List Prop} (h : a ∈ l) : (l ++ [a]).TFAE ↔ l.TFAE

theorem List.tfae_cons_cons {a b : Prop} {l : List Prop} : (a :: b :: l).TFAE ↔ (a ↔ b) ∧ (b :: l).TFAE

@[deprecated List.tfae_cons_of_mem (since := "2026-08-14")]

theorem List.tfae_cons_self {a : Prop} {l : List Prop} : (a :: a :: l).TFAE ↔ (a :: l).TFAE

theorem List.tfae_of_cycle {a b : Prop} {l : List Prop} (h_chain : IsChain (fun (x1 x2 : Prop) => x1 → x2) (a :: b :: l)) (h_last : l.getLastD b → a) : (a :: b :: l).TFAE