OAI/Combinatorics/InfiniteMatroid/Cardinality.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.InfiniteMatroidCounterexample.CIndex line 11
2. lemma OAI.InfiniteMatroidCounterexample.cindex_card line 13
3. lemma OAI.InfiniteMatroidCounterexample.cindex_initial line 15
4. lemma OAI.InfiniteMatroidCounterexample.cindex_predecessors line 18
5. lemma OAI.InfiniteMatroidCounterexample.cindex_initial_segment line 21
6. lemma OAI.InfiniteMatroidCounterexample.finite_union_small line 34

   Source documentation

   Cardinal arithmetic used at each stage; it does not assert regularity of the continuum.

   lemma finite_union_small {α ι : Type} (hι : Cardinal.mk ι < Cardinal.continuum)
       (F : ι → Set α) (hF : ∀ i, (F i).Finite) :
       Cardinal.mk (⋃ i, F i) < Cardinal.continuum := by
   …

7. lemma OAI.InfiniteMatroidCounterexample.exists_avoid_finite_family line 48
8. lemma OAI.InfiniteMatroidCounterexample.binary_card line 59
9. def OAI.InfiniteMatroidCounterexample.cindexBinaryEquiv line 64
10. lemma OAI.InfiniteMatroidCounterexample.exists_set_enumeration line 68

    Source documentation

    Enumeration of all subsets of any countably infinite type, on the initial continuum ordinal.

    lemma exists_set_enumeration (α : Type) [Countable α] [Infinite α] :
        ∃ f : CIndex → Set α, Function.Surjective f := by
    …

    Mentions: OAI.InfiniteMatroidCounterexample.CIndex

11. lemma OAI.InfiniteMatroidCounterexample.cardinal_prod_bool_lt line 76