Triplewise predicates on list.

Main definitions

• List.Triplewise says that a predicate applies to all ordered triples of elements of a list.

inductive List.Triplewise {α : Type u_1} (p : α → α → α → Prop) : List α → Prop

Whether a predicate holds for all ordered triples of elements of a list.

• nil {α : Type u_1} {p : α → α → α → Prop} : Triplewise p []
• cons {α : Type u_1} {p : α → α → α → Prop} {a : α} {l : List α} : Pairwise (p a) l → Triplewise p l → Triplewise p (a :: l)

theorem List.triplewise_iff {α : Type u_1} (p : α → α → α → Prop) (a✝ : List α) : Triplewise p a✝ ↔ a✝ = [] ∨ ∃ (a : α), ∃ (l : List α), Pairwise (p a) l ∧ Triplewise p l ∧ a✝ = a :: l

theorem List.triplewise_cons {α : Type u_1} {a : α} {l : List α} {p : α → α → α → Prop} : Triplewise p (a :: l) ↔ Pairwise (p a) l ∧ Triplewise p l

@[simp]

theorem List.triplewise_singleton {α : Type u_1} (a : α) (p : α → α → α → Prop) : Triplewise p [a]

@[simp]

theorem List.triplewise_pair {α : Type u_1} (a b : α) (p : α → α → α → Prop) : Triplewise p [a, b]

@[simp]

theorem List.triplewise_triple {α : Type u_1} {a b c : α} {p : α → α → α → Prop} : Triplewise p [a, b, c] ↔ p a b c

theorem List.Triplewise.imp {α : Type u_1} {l : List α} {p q : α → α → α → Prop} (h : ∀ {a b c : α}, p a b c → q a b c) (hl : Triplewise p l) : Triplewise q l

theorem List.triplewise_map {α : Type u_1} {β : Type u_2} {l : List α} {f : α → β} {p' : β → β → β → Prop} : Triplewise p' (map f l) ↔ Triplewise (fun (a b c : α) => p' (f a) (f b) (f c)) l

theorem List.Triplewise.of_map {α : Type u_1} {β : Type u_2} {l : List α} {p : α → α → α → Prop} {f : α → β} {p' : β → β → β → Prop} (h : ∀ {a b c : α}, p' (f a) (f b) (f c) → p a b c) (hl : Triplewise p' (List.map f l)) : Triplewise p l

theorem List.Triplewise.map {α : Type u_1} {β : Type u_2} {l : List α} {p : α → α → α → Prop} {f : α → β} {p' : β → β → β → Prop} (h : ∀ {a b c : α}, p a b c → p' (f a) (f b) (f c)) (hl : Triplewise p l) : Triplewise p' (List.map f l)

theorem List.triplewise_iff_getElem {α : Type u_1} {l : List α} {p : α → α → α → Prop} : Triplewise p l ↔ ∀ (i j k : Nat) (hij : i < j) (hjk : j < k) (hk : k < l.length), p l[i] l[j] l[k]

theorem List.triplewise_append {α : Type u_1} {l₁ l₂ : List α} {p : α → α → α → Prop} : Triplewise p (l₁ ++ l₂) ↔ Triplewise p l₁ ∧ Triplewise p l₂ ∧ (∀ (a : α), a ∈ l₁ → Pairwise (p a) l₂) ∧ ∀ (a : α), a ∈ l₂ → Pairwise (fun (x y : α) => p x y a) l₁

theorem List.triplewise_reverse {α : Type u_1} {l : List α} {p : α → α → α → Prop} : Triplewise p l.reverse ↔ Triplewise (fun (a b c : α) => p c b a) l