OAI/Geometry/CylinderCovering/Convexity/OpenParallelogram.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.RuledApproximation.IsParallelogram.exists_openParallelogram_superset line 15
2. theorem OAI.RuledApproximation.IsParallelogram.exists_openParallelogram_superset_exact line 28
3. theorem OAI.RuledApproximation.Cylinder.basePlane_finrank line 45
4. theorem OAI.RuledApproximation.Cylinder.enlarge_openParallelogram line 55
5. theorem OAI.RuledApproximation.finite_enlarge_openParallelogram line 65
6. theorem OAI.RuledApproximation.openParallelogramEnlargement_result line 89