OAI/Geometry/CylinderCovering/Radial/PairedActual.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.CylinderCovering.RadialPairedSweep.upperData_localSweep line 16
2. lemma OAI.CylinderCovering.RadialPairedSweep.lowerData_localSweep line 32
3. lemma OAI.CylinderCovering.RadialPairedSweep.upperData_actualBase line 48
4. lemma OAI.CylinderCovering.RadialPairedSweep.lowerData_actualBase line 54
5. lemma OAI.CylinderCovering.RadialPairedSweep.pairedActualCost_eq line 60
6. lemma OAI.CylinderCovering.RadialPairedSweep.upperLocalSweep_subset_frozenCylinder line 67
7. lemma OAI.CylinderCovering.RadialPairedSweep.lowerLocalSweep_subset_frozenCylinder line 74
8. lemma OAI.CylinderCovering.RadialPairedSweep.upperActualBase_subset_frozenBase line 81
9. lemma OAI.CylinderCovering.RadialPairedSweep.lowerActualBase_subset_frozenBase line 88
10. lemma OAI.CylinderCovering.RadialPairedSweep.pairedActualCost_nonneg line 95
11. theorem OAI.CylinderCovering.RadialPairedSweep.paired_actual_sweeps line 101