English
G.CliqueFreeOn s 2 is equivalent to s being pairwise non-adjacent complement.
Русский
G.CliqueFreeOn s 2 эквивалентно тому, что для любых двух элементов из s они не образуют клику, с точки зрения дополнения взаимной смежности.
LaTeX
$$For graph $G$ and set $s$, $G.CliqueFreeOn s 2$ iff $s$ is pairwise $(G$-adjacency complemented$)$.$$
Lean4
@[simp]
theorem cliqueFreeOn_two : G.CliqueFreeOn s 2 ↔ s.Pairwise (G.Adjᶜ) := by
classical
refine ⟨fun h a ha b hb _ hab => h ?_ ⟨by simpa [hab.ne], card_pair hab.ne⟩, ?_⟩
· push_cast
exact Set.insert_subset_iff.2 ⟨ha, Set.singleton_subset_iff.2 hb⟩
simp only [CliqueFreeOn, isNClique_iff, card_eq_two, not_and, not_exists]
rintro h t hst ht a b hab rfl
simp only [coe_insert, coe_singleton, Set.insert_subset_iff, Set.singleton_subset_iff] at hst
refine h hst.1 hst.2 hab (ht ?_ ?_ hab) <;> simp
