OAI/Combinatorics/MatchingCount/Graphs/Vertex.lean

GitHub source file

38 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.MatchingFPRAS.RealGeometry.Vertex line 9
  2. def OAI.MatchingFPRAS.RealGeometry.atVertex line 11
  3. lemma OAI.MatchingFPRAS.RealGeometry.atVertex_zero line 16
  4. lemma OAI.MatchingFPRAS.RealGeometry.atVertex_last line 19
  5. lemma OAI.MatchingFPRAS.RealGeometry.atVertex_internal line 22
  6. lemma OAI.MatchingFPRAS.RealGeometry.atVertex_eq_inr_iff line 29
  7. lemma OAI.MatchingFPRAS.RealGeometry.atVertex_eq_inl_iff line 47
  8. theorem OAI.MatchingFPRAS.RealGeometry.atVertex_injective line 57
  9. theorem OAI.MatchingFPRAS.RealGeometry.internal_private line 79
  10. def OAI.MatchingFPRAS.RealGeometry.edge line 86
  11. lemma OAI.MatchingFPRAS.RealGeometry.first_vertex_terminal line 89
  12. lemma OAI.MatchingFPRAS.RealGeometry.second_vertex_terminal line 96
  13. lemma OAI.MatchingFPRAS.RealGeometry.edge_ordered_injective line 103
  14. lemma OAI.MatchingFPRAS.RealGeometry.edge_ordered_not_reverse line 125
  15. theorem OAI.MatchingFPRAS.RealGeometry.edge_injective line 157
  16. def OAI.MatchingFPRAS.RealGeometry.activity line 166
  17. lemma OAI.MatchingFPRAS.RealGeometry.activity_symm line 171
  18. lemma OAI.MatchingFPRAS.RealGeometry.activity_nonneg line 177
  19. theorem OAI.MatchingFPRAS.RealGeometry.activity_on_edge line 186
  20. lemma OAI.MatchingFPRAS.RealGeometry.activity_eq_zero_of_not_edge line 200
  21. theorem OAI.MatchingFPRAS.RealGeometry.activity_eq_edge_or_zero line 208
  22. theorem OAI.MatchingFPRAS.RealGeometry.internal_incident_iff line 224
  23. theorem OAI.MatchingFPRAS.RealGeometry.internal_activity_le line 238
  24. lemma OAI.MatchingFPRAS.RealGeometry.edge_not_diag line 251
  25. def OAI.MatchingFPRAS.RealGeometry.realThreshold line 260
  26. def OAI.MatchingFPRAS.RealGeometry.logicalThreshold line 266
  27. def OAI.MatchingFPRAS.RealGeometry.contract line 271
  28. lemma OAI.MatchingFPRAS.RealGeometry.contract_terminal line 275
  29. lemma OAI.MatchingFPRAS.RealGeometry.contract_atVertex line 278
  30. lemma OAI.MatchingFPRAS.RealGeometry.contracted_edge line 289
  31. lemma OAI.MatchingFPRAS.RealGeometry.reachable_of_edge_reachable line 304
  32. theorem OAI.MatchingFPRAS.RealGeometry.threshold_contract line 313
  33. lemma OAI.MatchingFPRAS.RealGeometry.positions_reachable line 337
  34. theorem OAI.MatchingFPRAS.RealGeometry.threshold_lift_edge line 348
  35. theorem OAI.MatchingFPRAS.RealGeometry.terminal_threshold_iff line 359
  36. lemma OAI.MatchingFPRAS.RealGeometry.activity_on_eq line 373
  37. theorem OAI.MatchingFPRAS.RealGeometry.realThreshold_adj_iff line 380
  38. theorem OAI.MatchingFPRAS.RealGeometry.path_interval_reachable line 391