OAI/Combinatorics/MatchingEntropy/EdgeReduction.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MatchingEntropyBounds.LooplessGraph.RemainingVertex line 17
  2. instance OAI.MatchingEntropyBounds.LooplessGraph.remainingVertexDecidable line 20
  3. def OAI.MatchingEntropyBounds.LooplessGraph.RemainingEdge line 23
  4. instance OAI.MatchingEntropyBounds.LooplessGraph.remainingEdgeDecidable line 26
  5. def OAI.MatchingEntropyBounds.LooplessGraph.deleteEndpoints line 30
  6. theorem OAI.MatchingEntropyBounds.LooplessGraph.remainingEdge_ne line 37
  7. theorem OAI.MatchingEntropyBounds.LooplessGraph.remaining_of_incident line 43
  8. theorem OAI.MatchingEntropyBounds.LooplessGraph.deleteEndpoints_incident line 51
  9. theorem OAI.MatchingEntropyBounds.LooplessGraph.matching_common_vertex line 57
  10. theorem OAI.MatchingEntropyBounds.LooplessGraph.matching_remaining line 65
  11. def OAI.MatchingEntropyBounds.LooplessGraph.addForced line 74
  12. theorem OAI.MatchingEntropyBounds.LooplessGraph.mem_addForced line 96
  13. theorem OAI.MatchingEntropyBounds.LooplessGraph.mem_addForced_remaining line 109
  14. def OAI.MatchingEntropyBounds.LooplessGraph.removeForced line 116
  15. theorem OAI.MatchingEntropyBounds.LooplessGraph.mem_removeForced line 130
  16. def OAI.MatchingEntropyBounds.LooplessGraph.forcedMatchingEquiv line 135
  17. theorem OAI.MatchingEntropyBounds.LooplessGraph.addForced_injective line 159
  18. theorem OAI.MatchingEntropyBounds.LooplessGraph.remaining_vertex_card line 166
  19. theorem OAI.MatchingEntropyBounds.LooplessGraph.range_addForced line 180
  20. theorem OAI.MatchingEntropyBounds.LooplessGraph.law_support_of_mean_one line 190
  21. theorem OAI.MatchingEntropyBounds.LooplessGraph.forcedLaw_feasible line 204
  22. theorem OAI.MatchingEntropyBounds.LooplessGraph.forced_coordinate_zero line 227
  23. theorem OAI.MatchingEntropyBounds.LooplessGraph.separableLower_forced line 241
  24. theorem OAI.MatchingEntropyBounds.entropy_fiberMass_injective line 256
  25. theorem OAI.MatchingEntropyBounds.LooplessGraph.liftForced_feasible line 277
  26. theorem OAI.MatchingEntropyBounds.LooplessGraph.maxMatchingEntropy_forced_le line 302