OAI/Geometry/IntegralFillings/Slicing/CoordinateCoarea.lean
6 declarations, 0 contain sorry, 0 declared as axioms
- lemma
OAI.SharpIntegralFillings.IntegerChart.majorant_test_boundline 40 - lemma
OAI.SharpIntegralFillings.IntegerChart.ae_integrable_coordinateline 76 - lemma
OAI.SharpIntegralFillings.IntegerChart.ae_coordinate_of_aeline 88 - theorem
OAI.SharpIntegralFillings.IntegerChart.coordinate_coarea_majorantline 105 - theorem
OAI.SharpIntegralFillings.IntegerChart.sharp_coordinate_coarea_majorantline 173 - lemma
OAI.SharpIntegralFillings.BorelCoefficients.integrable_boundedLipline 252