English
A finite subset s of α ⊕ β ⊕ γ forms a 3-clique in graph t if and only if there exists x ∈ t with toTriangle x = s.
Русский
Множество s ⊆ α ⊕ β ⊕ γ является 3- clique графа t тогда и только тогда существует x ∈ t, такое что toTriangle x = s.
LaTeX
$$$ (graph\ t).IsNClique\ 3\ s \;\iff\; \exists x\in t:\ toTriangle\ x = s $$$
Lean4
nonrec theorem is3Clique_iff [NoAccidental t] {s : Finset (α ⊕ β ⊕ γ)} :
(graph t).IsNClique 3 s ↔ ∃ x, x ∈ t ∧ toTriangle x = s :=
by
refine ⟨fun h ↦ ?_, ?_⟩
· rw [is3Clique_iff] at h
obtain ⟨x, y, z, hxy, hxz, hyz, rfl⟩ := h
obtain ⟨a, b, c, habc, hab, hac, hbc⟩ := graph_triple hxy hxz hyz
refine ⟨(a, b, c), ?_, habc⟩
obtain ⟨c', hc'⟩ := in₀₁_iff.1 hab
obtain ⟨b', hb'⟩ := in₀₂_iff.1 hac
obtain ⟨a', ha'⟩ := in₁₂_iff.1 hbc
obtain rfl | rfl | rfl := NoAccidental.eq_or_eq_or_eq ha' hb' hc' <;> assumption
· rintro ⟨x, hx, rfl⟩
exact toTriangle_is3Clique hx
