OAI/Combinatorics/MatchingPSD/MatchingFibers.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MatchingSmoothing.Pairing.transport line 11
  2. lemma OAI.MatchingSmoothing.Pairing.transport_apply line 20
  3. lemma OAI.MatchingSmoothing.Pairing.transport_refl line 23
  4. lemma OAI.MatchingSmoothing.Pairing.transport_trans line 27
  5. lemma OAI.MatchingSmoothing.Pairing.transport_symm line 32
  6. def OAI.MatchingSmoothing.Pairing.transportEquiv line 37
  7. lemma OAI.MatchingSmoothing.Pairing.transport_perm line 43
  8. def OAI.MatchingSmoothing.Pairing.sum line 45
  9. lemma OAI.MatchingSmoothing.Pairing.sum_inl line 55
  10. lemma OAI.MatchingSmoothing.Pairing.sum_inr line 57
  11. lemma OAI.MatchingSmoothing.Pairing.sum_relabel_left line 60
  12. lemma OAI.MatchingSmoothing.Pairing.transport_relabel line 65
  13. def OAI.MatchingSmoothing.Pairing.cellwise line 72
  14. lemma OAI.MatchingSmoothing.Pairing.cellwise_apply line 82
  15. lemma OAI.MatchingSmoothing.tableCoordinate_transport line 91
  16. lemma OAI.MatchingSmoothing.tableCoordinate_sum line 97
  17. lemma OAI.MatchingSmoothing.tableCoordinate_nonneg line 105
  18. lemma OAI.MatchingSmoothing.tableCoordinate_eq_zero_iff line 110
  19. lemma OAI.MatchingSmoothing.tableCoordinate_constant line 116
  20. lemma OAI.MatchingSmoothing.Pairing.sum_injective line 128
  21. lemma OAI.MatchingSmoothing.Pairing.exists_sum line 136
  22. def OAI.MatchingSmoothing.Pairing.sumFiberEquiv line 168