OAI/Geometry/CylinderCovering/Radial/FinitePair.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.CylinderCovering.RadialPairedSweep.join_upper line 10
2. lemma OAI.CylinderCovering.RadialPairedSweep.join_lower line 15
3. lemma OAI.CylinderCovering.RadialPairedSweep.join_totalArea line 20
4. lemma OAI.CylinderCovering.RadialPairedSweep.join_covers_union line 31
5. lemma OAI.CylinderCovering.RadialPairedSweep.join_totalArea_tendsto line 43
6. lemma OAI.CylinderCovering.RadialPairedSweep.upperSweep_mono line 50
7. lemma OAI.CylinderCovering.RadialPairedSweep.lowerSweep_mono line 56
8. lemma OAI.CylinderCovering.RadialPairedSweep.eventually_strict_finite_cost line 62