OAI/Geometry/CAT0Fillings/Slices/Approximation.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.CAT0Fillings.BorelCoefficients.borelAction_const_coord line 17
2. def OAI.CAT0Fillings.BorelCoefficients.levelClamp line 24
3. lemma OAI.CAT0Fillings.BorelCoefficients.levelClamp_lipschitz line 28
4. lemma OAI.CAT0Fillings.BorelCoefficients.levelClamp_eq line 33
5. lemma OAI.CAT0Fillings.BorelCoefficients.levelClamp_tendsto line 40
6. lemma OAI.CAT0Fillings.BorelCoefficients.borelAction_eq_levelClamp line 58
7. theorem OAI.CAT0Fillings.BorelCoefficients.borelAction_locality_level line 109
8. theorem OAI.CAT0Fillings.BorelCoefficients.borelAction_congr_coord_on_support line 141
9. def OAI.CAT0Fillings.SliceReconstruction.metricCone line 176
10. lemma OAI.CAT0Fillings.SliceReconstruction.metricCone_lipschitz line 180
11. def OAI.CAT0Fillings.SliceReconstruction.metricConeApprox line 188
12. lemma OAI.CAT0Fillings.SliceReconstruction.metricConeApprox_lipschitz line 192
13. lemma OAI.CAT0Fillings.SliceReconstruction.le_metricConeApprox line 198
14. lemma OAI.CAT0Fillings.SliceReconstruction.metricConeApprox_antitone line 204
15. lemma OAI.CAT0Fillings.SliceReconstruction.metricConeApprox_le_cone line 208
16. lemma OAI.CAT0Fillings.SliceReconstruction.metricConeApprox_tendsto line 215
17. structure OAI.CAT0Fillings.SliceReconstruction.LipLattice line 236
18. lemma OAI.CAT0Fillings.SliceReconstruction.LipLattice.pi_dist line 248
19. lemma OAI.CAT0Fillings.SliceReconstruction.LipLattice.comp_pi line 279