OAI/Combinatorics/InfiniteMatroid/PackingCovering.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.InfiniteMatroidCounterexample.contraction_indep_compl_spanning line 9
2. lemma OAI.InfiniteMatroidCounterexample.spanning_union_of_restrictions line 17
3. lemma OAI.InfiniteMatroidCounterexample.indep_compl_of_selfDual_spanning line 29
4. lemma OAI.InfiniteMatroidCounterexample.independent_cover_of_packing_covering line 35

   Source documentation

   The mixed packing/covering reduction, not merely the two pure cases.

   lemma independent_cover_of_packing_covering {α : Type*} (M₀ M₁ : Matroid α)
       (hE₀ : M₀.E = univ) (hE₁ : M₁.E = univ) (hM₀ : M₀.dual = M₀) (hM₁ : M₁.dual = M₁)
       (h : HasPackingCovering M₀ M₁) :
       ∃ J₀ J₁ : Set α, M₀.Indep J₀ ∧ M₁.Indep J₁ ∧ J₀ ∪ J₁ = univ := by
   …

   Mentions: OAI.InfiniteMatroidCounterexample.HasPackingCovering