OAI/Combinatorics/InfiniteMatroid/Prototype.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.InfiniteMatroidCounterexample.sameClass_iff_differences line 10
  2. lemma OAI.InfiniteMatroidCounterexample.sameClass_of_small_gap line 17
  3. lemma OAI.InfiniteMatroidCounterexample.small_sdiff_of_class_subset line 26
  4. def OAI.InfiniteMatroidCounterexample.Outcome line 34
  5. lemma OAI.InfiniteMatroidCounterexample.outcome_compl line 35
  6. def OAI.InfiniteMatroidCounterexample.Meets line 41
  7. lemma OAI.InfiniteMatroidCounterexample.meets_mono line 42
  8. lemma OAI.InfiniteMatroidCounterexample.localRule_meets_of_small_left line 46
  9. lemma OAI.InfiniteMatroidCounterexample.localRule_meets_of_small_right line 72
  10. abbrev OAI.InfiniteMatroidCounterexample.Prototype line 82
  11. def OAI.InfiniteMatroidCounterexample.flipPrototype line 84
  12. lemma OAI.InfiniteMatroidCounterexample.flipPrototype_flip line 85
  13. def OAI.InfiniteMatroidCounterexample.PrototypeBases line 88
  14. lemma OAI.InfiniteMatroidCounterexample.prototypeBases_mono line 89
  15. lemma OAI.InfiniteMatroidCounterexample.localRule_subset_bases line 92
  16. structure OAI.InfiniteMatroidCounterexample.RankModel.GoodPrototypes line 98
  17. lemma OAI.InfiniteMatroidCounterexample.RankModel.good_empty line 103
  18. lemma OAI.InfiniteMatroidCounterexample.RankModel.bases_compl_closed line 105
  19. lemma OAI.InfiniteMatroidCounterexample.RankModel.bases_antichain line 110
  20. lemma OAI.InfiniteMatroidCounterexample.RankModel.bases_swap line 119
  21. lemma OAI.InfiniteMatroidCounterexample.RankModel.bases_admissible line 126
  22. lemma OAI.InfiniteMatroidCounterexample.RankModel.unmet_separation line 131