OAI/Combinatorics/InfiniteMatroid/DoubleRay.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.InfiniteMatroidCounterexample.bundleAt line 10

    Source documentation

    Inward (false) and outward (true) bundles with the central edge at -1.

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

    def bundleAt (n : ℤ) (b : Bool) : ℤ :=
…
  2. lemma OAI.InfiniteMatroidCounterexample.bundleAt_bounds line 13
  3. lemma OAI.InfiniteMatroidCounterexample.bundleAt_injective line 16
  4. lemma OAI.InfiniteMatroidCounterexample.bundleAt_right line 19
  5. lemma OAI.InfiniteMatroidCounterexample.bundleAt_left line 23
  6. def OAI.InfiniteMatroidCounterexample.parityBit line 28

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

  7. abbrev OAI.InfiniteMatroidCounterexample.Vertex line 29

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

  8. def OAI.InfiniteMatroidCounterexample.componentMap line 31

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

  9. def OAI.InfiniteMatroidCounterexample.globalComponentMap line 34

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

  10. lemma OAI.InfiniteMatroidCounterexample.globalComponentMap_injective line 37
  11. lemma OAI.InfiniteMatroidCounterexample.globalComponentMap_surjective line 50
  12. def OAI.InfiniteMatroidCounterexample.componentEquiv line 61

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

  13. def OAI.InfiniteMatroidCounterexample.rayMatroid line 103

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

  14. lemma OAI.InfiniteMatroidCounterexample.rayMatroid_ground line 106
  15. lemma OAI.InfiniteMatroidCounterexample.rayMatroid_indep_iff line 116
  16. lemma OAI.InfiniteMatroidCounterexample.rayMatroid_isBase_iff line 120
  17. lemma OAI.InfiniteMatroidCounterexample.selfDual_compl_base_iff line 125
  18. lemma OAI.InfiniteMatroidCounterexample.rayMatroid_selfDual line 132
  19. def OAI.InfiniteMatroidCounterexample.assignment line 141

    Source documentation

    The independent partition is assigned to vertices by parity.

    def assignment {α : Type*} (I : Set (ℤ × α)) (n : ℤ) : Set (α × Bool) :=
…
  20. lemma OAI.InfiniteMatroidCounterexample.assignment_indep line 144