OAI/Geometry/RuledCovering/ConvexBases.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.RuledApproximation.IsParallelogram.convex line 14

    Source documentation

    The shape predicate denotes a genuinely compact convex base, not merely four distinguished points or an unbounded affine plane.

    Distinct definitions of this name: OAI/Geometry/CylinderCovering/Convexity/ParallelogramGeometry.lean:69 (different declaration text). Qualify references as OAI.RuledApproximation.IsParallelogram.convex@path.

    lemma IsParallelogram.convex {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E]
    {P : Set E} (hP : IsParallelogram P) : Convex ℝ P := by
…

    Mentions: OAI.RuledApproximation.IsParallelogram

  2. lemma OAI.RuledApproximation.IsTriangle.isCompact line 28
  3. lemma OAI.RuledApproximation.IsTriangle.convex line 43
  4. lemma OAI.RuledApproximation.Cylinder.parallelogram_compact_convex line 55
  5. lemma OAI.RuledApproximation.Cylinder.triangle_compact_convex line 58
  6. lemma OAI.RuledApproximation.IsSquareTile.compact_convex line 61