OAI/Combinatorics/InfiniteMatroid/Reservations.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.InfiniteMatroidCounterexample.liftD line 10
  2. lemma OAI.InfiniteMatroidCounterexample.density_liftD line 12
  3. lemma OAI.InfiniteMatroidCounterexample.small_liftD_iff line 21
  4. def OAI.InfiniteMatroidCounterexample.DCell line 25
  5. def OAI.InfiniteMatroidCounterexample.HCell line 28
  6. lemma OAI.InfiniteMatroidCounterexample.dCell_subset_Acompl line 30
  7. lemma OAI.InfiniteMatroidCounterexample.hCell_disjoint line 34
  8. lemma OAI.InfiniteMatroidCounterexample.card_avoid_cells line 39
  9. def OAI.InfiniteMatroidCounterexample.avoidCells line 53
  10. lemma OAI.InfiniteMatroidCounterexample.eventually_avoidCells line 56
  11. lemma OAI.InfiniteMatroidCounterexample.eventually_avoidHCells line 79
  12. lemma OAI.InfiniteMatroidCounterexample.small_biUnion line 86
  13. lemma OAI.InfiniteMatroidCounterexample.bad_cells_finite line 96
  14. lemma OAI.InfiniteMatroidCounterexample.simultaneous_reservations line 134