OAI/Combinatorics/MatchingPSD/Pairings.lean

GitHub source file

42 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.MatchingSmoothing.Pairing line 8
  2. lemma OAI.MatchingSmoothing.Pairing.ext line 14
  3. lemma OAI.MatchingSmoothing.Pairing.partner_partner line 17
  4. lemma OAI.MatchingSmoothing.Pairing.partner_ne line 19
  5. lemma OAI.MatchingSmoothing.Pairing.partner_eq_iff line 21
  6. def OAI.MatchingSmoothing.Pairing.relabel line 24
  7. lemma OAI.MatchingSmoothing.Pairing.relabel_apply line 34
  8. lemma OAI.MatchingSmoothing.Pairing.relabel_one line 37
  9. lemma OAI.MatchingSmoothing.Pairing.relabel_mul line 39
  10. def OAI.MatchingSmoothing.Pairing.relabelEquiv line 44
  11. def OAI.MatchingSmoothing.Pairing.act line 50
  12. lemma OAI.MatchingSmoothing.Pairing.act_apply line 58
  13. lemma OAI.MatchingSmoothing.Pairing.act_mul line 61
  14. lemma OAI.MatchingSmoothing.Pairing.act_one line 66
  15. lemma OAI.MatchingSmoothing.Pairing.partner_sq line 68
  16. lemma OAI.MatchingSmoothing.Pairing.cycleType_eq line 72
  17. lemma OAI.MatchingSmoothing.Pairing.exists_relabel line 89
  18. lemma OAI.MatchingSmoothing.Pairing.relabel_swap_partner line 96
  19. lemma OAI.MatchingSmoothing.Pairing.exists_internal_edge_compl line 104
  20. lemma OAI.MatchingSmoothing.Pairing.no_sign_on_complement line 115
  21. def OAI.MatchingSmoothing.Pairing.SameInternal line 126
  22. lemma OAI.MatchingSmoothing.Pairing.align_partners line 129
  23. def OAI.MatchingSmoothing.Pairing.restrict line 186
  24. lemma OAI.MatchingSmoothing.Pairing.restrict_apply line 193
  25. def OAI.MatchingSmoothing.Pairing.closure line 197
  26. lemma OAI.MatchingSmoothing.Pairing.mem_closure line 200
  27. lemma OAI.MatchingSmoothing.Pairing.stable_closure line 211
  28. lemma OAI.MatchingSmoothing.Pairing.agree_on_closure line 215
  29. lemma OAI.MatchingSmoothing.Pairing.align_remaining line 224
  30. lemma OAI.MatchingSmoothing.Pairing.exists_relabel_fixing line 267
  31. lemma OAI.MatchingSmoothing.Pairing.extend_swap line 277
  32. lemma OAI.MatchingSmoothing.Pairing.invariant_of_swap_invariant line 289
  33. lemma OAI.MatchingSmoothing.Pairing.sameInternal_value_of_invariant line 320
  34. def OAI.MatchingSmoothing.Pairing.edgeCoord line 329
  35. def OAI.MatchingSmoothing.Pairing.internalPattern line 333
  36. lemma OAI.MatchingSmoothing.Pairing.internalPattern_eq_iff line 337
  37. lemma OAI.MatchingSmoothing.Pairing.internal_indicator_mem_lowDegree line 348
  38. lemma OAI.MatchingSmoothing.Pairing.mem_lowDegree_of_swap_invariant line 369
  39. lemma OAI.MatchingSmoothing.Pairing.exists_perm_fixing_pair line 379
  40. lemma OAI.MatchingSmoothing.Pairing.act_swap_involution line 398
  41. lemma OAI.MatchingSmoothing.Pairing.act_swap_conj line 402
  42. lemma OAI.MatchingSmoothing.Pairing.act_commute_of_swap_fixed line 407