OAI/Combinatorics/InfiniteMatroid/TransfiniteConstruction.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.InfiniteMatroidCounterexample.stagePrototypes line 11
  2. lemma OAI.InfiniteMatroidCounterexample.stagePrototypes_finite line 14
  3. def OAI.InfiniteMatroidCounterexample.pastPrototypes line 19
  4. def OAI.InfiniteMatroidCounterexample.initialPrototypes line 21
  5. def OAI.InfiniteMatroidCounterexample.allPrototypes line 23
  6. lemma OAI.InfiniteMatroidCounterexample.stage_subset_past line 26
  7. lemma OAI.InfiniteMatroidCounterexample.stage_subset_initial line 30
  8. lemma OAI.InfiniteMatroidCounterexample.initial_subset_past line 35
  9. lemma OAI.InfiniteMatroidCounterexample.initial_subset_all line 41
  10. lemma OAI.InfiniteMatroidCounterexample.past_cardinal line 47
  11. lemma OAI.InfiniteMatroidCounterexample.exists_interval_enumeration line 51
  12. lemma OAI.InfiniteMatroidCounterexample.RankModel.good_past_of_initial line 63
  13. lemma OAI.InfiniteMatroidCounterexample.RankModel.good_all_of_initial line 80
  14. lemma OAI.InfiniteMatroidCounterexample.RankModel.exists_stage line 98
  15. def OAI.InfiniteMatroidCounterexample.RankModel.assemblyStep line 110
  16. def OAI.InfiniteMatroidCounterexample.RankModel.assembled line 119
  17. lemma OAI.InfiniteMatroidCounterexample.RankModel.assembled_eq line 122
  18. lemma OAI.InfiniteMatroidCounterexample.RankModel.assemblyStep_spec line 126
  19. lemma OAI.InfiniteMatroidCounterexample.RankModel.assembled_good_initial line 138
  20. lemma OAI.InfiniteMatroidCounterexample.RankModel.assembled_meets line 148
  21. lemma OAI.InfiniteMatroidCounterexample.RankModel.exists_complete_prototypes line 158

    Source documentation

    The continuum recursion meets every interval and preserves all old classes.

    lemma exists_complete_prototypes : ∃ P : Set Prototype,
    R.GoodPrototypes P ∧ ∀ I Y, I ⊆ Y → Meets (PrototypeBases P) I Y := by
…

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

  22. lemma OAI.InfiniteMatroidCounterexample.RankModel.exists_basisSystem line 167