OAI/Combinatorics/InfiniteMatroid/PrototypeExtension.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.InfiniteMatroidCounterexample.prototypePair line 10
2. lemma OAI.InfiniteMatroidCounterexample.mem_prototypePair line 11
3. lemma OAI.InfiniteMatroidCounterexample.prototypePair_finite line 14
4. lemma OAI.InfiniteMatroidCounterexample.symmDiff_inter_right line 15
5. lemma OAI.InfiniteMatroidCounterexample.RankModel.good_union line 23
6. lemma OAI.InfiniteMatroidCounterexample.RankModel.good_pair line 40
7. lemma OAI.InfiniteMatroidCounterexample.RankModel.good_insert_pair line 59
8. lemma OAI.InfiniteMatroidCounterexample.RankModel.upper_difference_positive line 74
9. lemma OAI.InfiniteMatroidCounterexample.RankModel.lower_difference_positive line 81
10. lemma OAI.InfiniteMatroidCounterexample.RankModel.extend_unmet line 89

    Source documentation

    At an unmet interval the exact reservation construction adds one complementary pair.

    lemma extend_unmet {P : Set Prototype} (hP : R.GoodPrototypes P)
        (hcard : Cardinal.mk P < Cardinal.continuum) {I Y : Set E0} (hIY : I ⊆ Y)
        (hnot : ¬ Meets (PrototypeBases P) I Y) :
        ∃ B, R.GoodPrototypes (P ∪ prototypePair B) ∧ Meets (PrototypeBases (P ∪ prototypePair B)) I Y := by
    …

    Mentions: OAI.InfiniteMatroidCounterexample.Prototype, OAI.InfiniteMatroidCounterexample.E0, OAI.InfiniteMatroidCounterexample.Meets, OAI.InfiniteMatroidCounterexample.PrototypeBases, OAI.InfiniteMatroidCounterexample.prototypePair