OAI/Combinatorics/PerfectMatching/ForcedReduction.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MatchingEntropy.LooplessGraph.RemainingVertex line 15
  2. instance OAI.MatchingEntropy.LooplessGraph.remainingVertexDecidable line 18
  3. def OAI.MatchingEntropy.LooplessGraph.RemainingEdge line 21
  4. instance OAI.MatchingEntropy.LooplessGraph.remainingEdgeDecidable line 24
  5. def OAI.MatchingEntropy.LooplessGraph.deleteEndpoints line 28
  6. theorem OAI.MatchingEntropy.LooplessGraph.remainingEdge_ne line 35
  7. theorem OAI.MatchingEntropy.LooplessGraph.remaining_of_incident line 41
  8. theorem OAI.MatchingEntropy.LooplessGraph.deleteEndpoints_incident line 49
  9. theorem OAI.MatchingEntropy.LooplessGraph.matching_common_vertex line 55
  10. theorem OAI.MatchingEntropy.LooplessGraph.matching_remaining line 63
  11. def OAI.MatchingEntropy.LooplessGraph.addForced line 72
  12. theorem OAI.MatchingEntropy.LooplessGraph.mem_addForced line 94
  13. theorem OAI.MatchingEntropy.LooplessGraph.mem_addForced_remaining line 107
  14. def OAI.MatchingEntropy.LooplessGraph.removeForced line 114
  15. theorem OAI.MatchingEntropy.LooplessGraph.mem_removeForced line 128
  16. def OAI.MatchingEntropy.LooplessGraph.forcedMatchingEquiv line 133
  17. theorem OAI.MatchingEntropy.LooplessGraph.addForced_injective line 157
  18. theorem OAI.MatchingEntropy.LooplessGraph.remaining_vertex_card line 164
  19. theorem OAI.MatchingEntropy.LooplessGraph.range_addForced line 178
  20. theorem OAI.MatchingEntropy.LooplessGraph.law_support_of_mean_one line 188
  21. theorem OAI.MatchingEntropy.LooplessGraph.forcedLaw_feasible line 202
  22. theorem OAI.MatchingEntropy.LooplessGraph.forced_coordinate_zero line 225
  23. theorem OAI.MatchingEntropy.LooplessGraph.separableLower_forced line 239
  24. theorem OAI.MatchingEntropy.entropy_fiberMass_injective line 254
  25. theorem OAI.MatchingEntropy.LooplessGraph.liftForced_feasible line 275
  26. theorem OAI.MatchingEntropy.LooplessGraph.maxMatchingEntropy_forced_le line 300