diff --git a/Mathlib/Combinatorics/SimpleGraph/IndependentSet.lean b/Mathlib/Combinatorics/SimpleGraph/IndependentSet.lean
index 4c431919d729b..0d7e7fdb90020 100644
--- a/Mathlib/Combinatorics/SimpleGraph/IndependentSet.lean
+++ b/Mathlib/Combinatorics/SimpleGraph/IndependentSet.lean
@@ -519,4 +519,59 @@ theorem independentSetFinset_map_of_equiv (e : α ≃ β) (n : ℕ) :
 -/
 end IndependentSetFinset
 
+section CocliqueNumber
+
+variable {α : Type*} {G : SimpleGraph α}
+
+/-- The maximal number of vertices of an independent set in a graph `G`. -/
+noncomputable def cocliqueNum (G : SimpleGraph α) : ℕ := sSup {n | ∃ s, G.IsNIndependentSet n s}
+
+lemma cocliqueNum_eq_compl_cliqueNum : G.cocliqueNum = Gᶜ.cliqueNum := by
+  simp [cliqueNum, ← isNIndependentSet_iff_isNClique_of_complement, cocliqueNum]
+
+/-- An independent set in a graph `G` such that there is no independent set with more vertices. -/
+def isMaximumIndependentSet (G : SimpleGraph α) (s : Finset α) : Prop :=
+  G.IsIndependentSet s ∧ ∀ (t : Finset α), G.IsIndependentSet t → #t ≤ #s
+
+lemma isMaximumIndependentSet_iff_compl_isMaximumClique (s : Finset α)  :
+    G.isMaximumIndependentSet s ↔ Gᶜ.isMaximumClique s := by
+  simp [isMaximumIndependentSet, isIndependentSet_iff_isClique_of_complement] at *
+  exact Iff.symm (Eq.to_iff rfl)
+
+/-- An independent set in a graph `G` that cannot be extended by adding vertices. -/
+def isMaximalIndependentSet (G : SimpleGraph α) (s : Finset α) : Prop :=
+  G.IsIndependentSet s ∧ ¬ ∃ (t : Finset α), G.IsIndependentSet t ∧ s ⊂ t
+
+lemma isMaximalIndependentSet_iff_compl_isMaximalClique (s : Finset α)  :
+    G.isMaximalIndependentSet s ↔ Gᶜ.isMaximalClique s := by
+  simp [isMaximalIndependentSet, isIndependentSet_iff_isClique_of_complement, ← not_and,
+  ← not_exists] at *
+  exact Iff.symm (Eq.to_iff rfl)
+
+lemma maximalIndependentSet_if_maximumIndependentSet
+    {s : Finset α} (smax : G.isMaximumIndependentSet s) : G.isMaximalIndependentSet s := by
+  simp [isMaximalIndependentSet, isMaximumIndependentSet,
+  isIndependentSet_iff_isClique_of_complement, ← not_and, ← not_exists] at *
+  exact maximalClique_if_maximumClique smax
+
+variable [fin : Fintype α]
+
+lemma fintype_cocliqueNum_bddAbove : BddAbove {n | ∃ s, G.IsNIndependentSet n s} := by
+  simp [isNIndependentSet_iff_isNClique_of_complement, fintype_cliqueNum_bddAbove,
+  cocliqueNum_eq_compl_cliqueNum]
+
+theorem independentSet_card_le_cocliqueNum (t : Finset α) (tc : G.IsIndependentSet t) :
+    #t ≤ G.cocliqueNum := by
+  simp [isIndependentSet_iff_isClique_of_complement, cocliqueNum,
+  isNIndependentSet_iff_isNClique_of_complement] at *
+  exact clique_card_le_cliqueNum t tc
+
+theorem maximumIndependentSet_card_eq_cocliqueNum
+    (t : Finset α) (tmc : G.isMaximumIndependentSet t) : #t = G.cocliqueNum := by
+  simp [isMaximumIndependentSet, isIndependentSet_iff_isClique_of_complement, cocliqueNum,
+  isNIndependentSet_iff_isNClique_of_complement] at *
+  exact maximumClique_card_eq_cliqueNum t tmc
+
+end CocliqueNumber
+
 end SimpleGraph