OAI/Combinatorics/ListHadwiger/PairedSources.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.LinearListHadwiger.Sampling.expectation_inter_card line 9
  2. lemma OAI.LinearListHadwiger.Sampling.expectation_inter_card_le line 24
  3. theorem OAI.LinearListHadwiger.Sampling.fixed_region line 32
  4. def OAI.LinearListHadwiger.PairedSources.graph line 121
  5. def OAI.LinearListHadwiger.PairedSources.routeHom line 143
  6. lemma OAI.LinearListHadwiger.PairedSources.lift_regular line 163
  7. structure OAI.LinearListHadwiger.PairedSources.Packing line 192
  8. lemma OAI.LinearListHadwiger.PairedSources.mapped_route line 204
  9. def OAI.LinearListHadwiger.PairedSources.Valid line 239
  10. lemma OAI.LinearListHadwiger.PairedSources.ordinary_valid_on_walk line 243
  11. lemma OAI.LinearListHadwiger.PairedSources.lift_source_path line 265
  12. theorem OAI.LinearListHadwiger.PairedSources.combine line 297