English
If t is explicitly disjoint, then the family {toTriangle(z) : z ∈ t} consists of pairwise disjoint vertex-sets.
Русский
Если t имеет явную несоприкосновенность, то семейство {toTriangle(z) : z ∈ t} образует пары непересекающихся наборов вершин.
LaTeX
$$$\forall z_1,z_2\in t,\ z_1\neq z_2\Rightarrow (toTriangle\ z_1)\cap (toTriangle\ z_2)=\emptyset$$$
Lean4
theorem map_toTriangle_disjoint [ExplicitDisjoint t] :
(t.map toTriangle : Set (Finset (α ⊕ β ⊕ γ))).Pairwise fun x y ↦ (x ∩ y : Set (α ⊕ β ⊕ γ)).Subsingleton :=
by
intro
simp only [Finset.coe_map, Set.mem_image, Finset.mem_coe, Prod.exists, Ne, forall_exists_index, and_imp]
rintro a b c habc rfl e x y z hxyz rfl h'
have := ne_of_apply_ne _ h'
simp only [Ne, Prod.mk_inj, not_and] at this
simp only [toTriangle_apply, in₀, in₁, in₂, Set.mem_inter_iff, mem_insert, mem_singleton, mem_coe, and_imp,
Sum.forall, Set.Subsingleton]
suffices ¬(a = x ∧ b = y) ∧ ¬(a = x ∧ c = z) ∧ ¬(b = y ∧ c = z) by aesop
refine ⟨?_, ?_, ?_⟩
· rintro ⟨rfl, rfl⟩
exact this rfl rfl (ExplicitDisjoint.inj₂ habc hxyz)
· rintro ⟨rfl, rfl⟩
exact this rfl (ExplicitDisjoint.inj₁ habc hxyz) rfl
· rintro ⟨rfl, rfl⟩
exact this (ExplicitDisjoint.inj₀ habc hxyz) rfl rfl
