OAI/Combinatorics/InfiniteMatroid/OrdinalRank.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.InfiniteMatroidCounterexample.SubsetIdeal.large_of_modSubset line 17
  2. lemma OAI.InfiniteMatroidCounterexample.SubsetIdeal.large_iff_symmDiff line 22
  3. structure OAI.InfiniteMatroidCounterexample.RankModel line 29

    Source documentation

    The properties of the ordinal rank which are used by the global assembly.

    structure RankModel (α : Type) where
…
  4. lemma OAI.InfiniteMatroidCounterexample.RankModel.invariant line 40
  5. lemma OAI.InfiniteMatroidCounterexample.exists_large_enumeration line 54
  6. lemma OAI.InfiniteMatroidCounterexample.rank_candidates_nonempty line 72
  7. def OAI.InfiniteMatroidCounterexample.ordinalRank line 77
  8. lemma OAI.InfiniteMatroidCounterexample.ordinalRank_spec line 83
  9. lemma OAI.InfiniteMatroidCounterexample.ordinalRank_le line 89
  10. lemma OAI.InfiniteMatroidCounterexample.ordinalRank_antitone line 94
  11. lemma OAI.InfiniteMatroidCounterexample.ordinalRank_thinning line 99
  12. lemma OAI.InfiniteMatroidCounterexample.exists_rankModel line 123