OAI/Geometry/CylinderCovering/Rational/Product.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.SlopeRational.open_cover_reflection line 13
2. theorem OAI.SlopeRational.product_finite_sweeps_separate line 27
3. theorem OAI.SlopeRational.product_finite_sweeps line 50
4. theorem OAI.SlopeRational.product_strict_cover_of_coverage_cost line 58
5. theorem OAI.SlopeRational.product_fractional_eventually line 83
6. theorem OAI.SlopeRational.product_approximation line 101
7. theorem OAI.SlopeRational.product_fractional line 105
8. theorem OAI.SlopeRational.product_realization line 110