Skip to content

Commit

Permalink
add coclique number and maximum/maximal independent sets
Browse files Browse the repository at this point in the history
  • Loading branch information
ooovi committed Oct 31, 2024
1 parent 073f32c commit e2f3d3f
Showing 1 changed file with 55 additions and 0 deletions.
55 changes: 55 additions & 0 deletions Mathlib/Combinatorics/SimpleGraph/IndependentSet.lean
Original file line number Diff line number Diff line change
Expand Up @@ -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

0 comments on commit e2f3d3f

Please sign in to comment.