OAI/Geometry/CylinderCovering/Radial/Regularity.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.CylinderCovering.RadialSweep.velocity_derivWithin line 10
2. theorem OAI.CylinderCovering.RadialSweep.velocity_contDiffOn line 14
3. theorem OAI.CylinderCovering.RadialSweep.velocity_hasDerivAt line 22
4. theorem OAI.CylinderCovering.RadialSweep.velocity_contDiffOn_interior line 26
5. theorem OAI.RadialNilpotent.isOpen_radialSector line 36
6. theorem OAI.RadialNilpotent.positive_radial_parameters_unique line 59