OAI/Geometry/CAT0Fillings/Currents/WeakClosure.lean
5 declarations, 0 contain sorry, 0 declared as axioms
- lemma
OAI.CAT0Fillings.Foundations.eval_tendsto_of_uniform_modulusline 34 - lemma
OAI.CAT0Fillings.Foundations.metricCurrent_of_bounded_weak_limitline 67 - lemma
OAI.CAT0Fillings.Foundations.boundarySucc_boundarySuccline 124 - lemma
OAI.CAT0Fillings.Foundations.boundarySucc_weak_limitline 139 - lemma
OAI.CAT0Fillings.Foundations.normal_of_bounded_integral_weak_limitline 149