OAI/Combinatorics/InfiniteMatroid/Waves.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.InfiniteMatroidCounterexample.Wave line 8
2. theorem OAI.InfiniteMatroidCounterexample.exists_maximal_wave line 14
3. lemma OAI.InfiniteMatroidCounterexample.contractOnto_ground_sdiff line 46
4. lemma OAI.InfiniteMatroidCounterexample.contractOnto_ground line 49
5. lemma OAI.InfiniteMatroidCounterexample.Wave.lift_contract line 52
6. lemma OAI.InfiniteMatroidCounterexample.residual_wave_empty line 80
7. lemma OAI.InfiniteMatroidCounterexample.wave_of_restriction_packing line 90
8. lemma OAI.InfiniteMatroidCounterexample.FamilyCovering.empty line 99
9. lemma OAI.InfiniteMatroidCounterexample.residual_covering_condition line 104