OAI/Analysis/SphereIsometry/ConvexDiameter.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Tingley.DiameterLE.convexHull line 16

   Source documentation

   Taking a convex hull preserves a pairwise diameter bound.

   theorem DiameterLE.convexHull {A : Set E} {δ : ℝ} (h : DiameterLE A δ) :
       DiameterLE (convexHull ℝ A) δ := by
   …

   Mentions: OAI.Tingley.DiameterLE

2. theorem OAI.Tingley.norm_le_of_mem_convexHull line 23

   Source documentation

   A norm bound on a set also holds on its convex hull.

   theorem norm_le_of_mem_convexHull {A : Set E} {R : ℝ}
       (hR : ∀ x ∈ A, ‖x‖ ≤ R) {x : E} (hx : x ∈ convexHull ℝ A) : ‖x‖ ≤ R := by
   …