def Triplewise {α : Type u_1} (r : α → α → α → Prop) : Prop

Equations

• Triplewise r = ∀ ⦃i j k : α⦄, i ≠ j → j ≠ k → i ≠ k → r i j k

def Set.Triplewise {α : Type u_1} (s : Set α) (r : α → α → α → Prop) : Prop

The ternary relation r holds triplewise on the set s if r x y z for all distinct x y z ∈ s.

Equations

• s.Triplewise r = ∀ ⦃x : α⦄, x ∈ s → ∀ ⦃y : α⦄, y ∈ s → ∀ ⦃z : α⦄, z ∈ s → x ≠ y → y ≠ z → x ≠ z → r x y z

theorem Set.Triplewise.eq {α : Type u_1} {r : α → α → α → Prop} {s : Set α} {x y z : α} (hs : s.Triplewise r) (hx : x ∈ s) (hy : y ∈ s) (hz : z ∈ s) (h : ¬r x y z) : x = y ∨ y = z ∨ x = z

theorem Set.Triplewise.mono {α : Type u_1} {r : α → α → α → Prop} {s t : Set α} (h : t ⊆ s) (hs : s.Triplewise r) : t.Triplewise r

@[simp]

theorem Set.Triplewise_univ_iff {α : Type u_1} {r : α → α → α → Prop} : univ.Triplewise r ↔ Triplewise r

theorem Set.triplewise_of_encard_lt {α : Type u_1} {s : Set α} (r : α → α → α → Prop) (h : s.encard < 3) : s.Triplewise r

@[simp]

theorem Set.triplewise_empty {α : Type u_1} (r : α → α → α → Prop) : ∅.Triplewise r

@[simp]

theorem Set.triplewise_singleton {α : Type u_1} {x : α} (r : α → α → α → Prop) : {x}.Triplewise r

@[simp]

theorem Set.triplewise_pair {α : Type u_1} {x y : α} (r : α → α → α → Prop) : {x, y}.Triplewise r

theorem Set.triplewise_insert {α : Type u_1} {r : α → α → α → Prop} {s : Set α} {x : α} : (insert x s).Triplewise r ↔ s.Triplewise r ∧ ∀ y ∈ s, ∀ z ∈ s, x ≠ y → x ≠ z → y ≠ z → r x y z ∧ r y x z ∧ r y z x

theorem Set.triplewise_insert_of_not_mem {α : Type u_1} {r : α → α → α → Prop} {s : Set α} {x : α} (hx : x ∉ s) : (insert x s).Triplewise r ↔ s.Triplewise r ∧ ∀ y ∈ s, ∀ z ∈ s, y ≠ z → r x y z ∧ r y x z ∧ r y z x

theorem Set.Triplewise.insert {α : Type u_1} {r : α → α → α → Prop} {s : Set α} {x : α} (hs : s.Triplewise r) (h : ∀ y ∈ s, ∀ z ∈ s, x ≠ y → x ≠ z → y ≠ z → r x y z ∧ r y x z ∧ r y z x) : (insert x s).Triplewise r

theorem Set.Triplewise.insert_of_not_mem {α : Type u_1} {r : α → α → α → Prop} {s : Set α} {x : α} (hx : x ∉ s) (hs : s.Triplewise r) (h : ∀ y ∈ s, ∀ z ∈ s, y ≠ z → r x y z ∧ r y x z ∧ r y z x) : (insert x s).Triplewise r

theorem Set.triplewise_set_pred_iff {α : Type u_1} {S : Set α} {P : Set α → Prop} : (S.Triplewise fun (x1 x2 x3 : α) => P {x1, x2, x3}) ↔ ∀ T ⊆ S, T.ncard = 3 → P T