1. FormalConjecturesForMathlib
  2. Data
  3. Set
  4. Triplewise
/- Copyright 2025 The Formal Conjectures Authors. Licensed under the Apache License, Version 2.0 (the "License"); you may not use this file except in compliance with the License. You may obtain a copy of the License at https://www.apache.org/licenses/LICENSE-2.0 Unless required by applicable law or agreed to in writing, software distributed under the License is distributed on an "AS IS" BASIS, WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. See the License for the specific language governing permissions and limitations under the License. -/ module public import Mathlib.Data.ENat.Lattice public import Mathlib.Data.Set.Card public import Mathlib.Order.CompletePartialOrder import Mathlib.Tactic.NormNum.Ineq@[expose] public sectiondef Triplewise {α : Type*} (r : α → α → α → Prop) : Prop := ∀ ⦃i j k ⦄, i ≠ j → j ≠ k → i ≠ k → r i j knamespace Setvariable {α : Type*} {r : α → α → α → Prop} {s t : Set α} {x y z : α}

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

protected def Triplewise (s : Set α) (r : α → α → α → Prop) : Prop := ∀ ⦃x⦄, x ∈ s → ∀ ⦃y⦄, y ∈ s → ∀ ⦃z⦄, z ∈ s → x ≠ y → y ≠ z → x ≠ z → r x y zprotected theorem Triplewise.eq (hs : s.Triplewise r) (hx : x ∈ s) (hy : y ∈ s) (hz : z ∈ s) (h : ¬r x y z) : x = y ∨ y = z ∨ x = z := α:Type u_1r:α → α → α → Props:Set αx:αy:αz:αhs:s.Triplewise rhx:x ∈ shy:y ∈ shz:z ∈ sh:¬r x y z⊢ x = y ∨ y = z ∨ x = z α:Type u_1r:α → α → α → Props:Set αx:αy:αz:αhs:s.Triplewise rhx:x ∈ shy:y ∈ shz:z ∈ sh:¬r x y zthis:x ≠ y → y ≠ z → x ≠ z → False⊢ x = y ∨ y = z ∨ x = z All goals completed! 🐙theorem Triplewise.mono (h : t ⊆ s) (hs : s.Triplewise r) : t.Triplewise r := fun _ hx _ hy _ hz hxy hyz hxz ↦ hs (h hx) (h hy) (h hz) hxy hyz hxz@[simp] theorem Triplewise_univ_iff : Set.univ.Triplewise r ↔ Triplewise r := α:Type u_1r:α → α → α → Prop⊢ univ.Triplewise r ↔ Triplewise r All goals completed! 🐙theorem triplewise_of_encard_lt (r : α → α → α → Prop) (h : s.encard < 3) : s.Triplewise r := α:Type u_1s:Set αr:α → α → α → Proph:s.encard < 3⊢ s.Triplewise r α:Type u_1s:Set αr:α → α → α → Proph:s.encard < 3⊢ ∀ ⦃x : α⦄, x ∈ s → ∀ ⦃y : α⦄, y ∈ s → ∀ ⦃z : α⦄, z ∈ s → x ≠ y → y ≠ z → x ≠ z → r x y z α:Type u_1s:Set αr:α → α → α → Proph:∃ x ∈ s, ∃ y ∈ s, ∃ z ∈ s, x ≠ y ∧ y ≠ z ∧ x ≠ z ∧ ¬r x y z⊢ 3 ≤ s.encard α:Type u_1s:Set αr:α → α → α → Propx:αhx:x ∈ sy:αhy:y ∈ sz:αhz:z ∈ shxy:x ≠ yhyz:y ≠ zhxz:x ≠ zright✝:¬r x y z⊢ 3 ≤ s.encard α:Type u_1s:Set αr:α → α → α → Propx:αhx:x ∈ sy:αhy:y ∈ sz:αhz:z ∈ shxy:x ≠ yhyz:y ≠ zhxz:x ≠ zright✝:¬r x y z⊢ 3 ≤ {x, y, z}.encardα:Type u_1s:Set αr:α → α → α → Propx:αhx:x ∈ sy:αhy:y ∈ sz:αhz:z ∈ shxy:x ≠ yhyz:y ≠ zhxz:x ≠ zright✝:¬r x y z⊢ {x, y, z}.encard ≤ s.encard α:Type u_1s:Set αr:α → α → α → Propx:αhx:x ∈ sy:αhy:y ∈ sz:αhz:z ∈ shxy:x ≠ yhyz:y ≠ zhxz:x ≠ zright✝:¬r x y z⊢ 3 ≤ {x, y, z}.encard α:Type u_1s:Set αr:α → α → α → Propx:αhx:x ∈ sy:αhy:y ∈ sz:αhz:z ∈ shxy:x ≠ yhyz:y ≠ zhxz:x ≠ zright✝:¬r x y z⊢ 3 ≤ 1 + 1 + 1 All goals completed! 🐙 α:Type u_1s:Set αr:α → α → α → Propx:αhx:x ∈ sy:αhy:y ∈ sz:αhz:z ∈ shxy:x ≠ yhyz:y ≠ zhxz:x ≠ zright✝:¬r x y z⊢ {x, y, z}.encard ≤ s.encard exact encard_le_encard_of_injOn (α:Type u_1s:Set αr:α → α → α → Propx:αhx:x ∈ sy:αhy:y ∈ sz:αhz:z ∈ shxy:x ≠ yhyz:y ≠ zhxz:x ≠ zright✝:¬r x y z⊢ MapsTo id {x, y, z} s All goals completed! 🐙) (injOn_id _)@[simp] theorem triplewise_empty (r : α → α → α → Prop) : Set.Triplewise ∅ r := (notMem_empty · · |>.elim)@[simp] theorem triplewise_singleton (r : α → α → α → Prop) : Set.Triplewise {x} r := α:Type u_1x:αr:α → α → α → Prop⊢ {x}.Triplewise r α:Type u_1x:αr:α → α → α → Prop⊢ {x}.encard < 3 All goals completed! 🐙@[simp] theorem triplewise_pair (r : α → α → α → Prop) : Set.Triplewise {x, y} r := α:Type u_1x:αy:αr:α → α → α → Prop⊢ {x, y}.Triplewise r α:Type u_1x:αy:αr:α → α → α → Prop⊢ {x, y}.encard < 3 α:Type u_1x:αy:αr:α → α → α → Prop⊢ {y}.encard + 1 < 3 α:Type u_1x:αy:αr:α → α → α → Prop⊢ 1 + 1 < 3 All goals completed! 🐙α:Type u_1r:α → α → α → Props:Set αx:αx✝:s.Triplewise r ∧ ∀ y ∈ s, ∀ z ∈ s, x ≠ y → x ≠ z → y ≠ z → r x y z ∧ r y x z ∧ r y z xhs:s.Triplewise rhxs:∀ y ∈ s, ∀ z ∈ s, x ≠ y → x ≠ z → y ≠ z → r x y z ∧ r y x z ∧ r y z xw:αhw:w = x ∨ w ∈ sy:αhy:y = x ∨ y ∈ sz:αhz:z = x ∨ z ∈ shwy:w ≠ yhyz:y ≠ zhwz:w ≠ z⊢ r w y z α:Type u_1r:α → α → α → Props:Set αhs:s.Triplewise rw:αy:αz:αhwy:w ≠ yhyz:y ≠ zhwz:w ≠ zx✝:s.Triplewise r ∧ ∀ y ∈ s, ∀ z ∈ s, w ≠ y → w ≠ z → y ≠ z → r w y z ∧ r y w z ∧ r y z whxs:∀ y ∈ s, ∀ z ∈ s, w ≠ y → w ≠ z → y ≠ z → r w y z ∧ r y w z ∧ r y z why:y = w ∨ y ∈ shz:z = w ∨ z ∈ s⊢ r w y zα:Type u_1r:α → α → α → Props:Set αx:αx✝:s.Triplewise r ∧ ∀ y ∈ s, ∀ z ∈ s, x ≠ y → x ≠ z → y ≠ z → r x y z ∧ r y x z ∧ r y z xhs:s.Triplewise rhxs:∀ y ∈ s, ∀ z ∈ s, x ≠ y → x ≠ z → y ≠ z → r x y z ∧ r y x z ∧ r y z xw:αy:αhy:y = x ∨ y ∈ sz:αhz:z = x ∨ z ∈ shwy:w ≠ yhyz:y ≠ zhwz:w ≠ zhw:w ∈ s⊢ r w y z α:Type u_1r:α → α → α → Props:Set αhs:s.Triplewise rw:αy:αz:αhwy:w ≠ yhyz:y ≠ zhwz:w ≠ zx✝:s.Triplewise r ∧ ∀ y ∈ s, ∀ z ∈ s, w ≠ y → w ≠ z → y ≠ z → r w y z ∧ r y w z ∧ r y z whxs:∀ y ∈ s, ∀ z ∈ s, w ≠ y → w ≠ z → y ≠ z → r w y z ∧ r y w z ∧ r y z why:y = w ∨ y ∈ shz:z = w ∨ z ∈ s⊢ r w y z α:Type u_1r:α → α → α → Props:Set αhs:s.Triplewise rw:αy:αz:αhwy:w ≠ yhyz:y ≠ zhwz:w ≠ zx✝:s.Triplewise r ∧ ∀ y ∈ s, ∀ z ∈ s, w ≠ y → w ≠ z → y ≠ z → r w y z ∧ r y w z ∧ r y z whxs:∀ y ∈ s, ∀ z ∈ s, w ≠ y → w ≠ z → y ≠ z → r w y z ∧ r y w z ∧ r y z why:y = w ∨ y ∈ shz:z = w ∨ z ∈ s⊢ y ∈ sα:Type u_1r:α → α → α → Props:Set αhs:s.Triplewise rw:αy:αz:αhwy:w ≠ yhyz:y ≠ zhwz:w ≠ zx✝:s.Triplewise r ∧ ∀ y ∈ s, ∀ z ∈ s, w ≠ y → w ≠ z → y ≠ z → r w y z ∧ r y w z ∧ r y z whxs:∀ y ∈ s, ∀ z ∈ s, w ≠ y → w ≠ z → y ≠ z → r w y z ∧ r y w z ∧ r y z why:y = w ∨ y ∈ shz:z = w ∨ z ∈ s⊢ z ∈ s α:Type u_1r:α → α → α → Props:Set αhs:s.Triplewise rw:αy:αz:αhwy:w ≠ yhyz:y ≠ zhwz:w ≠ zx✝:s.Triplewise r ∧ ∀ y ∈ s, ∀ z ∈ s, w ≠ y → w ≠ z → y ≠ z → r w y z ∧ r y w z ∧ r y z whxs:∀ y ∈ s, ∀ z ∈ s, w ≠ y → w ≠ z → y ≠ z → r w y z ∧ r y w z ∧ r y z why:y = w ∨ y ∈ shz:z = w ∨ z ∈ s⊢ y ∈ s All goals completed! 🐙 α:Type u_1r:α → α → α → Props:Set αhs:s.Triplewise rw:αy:αz:αhwy:w ≠ yhyz:y ≠ zhwz:w ≠ zx✝:s.Triplewise r ∧ ∀ y ∈ s, ∀ z ∈ s, w ≠ y → w ≠ z → y ≠ z → r w y z ∧ r y w z ∧ r y z whxs:∀ y ∈ s, ∀ z ∈ s, w ≠ y → w ≠ z → y ≠ z → r w y z ∧ r y w z ∧ r y z why:y = w ∨ y ∈ shz:z = w ∨ z ∈ s⊢ z ∈ s All goals completed! 🐙 α:Type u_1r:α → α → α → Props:Set αhs:s.Triplewise rw:αy:αz:αhwy:w ≠ yhyz:y ≠ zhwz:w ≠ zhw:w ∈ sx✝:s.Triplewise r ∧ ∀ y_1 ∈ s, ∀ z ∈ s, y ≠ y_1 → y ≠ z → y_1 ≠ z → r y y_1 z ∧ r y_1 y z ∧ r y_1 z yhxs:∀ y_1 ∈ s, ∀ z ∈ s, y ≠ y_1 → y ≠ z → y_1 ≠ z → r y y_1 z ∧ r y_1 y z ∧ r y_1 z yhz:z = y ∨ z ∈ s⊢ r w y zα:Type u_1r:α → α → α → Props:Set αx:αx✝:s.Triplewise r ∧ ∀ y ∈ s, ∀ z ∈ s, x ≠ y → x ≠ z → y ≠ z → r x y z ∧ r y x z ∧ r y z xhs:s.Triplewise rhxs:∀ y ∈ s, ∀ z ∈ s, x ≠ y → x ≠ z → y ≠ z → r x y z ∧ r y x z ∧ r y z xw:αy:αz:αhz:z = x ∨ z ∈ shwy:w ≠ yhyz:y ≠ zhwz:w ≠ zhw:w ∈ shy:y ∈ s⊢ r w y z α:Type u_1r:α → α → α → Props:Set αhs:s.Triplewise rw:αy:αz:αhwy:w ≠ yhyz:y ≠ zhwz:w ≠ zhw:w ∈ sx✝:s.Triplewise r ∧ ∀ y_1 ∈ s, ∀ z ∈ s, y ≠ y_1 → y ≠ z → y_1 ≠ z → r y y_1 z ∧ r y_1 y z ∧ r y_1 z yhxs:∀ y_1 ∈ s, ∀ z ∈ s, y ≠ y_1 → y ≠ z → y_1 ≠ z → r y y_1 z ∧ r y_1 y z ∧ r y_1 z yhz:z = y ∨ z ∈ s⊢ r w y z exact (hxs w hw z (α:Type u_1r:α → α → α → Props:Set αhs:s.Triplewise rw:αy:αz:αhwy:w ≠ yhyz:y ≠ zhwz:w ≠ zhw:w ∈ sx✝:s.Triplewise r ∧ ∀ y_1 ∈ s, ∀ z ∈ s, y ≠ y_1 → y ≠ z → y_1 ≠ z → r y y_1 z ∧ r y_1 y z ∧ r y_1 z yhxs:∀ y_1 ∈ s, ∀ z ∈ s, y ≠ y_1 → y ≠ z → y_1 ≠ z → r y y_1 z ∧ r y_1 y z ∧ r y_1 z yhz:z = y ∨ z ∈ s⊢ z ∈ s All goals completed! 🐙) hwy.symm hyz hwz).2.1 α:Type u_1r:α → α → α → Props:Set αhs:s.Triplewise rw:αy:αz:αhwy:w ≠ yhyz:y ≠ zhwz:w ≠ zhw:w ∈ shy:y ∈ sx✝:s.Triplewise r ∧ ∀ y ∈ s, ∀ z_1 ∈ s, z ≠ y → z ≠ z_1 → y ≠ z_1 → r z y z_1 ∧ r y z z_1 ∧ r y z_1 zhxs:∀ y ∈ s, ∀ z_1 ∈ s, z ≠ y → z ≠ z_1 → y ≠ z_1 → r z y z_1 ∧ r y z z_1 ∧ r y z_1 z⊢ r w y zα:Type u_1r:α → α → α → Props:Set αx:αx✝:s.Triplewise r ∧ ∀ y ∈ s, ∀ z ∈ s, x ≠ y → x ≠ z → y ≠ z → r x y z ∧ r y x z ∧ r y z xhs:s.Triplewise rhxs:∀ y ∈ s, ∀ z ∈ s, x ≠ y → x ≠ z → y ≠ z → r x y z ∧ r y x z ∧ r y z xw:αy:αz:αhwy:w ≠ yhyz:y ≠ zhwz:w ≠ zhw:w ∈ shy:y ∈ shz:z ∈ s⊢ r w y z α:Type u_1r:α → α → α → Props:Set αhs:s.Triplewise rw:αy:αz:αhwy:w ≠ yhyz:y ≠ zhwz:w ≠ zhw:w ∈ shy:y ∈ sx✝:s.Triplewise r ∧ ∀ y ∈ s, ∀ z_1 ∈ s, z ≠ y → z ≠ z_1 → y ≠ z_1 → r z y z_1 ∧ r y z z_1 ∧ r y z_1 zhxs:∀ y ∈ s, ∀ z_1 ∈ s, z ≠ y → z ≠ z_1 → y ≠ z_1 → r z y z_1 ∧ r y z z_1 ∧ r y z_1 z⊢ r w y z All goals completed! 🐙 All goals completed! 🐙theorem triplewise_insert_of_not_mem (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 := α:Type u_1r:α → α → α → Props: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 α:Type u_1r:α → α → α → Props:Set αx:αhx:x ∉ s⊢ ∀ a ∈ s, ∀ c ∈ s, x ≠ a → x ≠ c → a ≠ c → r x a c ∧ r a x c ∧ r a c x ↔ a ≠ c → r x a c ∧ r a x c ∧ r a c x α:Type u_1r:α → α → α → Props:Set αx:αhx:x ∉ sy:αhy:y ∈ sz:αhz:z ∈ s⊢ x ≠ y → x ≠ z → y ≠ z → r x y z ∧ r y x z ∧ r y z x ↔ y ≠ z → r x y z ∧ r y x z ∧ r y z x All goals completed! 🐙protected theorem Triplewise.insert (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 := Set.triplewise_insert.mpr ⟨hs, h⟩protected theorem Triplewise.insert_of_not_mem (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 := (Set.triplewise_insert_of_not_mem hx).mpr ⟨hs, h⟩theorem triplewise_set_pred_iff {S : Set α} {P : Set α → Prop} : S.Triplewise (P {·, ·, ·}) ↔ ∀ T ⊆ S, T.ncard = 3 → P T := α:Type u_1S:Set αP:Set α → Prop⊢ (S.Triplewise fun x1 x2 x3 ↦ P {x1, x2, x3}) ↔ ∀ T ⊆ S, T.ncard = 3 → P T α:Type u_1S:Set αP:Set α → Prop⊢ (S.Triplewise fun x1 x2 x3 ↦ P {x1, x2, x3}) → ∀ T ⊆ S, T.ncard = 3 → P Tα:Type u_1S:Set αP:Set α → Prop⊢ (∀ T ⊆ S, T.ncard = 3 → P T) → S.Triplewise fun x1 x2 x3 ↦ P {x1, x2, x3} α:Type u_1S:Set αP:Set α → Prop⊢ (S.Triplewise fun x1 x2 x3 ↦ P {x1, x2, x3}) → ∀ T ⊆ S, T.ncard = 3 → P T α:Type u_1S:Set αP:Set α → Proph:S.Triplewise fun x1 x2 x3 ↦ P {x1, x2, x3}T:Set αhT:T ⊆ ST_ncard:T.ncard = 3⊢ P T α:Type u_1S:Set αP:Set α → Proph:S.Triplewise fun x1 x2 x3 ↦ P {x1, x2, x3}x:αy:αz:αhxy:x ≠ yhxz:x ≠ zhyz:y ≠ zhT:{x, y, z} ⊆ ST_ncard:{x, y, z}.ncard = 3⊢ P {x, y, z} simp_rw α:Type u_1S:Set αP:Set α → Proph:S.Triplewise fun x1 x2 x3 ↦ P {x1, x2, x3}x:αy:αz:αhxy:x ≠ yhxz:x ≠ zhyz:y ≠ zhT:{x, y, z} ⊆ ST_ncard:{x, y, z}.ncard = 3⊢ P {x, y, z}α:Type u_1S:Set αP:Set α → Proph:S.Triplewise fun x1 x2 x3 ↦ P {x1, x2, x3}x:αy:αz:αhxy:x ≠ yhxz:x ≠ zhyz:y ≠ zT_ncard:{x, y, z}.ncard = 3hT:x ∈ S ∧ y ∈ S ∧ {z} ⊆ S⊢ P {x, y, z} α:Type u_1S:Set αP:Set α → Proph:S.Triplewise fun x1 x2 x3 ↦ P {x1, x2, x3}x:αy:αz:αhxy:x ≠ yhxz:x ≠ zhyz:y ≠ zT_ncard:{x, y, z}.ncard = 3hT:x ∈ S ∧ y ∈ S ∧ z ∈ S⊢ P {x, y, z}] at hT All goals completed! 🐙 α:Type u_1S:Set αP:Set α → Prop⊢ (∀ T ⊆ S, T.ncard = 3 → P T) → S.Triplewise fun x1 x2 x3 ↦ P {x1, x2, x3} α:Type u_1S:Set αP:Set α → Proph:∀ T ⊆ S, T.ncard = 3 → P Tx:αhx:x ∈ Sy:αhy:y ∈ Sz:αhz:z ∈ Shxy:x ≠ yhyz:y ≠ zhxz:x ≠ z⊢ P {x, y, z} α:Type u_1S:Set αP:Set α → Proph:∀ T ⊆ S, T.ncard = 3 → P Tx:αhx:x ∈ Sy:αhy:y ∈ Sz:αhz:z ∈ Shxy:x ≠ yhyz:y ≠ zhxz:x ≠ z⊢ {x, y, z} ⊆ S All goals completed! 🐙end Set