OAI/Geometry/CAT0Fillings/Scaling/Metric.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.CAT0Fillings.power_mul_dimension line 13
2. lemma OAI.CAT0Fillings.fillingPower_gt_one line 16
3. lemma OAI.CAT0Fillings.normalized_scale line 19
4. def OAI.CAT0Fillings.ScaledSpace line 62
5. instance OAI.CAT0Fillings.ScaledSpace.(instance at line 65) line 65
6. instance OAI.CAT0Fillings.ScaledSpace.(instance at line 66) line 66
7. def OAI.CAT0Fillings.ScaledSpace.toBase line 67
8. def OAI.CAT0Fillings.ScaledSpace.ofBase line 68
9. lemma OAI.CAT0Fillings.ScaledSpace.to_of line 70
10. lemma OAI.CAT0Fillings.ScaledSpace.of_to line 72
11. instance OAI.CAT0Fillings.ScaledSpace.(instance at line 73) line 73
12. instance OAI.CAT0Fillings.ScaledSpace.(instance at line 101) line 101
13. instance OAI.CAT0Fillings.ScaledSpace.(instance at line 102) line 102
14. instance OAI.CAT0Fillings.ScaledSpace.(instance at line 103) line 103
15. lemma OAI.CAT0Fillings.ScaledSpace.dist_eq line 104
16. lemma OAI.CAT0Fillings.ScaledSpace.up_lipschitz line 105
17. lemma OAI.CAT0Fillings.ScaledSpace.down_lipschitz line 109
18. lemma OAI.CAT0Fillings.ScaledSpace.isCAT0 line 116