OAI/Geometry/CylinderCovering/Convexity/LevelCrossing.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.CylinderCovering.LevelCrossing.nonneg_of_left_minimum line 10
2. theorem OAI.CylinderCovering.LevelCrossing.nonneg_of_right_maximum line 22
3. theorem OAI.CylinderCovering.LevelCrossing.first_level_on_Icc line 34
4. theorem OAI.CylinderCovering.LevelCrossing.exists_level_nonneg_derivative line 65
5. theorem OAI.CylinderCovering.LevelCrossing.exists_level_nonneg_derivWithin line 88
6. theorem OAI.CylinderCovering.LevelCrossing.c1_level_crossing line 95