OAI/Geometry/CylinderCovering/Radial/ActualEndpoint.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.CylinderCovering.RadialSweep.raw_direction_ne_zero line 13
2. theorem OAI.CylinderCovering.RadialSweep.actual_direction_unit line 21
3. theorem OAI.CylinderCovering.RadialSweep.sweep_compact line 27
4. theorem OAI.CylinderCovering.RadialSweep.localSweep_compact line 32
5. theorem OAI.CylinderCovering.RadialSweep.iUnion_localSweep line 41
6. theorem OAI.CylinderCovering.RadialSweep.actualBase_compact line 54
7. theorem OAI.CylinderCovering.RadialSweep.actualBase_covers line 58
8. theorem OAI.CylinderCovering.RadialSweep.actualSweepStatement_of_aligned line 66
9. theorem OAI.CylinderCovering.RadialSweep.actualBase_subset_frozenBase line 111
10. theorem OAI.CylinderCovering.RadialSweep.actual_radial_sweep line 126