OAI/Geometry/CylinderCovering/Convexity/ParallelogramGeometry.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.RuledApproximation.parallelogram_coordinate_homeomorph line 13
  2. theorem OAI.RuledApproximation.parallelogram_coordinate_image line 24
  3. theorem OAI.RuledApproximation.parallelogram_interior line 40
  4. theorem OAI.RuledApproximation.IsParallelogram.compact line 56
  5. theorem OAI.RuledApproximation.IsParallelogram.convex line 69

    Distinct definitions of this name: OAI/Geometry/RuledCovering/ConvexBases.lean:14 (different declaration text). Qualify references as OAI.RuledApproximation.IsParallelogram.convex@path.

  6. theorem OAI.RuledApproximation.IsParallelogram.interior_nonempty line 82
  7. theorem OAI.RuledApproximation.IsParallelogram.isOpenParallelogram_interior line 89
  8. theorem OAI.RuledApproximation.IsParallelogram.homothety line 94