feat(SimpleGraph): independent sets

Mathlib.lean

@@ -2108,6 +2108,7 @@ import Mathlib.Combinatorics.SimpleGraph.Girth
 import Mathlib.Combinatorics.SimpleGraph.Hamiltonian
 import Mathlib.Combinatorics.SimpleGraph.Hasse
 import Mathlib.Combinatorics.SimpleGraph.IncMatrix
+import Mathlib.Combinatorics.SimpleGraph.IndependentSet
 import Mathlib.Combinatorics.SimpleGraph.Init
 import Mathlib.Combinatorics.SimpleGraph.LapMatrix
 import Mathlib.Combinatorics.SimpleGraph.LineGraph

Mathlib/Combinatorics/SimpleGraph/Clique.lean

@@ -6,6 +6,8 @@
 import Mathlib.Combinatorics.SimpleGraph.Path
 import Mathlib.Combinatorics.SimpleGraph.Operations
 import Mathlib.Data.Finset.Pairwise
+import Mathlib.Data.Nat.Lattice
+
 
 /-!
 # Graph cliques
@@ -152,6 +154,17 @@
     (G.map f).IsClique (s.map f) := by
   simpa
 
+lemma isClique_compl_map_iff_isClique_map_compl {f : α ↪ β} {s : Set α} :
+    (SimpleGraph.map f G)ᶜ.IsClique (f '' s) ↔ (SimpleGraph.map f Gᶜ).IsClique (f '' s) := by
+  repeat rw [isClique_iff, Set.Pairwise]
+  rw [forall₂_congr]; intro a ha
+  rw [forall₂_congr]; intro b hb
+  rw [←imp_congr_right]; intro hab
+  obtain ⟨a', _, ha'a⟩ := ha
+  obtain ⟨b', _, hb'b⟩ := hb
+  subst ha'a hb'b
+  simp only [map_adj_apply, compl_adj, ne_eq, EmbeddingLike.apply_eq_iff_eq]
+
 end Clique
 
 /-! ### `n`-cliques -/
@@ -594,4 +607,54 @@
 
 end CliqueFinset
 
+/-! ### Clique number -/
+
+
+section CliqueNumber
+
+variable {α : Type*} {G : SimpleGraph α}
+
+/-- The maximal number of vertices in a graph `G`. -/
+noncomputable def cliqueNum (G : SimpleGraph α) : ℕ := sSup {n | ∃ s, G.IsNClique n s}
+
+/-- A clique in a graph `G` such that there is no clique with more vertices. -/
+def isMaximumClique (G : SimpleGraph α) (s : Finset α) : Prop :=
+  G.IsClique s ∧ ∀ (t : Finset α), G.IsClique t → #t ≤ #s
+
+/-- A clique in a graph `G` that cannot be extended by adding vertices. -/
+def isMaximalClique (G : SimpleGraph α) (s : Finset α) : Prop :=
+  G.IsClique s ∧ ¬ ∃ (t : Finset α), G.IsClique t ∧ s ⊂ t
+
+lemma maximalClique_if_maximumClique {s : Finset α} (smax : G.isMaximumClique s) :
+    G.isMaximalClique s := by
+  rw [isMaximalClique, isMaximumClique] at *
+  by_contra h
+  simp_all only [not_exists, not_and, not_forall, Classical.not_imp, not_not, true_implies]
+  let ⟨t, tc, tsub⟩ := h
+  let ⟨_ , smaxf⟩ := smax
+  exact (not_and_self_iff (#t ≤ #s)).mp ⟨not_le_of_lt (card_lt_card tsub), smaxf t tc⟩
+
+variable [fin : Fintype α]
+
+lemma fintype_cliqueNum_bddAbove : BddAbove {n | ∃ s, G.IsNClique n s} := by
+  rw [bddAbove_def]
+  refine Exists.intro (Fintype.card α) ?_
+  rintro y ⟨sy, syc⟩
+  rw [isNClique_iff, ← And.right syc] at *
+  exact Finset.card_le_card (Finset.subset_univ sy)
+
+theorem clique_card_le_cliqueNum (t : Finset α) (tc : G.IsClique t) : #t ≤ G.cliqueNum :=
+  le_csSup fintype_cliqueNum_bddAbove (Exists.intro t ⟨tc, rfl⟩)
+
+theorem maximumClique_card_eq_cliqueNum (t : Finset α) (tmc : G.isMaximumClique t) :
+    #t = G.cliqueNum := by
+  let ⟨tclique, tmax⟩ := tmc
+  refine eq_of_le_of_not_lt (clique_card_le_cliqueNum _ tclique) ?_
+  have ⟨s, sclique, scn⟩ : G.cliqueNum ∈ {n | ∃ s, G.IsNClique n s} :=
+    Nat.sSup_mem ⟨ 0, by simp[isNClique_empty.mpr rfl] ⟩ fintype_cliqueNum_bddAbove
+  rw [cliqueNum, ← scn]
+  exact LE.le.not_lt (tmax s sclique)
+
+end CliqueNumber
+
 end SimpleGraph