OAI/Geometry/CylinderCovering/Convexity/FinitePlaneHausdorff.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.CylinderCovering.FinitePlaneHausdorff.compact_subset_isometry_range_measure_lt_top line 18
2. theorem OAI.CylinderCovering.FinitePlaneHausdorff.compact_subset_affine_plane_measure_lt_top line 29
3. theorem OAI.CylinderCovering.FinitePlaneHausdorff.orthogonal_unit_finrank line 42
4. theorem OAI.CylinderCovering.FinitePlaneHausdorff.compact_affine_hyperplane_measure_lt_top line 49
5. theorem OAI.CylinderCovering.FinitePlaneHausdorff.compact_perpendicular_measure_lt_top line 59