isMaximalClique — Mathlib

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)⟩

Похожие утверждения