From a3e14e0fda9abe2f950be653ea759c24fe21172c Mon Sep 17 00:00:00 2001
From: ovi <ovi@posteo.de>
Date: Thu, 31 Oct 2024 16:00:25 +0100
Subject: [PATCH] added a theorem on existence of a maximum clique

---
 Mathlib/Combinatorics/SimpleGraph/Clique.lean | 15 ++++++++++++---
 1 file changed, 12 insertions(+), 3 deletions(-)

diff --git a/Mathlib/Combinatorics/SimpleGraph/Clique.lean b/Mathlib/Combinatorics/SimpleGraph/Clique.lean
index bf740e5a79d07..3dfa9b62d22cb 100644
--- a/Mathlib/Combinatorics/SimpleGraph/Clique.lean
+++ b/Mathlib/Combinatorics/SimpleGraph/Clique.lean
@@ -635,15 +635,24 @@ lemma fintype_cliqueNum_bddAbove : BddAbove {n | ∃ s, G.IsNClique n s} := by
 theorem clique_card_le_cliqueNum (t : Finset α) (tc : G.IsClique t) : #t ≤ G.cliqueNum :=
   le_csSup fintype_cliqueNum_bddAbove (Exists.intro t ⟨tc, rfl⟩)
 
+lemma cliqueNum_attained : G.cliqueNum ∈ {n | ∃ s, G.IsNClique n s} :=
+    Nat.sSup_mem ⟨0, by simp[isNClique_empty.mpr rfl]⟩ fintype_cliqueNum_bddAbove
+
 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]
+  have ⟨s, sclique, scn⟩ := G.cliqueNum_attained
+  rw [← scn]
   exact LE.le.not_lt (tmax s sclique)
 
+theorem maximumClique_exists : ∃ s , G.isMaximumClique s := by
+  have ⟨s, smax⟩ := G.cliqueNum_attained
+  simp_all [isMaximumClique]
+  refine Exists.intro s ⟨smax.clique , ?_⟩
+  rw [smax.card_eq]
+  exact clique_card_le_cliqueNum
+
 end CliqueNumber
 
 end SimpleGraph