OAI/Combinatorics/Ramsey/CycleClique/Construction/IndependentPacking.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.CycleClique.Construction.HasIndependent.mono line 11
2. theorem OAI.CycleClique.Construction.exists_independent_subset line 19

   Source documentation

   A labelled independent set in an induced region supplies an actual ambient finset of exactly the certified weight.

   theorem exists_independent_subset {G : SimpleGraph V} {Y : Finset V} {n : ℕ}
       (h : HasIndependent (G.induce (Y : Set V)) n) :
       ∃ I : Finset V, I ⊆ Y ∧ G.IsIndepSet (I : Set V) ∧ I.card = n := by
   …

   Mentions: OAI.CycleClique.Construction.HasIndependent

3. theorem OAI.CycleClique.Construction.HasIndependent.le_indepNum line 36
4. theorem OAI.CycleClique.Construction.hasIndependent_iff_le_indepNum line 49
5. theorem OAI.CycleClique.Construction.hasIndependent_induce_mono line 62
6. theorem OAI.CycleClique.Construction.hasIndependent_one_of_nonempty line 71
7. theorem OAI.CycleClique.Construction.independent_packing line 78

   Source documentation

   The exact counting step behind both the terminal and finite packing tests. The regions may have different certified weights.

   theorem independent_packing [DecidableEq V] {G : SimpleGraph V} {k : ℕ}
       (hbound : IndependenceBound G k) (F : Finset ι) (I : ι → Finset V)
       (hind : ∀ i ∈ F, G.IsIndepSet (I i : Set V))
       (hdis : (F : Set ι).PairwiseDisjoint I)
       (hanti : ∀ i ∈ F, ∀ j ∈ F, i ≠ j → ∀ x ∈ I i, ∀ y ∈ I j, ¬ G.Adj x y) :
       ∑ i ∈ F, (I i).card ≤ k := by
   …

   Mentions: OAI.CycleClique.Construction.IndependenceBound