OAI/Combinatorics/MatchingCount/Sampling/Span.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MatchingFPRAS.Transport.OddPath.span line 15
  2. def OAI.MatchingFPRAS.Transport.OddPath.inside line 17
  3. def OAI.MatchingFPRAS.Transport.OddPath.ends line 19
  4. def OAI.MatchingFPRAS.Transport.OddPath.through line 21
  5. def OAI.MatchingFPRAS.Transport.OddPath.interior line 23
  6. def OAI.MatchingFPRAS.Transport.OddPath.closed line 25
  7. def OAI.MatchingFPRAS.Transport.OddPath.boundary line 27
  8. def OAI.MatchingFPRAS.Transport.OddPath.repaired line 30
  9. def OAI.MatchingFPRAS.Transport.OddPath.repairAdded line 33
  10. lemma OAI.MatchingFPRAS.Transport.OddPath.through_matching line 35
  11. lemma OAI.MatchingFPRAS.Transport.OddPath.interior_matching line 42
  12. lemma OAI.MatchingFPRAS.Transport.OddPath.inside_disjoint_ends line 58
  13. lemma OAI.MatchingFPRAS.Transport.OddPath.inside_union_ends line 71
  14. lemma OAI.MatchingFPRAS.Transport.OddPath.closed_matching line 87
  15. lemma OAI.MatchingFPRAS.Transport.OddPath.repaired_matching line 95
  16. lemma OAI.MatchingFPRAS.Transport.OddPath.closed_val line 108
  17. lemma OAI.MatchingFPRAS.Transport.OddPath.edge_injective line 117
  18. lemma OAI.MatchingFPRAS.Transport.OddPath.boundary_card line 136
  19. lemma OAI.MatchingFPRAS.Transport.OddPath.repair_conservation line 148
  20. structure OAI.MatchingFPRAS.Transport.CellPaths line 199