OAI/Combinatorics/MatchingEntropy/Contraction.lean

GitHub source file

36 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MatchingEntropyBounds.LooplessGraph.onSide line 16
  2. theorem OAI.MatchingEntropyBounds.LooplessGraph.onSide_incident_some line 32
  3. theorem OAI.MatchingEntropyBounds.LooplessGraph.onSide_incident_none line 53
  4. def OAI.MatchingEntropyBounds.LooplessGraph.boundaryEdge line 61
  5. theorem OAI.MatchingEntropyBounds.LooplessGraph.boundaryEdge_mem line 65
  6. theorem OAI.MatchingEntropyBounds.LooplessGraph.boundaryEdge_crosses line 70
  7. theorem OAI.MatchingEntropyBounds.LooplessGraph.eq_boundaryEdge line 75
  8. def OAI.MatchingEntropyBounds.LooplessGraph.liftedEdges line 80
  9. theorem OAI.MatchingEntropyBounds.LooplessGraph.mem_liftedEdges line 84
  10. theorem OAI.MatchingEntropyBounds.LooplessGraph.liftedEdges_keep line 96
  11. theorem OAI.MatchingEntropyBounds.LooplessGraph.lifted_cross_eq_boundary line 103
  12. theorem OAI.MatchingEntropyBounds.LooplessGraph.boundary_mem_lifted line 110
  13. theorem OAI.MatchingEntropyBounds.LooplessGraph.crosses_of_kept_both line 115
  14. theorem OAI.MatchingEntropyBounds.LooplessGraph.lifted_other_subset line 124
  15. theorem OAI.MatchingEntropyBounds.LooplessGraph.mem_glued_left line 136
  16. theorem OAI.MatchingEntropyBounds.LooplessGraph.mem_glued_right line 150
  17. theorem OAI.MatchingEntropyBounds.LooplessGraph.glued_perfect line 168
  18. def OAI.MatchingEntropyBounds.LooplessGraph.glueMatching line 198
  19. theorem OAI.MatchingEntropyBounds.LooplessGraph.indicator_glue_left line 205
  20. theorem OAI.MatchingEntropyBounds.LooplessGraph.indicator_glue_right line 213
  21. theorem OAI.MatchingEntropyBounds.LooplessGraph.boundary_eq_iff_mem line 221
  22. theorem OAI.MatchingEntropyBounds.LooplessGraph.boundary_fiber line 232
  23. theorem OAI.MatchingEntropyBounds.LooplessGraph.boundary_fiber_zero line 243
  24. theorem OAI.MatchingEntropyBounds.LooplessGraph.couple_laws line 253
  25. def OAI.MatchingEntropyBounds.LooplessGraph.sideMap line 292
  26. def OAI.MatchingEntropyBounds.LooplessGraph.liftVertices line 295
  27. theorem OAI.MatchingEntropyBounds.LooplessGraph.mem_liftVertices line 298
  28. theorem OAI.MatchingEntropyBounds.LooplessGraph.sideMap_some line 303
  29. theorem OAI.MatchingEntropyBounds.LooplessGraph.liftVertices_card line 307
  30. theorem OAI.MatchingEntropyBounds.LooplessGraph.onSide_cut_crosses line 331
  31. theorem OAI.MatchingEntropyBounds.LooplessGraph.crosses_lift_kept line 338
  32. theorem OAI.MatchingEntropyBounds.LooplessGraph.onSide_cutMass line 347
  33. theorem OAI.MatchingEntropyBounds.LooplessGraph.onSide_degree_some line 357
  34. theorem OAI.MatchingEntropyBounds.LooplessGraph.onSide_degree_none line 371
  35. theorem OAI.MatchingEntropyBounds.LooplessGraph.odd_compl_of_even line 383
  36. theorem OAI.MatchingEntropyBounds.LooplessGraph.restriction_mem_constraints line 394