OAI/Geometry/IntegralFillings/Charts/ExtensionsLimit.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SharpIntegralFillings.lipschitzOn_limit line 28
2. lemma OAI.SharpIntegralFillings.uniform_limit_on_totallyBounded line 37
3. def OAI.SharpIntegralFillings.mcShane line 66
4. lemma OAI.SharpIntegralFillings.mcShane_bddBelow line 69
5. lemma OAI.SharpIntegralFillings.mcShane_eqOn line 81
6. lemma OAI.SharpIntegralFillings.mcShane_lipschitz line 89
7. lemma OAI.SharpIntegralFillings.mcShane_dist_le line 104
8. lemma OAI.SharpIntegralFillings.exists_convergent_lipschitz_extensions line 122