OAI/Combinatorics/InfiniteMatroid/Basic.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.InfiniteMatroidCounterexample.D line 9

   Also declared: ComparatorChallenges/InfiniteMatroid.lean:8 (same declaration text), ComparatorChallenges/InfiniteMatroidCorollaries.lean:8 (same declaration text).

2. abbrev OAI.InfiniteMatroidCounterexample.E0 line 10

   Also declared: ComparatorChallenges/InfiniteMatroidCorollaries.lean:9 (same declaration text).

3. abbrev OAI.InfiniteMatroidCounterexample.E line 11

   Also declared: ComparatorChallenges/InfiniteMatroid.lean:9 (same declaration text), ComparatorChallenges/InfiniteMatroidCorollaries.lean:10 (same declaration text).

4. def OAI.InfiniteMatroidCounterexample.contractOnto line 13

   Also declared: ComparatorChallenges/InfiniteMatroid.lean:11 (same declaration text), ComparatorChallenges/InfiniteMatroidCorollaries.lean:12 (same declaration text).

5. def OAI.InfiniteMatroidCounterexample.HasPackingCovering line 16

   Also declared: ComparatorChallenges/InfiniteMatroid.lean:14 (same declaration text), ComparatorChallenges/InfiniteMatroidCorollaries.lean:15 (same declaration text).