OAI/Geometry/IntegralFillings/Currents/WeakCompactness.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SharpIntegralFillings.Foundations.exists_weak_cluster_of_mass_bound line 33
2. lemma OAI.SharpIntegralFillings.Foundations.exists_normal_weak_cluster_of_integral_mass_bound line 63
3. lemma OAI.SharpIntegralFillings.Foundations.IsMetricCurrent.first_difference_bound line 83
4. abbrev OAI.SharpIntegralFillings.Foundations.TestClass line 95
5. instance OAI.SharpIntegralFillings.Foundations.testClass_nonempty line 99
6. def OAI.SharpIntegralFillings.Foundations.TestClass.eval line 106
7. lemma OAI.SharpIntegralFillings.Foundations.TestClass.boundedLip line 110
8. lemma OAI.SharpIntegralFillings.Foundations.IntegerRectifiable.testClass_lipschitz line 114
9. lemma OAI.SharpIntegralFillings.Foundations.admissible_mem_testClass line 160