OAI/Combinatorics/InfiniteMatroid/LocalBases.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. instance OAI.InfiniteMatroidCounterexample.d_infinite line 13
2. instance OAI.InfiniteMatroidCounterexample.e0_infinite line 17
3. instance OAI.InfiniteMatroidCounterexample.d_countable line 18
4. instance OAI.InfiniteMatroidCounterexample.e0_countable line 19
5. def OAI.InfiniteMatroidCounterexample.labelEquiv line 21
6. def OAI.InfiniteMatroidCounterexample.natProbe line 25
7. lemma OAI.InfiniteMatroidCounterexample.natProbe_cylinder line 28
8. lemma OAI.InfiniteMatroidCounterexample.natProbe_shift line 50
9. lemma OAI.InfiniteMatroidCounterexample.fProbe_interpolation line 64
10. def OAI.InfiniteMatroidCounterexample.LocalLower line 97
11. lemma OAI.InfiniteMatroidCounterexample.localLower_antichain line 100