OAI/Combinatorics/InfiniteMatroid/BasisExtension.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.InfiniteMatroidCounterexample.sameClass_compl line 10
2. lemma OAI.InfiniteMatroidCounterexample.sameClass_add line 14
3. lemma OAI.InfiniteMatroidCounterexample.sameClass_delete line 21
4. lemma OAI.InfiniteMatroidCounterexample.positive_sameClass line 28
5. lemma OAI.InfiniteMatroidCounterexample.positive_pool_delete line 36
6. lemma OAI.InfiniteMatroidCounterexample.localLower_self line 46
7. lemma OAI.InfiniteMatroidCounterexample.localLower_swap line 55
8. lemma OAI.InfiniteMatroidCounterexample.localLower_correct_up line 78
9. lemma OAI.InfiniteMatroidCounterexample.localLower_correct_down line 87
10. def OAI.InfiniteMatroidCounterexample.LocalUpper line 97

    Source documentation

    Upper rule with its complement identity built into the definition.

    def LocalUpper (T : Set E0) : Set (Set E0) := {X | Xᶜ ∈ LocalLower Tᶜ}

    Mentions: OAI.InfiniteMatroidCounterexample.E0, OAI.InfiniteMatroidCounterexample.LocalLower

11. lemma OAI.InfiniteMatroidCounterexample.localUpper_iff line 99
12. def OAI.InfiniteMatroidCounterexample.LocalRule line 111
13. lemma OAI.InfiniteMatroidCounterexample.localRule_class line 114
14. lemma OAI.InfiniteMatroidCounterexample.localRule_self line 121
15. lemma OAI.InfiniteMatroidCounterexample.localRule_compl line 128
16. lemma OAI.InfiniteMatroidCounterexample.localRule_antichain line 134
17. lemma OAI.InfiniteMatroidCounterexample.localRule_swap line 143
18. lemma OAI.InfiniteMatroidCounterexample.localLower_interval line 159
19. lemma OAI.InfiniteMatroidCounterexample.localLower_lower_endpoint line 177
20. lemma OAI.InfiniteMatroidCounterexample.localLower_upper_endpoint line 189
21. lemma OAI.InfiniteMatroidCounterexample.localRule_interval line 201
22. lemma OAI.InfiniteMatroidCounterexample.localRule_lower_endpoint line 220
23. lemma OAI.InfiniteMatroidCounterexample.localRule_upper_endpoint line 240