OAI/Geometry/CAT0Fillings/Currents/ControlledSum.lean
3 declarations, 0 contain sorry, 0 declared as axioms
- lemma
OAI.CAT0Fillings.IsMetricCurrent.control_bound_uniformline 34 - lemma
OAI.CAT0Fillings.summable_controlled_actionsline 49 - lemma
OAI.CAT0Fillings.isMetricCurrent_tsum_controlledline 62