OAI/Geometry/CylinderCovering/Rational/Inversion.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SlopeRational.inverseRectangle_eq_box line 11
2. lemma OAI.SlopeRational.inverseRectangle_isClosed line 17
3. lemma OAI.SlopeRational.inverseRectangle_isCompact line 24
4. lemma OAI.SlopeRational.inverseRectangle_convex line 44
5. lemma OAI.SlopeRational.inverseRectangle_denominator_pos line 54
6. lemma OAI.SlopeRational.field_contDiffOn_inverseRectangle line 60
7. lemma OAI.SlopeRational.rectangleInversion_of_contDiff line 77
8. theorem OAI.SlopeRational.rectangleInversion_main line 144