OAI/Geometry/CAT0Fillings/Currents/WeakMass.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.CAT0Fillings.controls_of_weak_limits line 18
2. lemma OAI.CAT0Fillings.exists_controls_of_bounded_weak_limit line 30
3. lemma OAI.CAT0Fillings.mass_le_of_bounded_weak_limit line 56
4. lemma OAI.CAT0Fillings.BoundedLip.mul line 67
5. lemma OAI.CAT0Fillings.IsMetricCurrent.mass_bound_uniform line 93
6. lemma OAI.CAT0Fillings.IsMetricCurrent.eq_zero_of_mass_eq_zero line 109