OAI/Combinatorics/InfiniteMatroid/RankDescent.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.InfiniteMatroidCounterexample.raySlice line 9
2. lemma OAI.InfiniteMatroidCounterexample.raySlice_central line 12
3. lemma OAI.InfiniteMatroidCounterexample.raySlice_right line 17
4. lemma OAI.InfiniteMatroidCounterexample.raySlice_left line 29
5. def OAI.InfiniteMatroidCounterexample.rayVertex line 40
6. lemma OAI.InfiniteMatroidCounterexample.raySlice_step line 42
7. lemma OAI.InfiniteMatroidCounterexample.independent_rank_step line 61
8. lemma OAI.InfiniteMatroidCounterexample.no_independent_partition line 74
9. lemma OAI.InfiniteMatroidCounterexample.no_independent_cover line 99