OAI/Geometry/IntegralFillings/Currents/MassBounds.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SharpIntegralFillings.IsMetricCurrent.mass_bound line 16
2. def OAI.SharpIntegralFillings.BoundedLip.toBoundedContinuous line 54
3. lemma OAI.SharpIntegralFillings.continuous_integral_abs_boundedLip line 66
4. lemma OAI.SharpIntegralFillings.isClosed_controls line 80
5. lemma OAI.SharpIntegralFillings.IsMetricCurrent.exists_controls_mass_eq line 93