OAI/Geometry/CAT0Fillings/Reconstruction/LipschitzPieces.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.CAT0Fillings.JointBV.measurable_real_closedBall line 15
2. def OAI.CAT0Fillings.JointBV.DensityPiece line 21
3. lemma OAI.CAT0Fillings.JointBV.measurableSet_densityPiece line 25
4. lemma OAI.CAT0Fillings.JointBV.ae_mem_iUnion_densityPiece line 37
5. lemma OAI.CAT0Fillings.JointBV.measure_ball_bound_of_densityPiece line 60
6. lemma OAI.CAT0Fillings.JointBV.localMeanBound_of_densityPiece line 79
7. lemma OAI.CAT0Fillings.JointBV.exists_compact_cover_ae line 108
8. theorem OAI.CAT0Fillings.JointBV.common_compact_lipschitz_pieces line 128