OAI/Combinatorics/MatchingPSD/TableGeometry.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.MatchingSmoothing.predicateAverage_fiberEquiv line 11
2. lemma OAI.MatchingSmoothing.coordinates_eq_of_cross_eq line 19
3. lemma OAI.MatchingSmoothing.table_eq_iff_cross line 42
4. lemma OAI.MatchingSmoothing.crossVector_transport line 64
5. lemma OAI.MatchingSmoothing.histogram_comp_equiv line 70