OAI/Geometry/CAT0Fillings/Charts/ExtensionsLimit.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

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