English
If s is a maximum clique, then s is a maximal clique.
Русский
Если s является максимальной кликой, она также является максимальной кликой по определению.
LaTeX
$$$\\forall s,\\; (G.IsMaximumClique\\ s) \\Rightarrow \\text{Maximal } G.IsClique\\ s.toSet.$$$
Lean4
theorem isMaximalClique [Fintype α] (s : Finset α) (M : G.IsMaximumClique s) : Maximal G.IsClique s :=
⟨M.isClique, fun t ht hsub => by
by_contra hc
have fint : Fintype t := ofFinite ↑t
have ne : s ≠ t.toFinset := fun a ↦ by subst a; simp_all [Set.coe_toFinset, not_true_eq_false]
have hle : #t.toFinset ≤ #s := M.maximum t.toFinset (by simp [Set.coe_toFinset, ht])
have hlt : #s < #t.toFinset := card_lt_card (ssubset_of_ne_of_subset ne (Set.subset_toFinset.mpr hsub))
exact lt_irrefl _ (lt_of_lt_of_le hlt hle)⟩