OAI/Geometry/CylinderCovering/Convexity/CompactOuterConvergence.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.CylinderCovering.CompactOuterConvergence.cthickening_excess_tendsto line 16
2. theorem OAI.CylinderCovering.CompactOuterConvergence.excess_tendsto_of_eventually_subset_cthickening line 25
3. theorem OAI.CylinderCovering.CompactOuterConvergence.real_excess_tendsto_of_eventually_subset_cthickening line 36
4. theorem OAI.CylinderCovering.CompactOuterConvergence.linear_mesh_real_excess_tendsto line 45