Theorems · Theorem · functional analysis
strictConvex_closedBall
∀ (𝕜 : Type u_1) {E : Type u_2} [inst : NormedField 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : NormedAddCommGroup E]
[inst_3 : NormedSpace 𝕜 E] [StrictConvexSpace 𝕜 E] (x : E) (r : ℝ), StrictConvex 𝕜 (Metric.closedBall x r)A closed ball in a strictly convex space is strictly convex.
- Cited by
- 8 results in Mathlib
- Foundations
- Depth 163 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites15
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Setproof · cited by 53,352
- Realstatement and proof · cited by 25,697
- NormedAddCommGroupstatement and proof · cited by 15,752
- NormedSpacestatement and proof · cited by 12,499
- PartialOrderstatement and proof · cited by 6,410
- NormedFieldstatement and proof · cited by 1,084
- Metric.closedBallstatement · cited by 704
- le_or_gtproof · cited by 269
- StrictConvexstatement and proof · cited by 71
- StrictConvexSpacestatement and proof · cited by 57
- vadd_closedBall_zeroproof · cited by 4
- Metric.subsingleton_closedBallproof · cited by 3
Cited by8
Results whose statement or proof uses this declaration.
- combo_mem_ball_of_neproof · cited by 3
- centerMass_mem_ball_of_strictConvexSpaceproof · cited by 1
- StrictConvexSpace.extremePoints_closedBall_eq_sphereproof · cited by 1
- EuclideanGeometry.Sphere.dist_center_lt_radius_of_sbtwproof · cited by 1
- ae_eq_const_or_norm_average_lt_of_norm_le_constproof · cited by 1
- threeAPFree_sphereproof · cited by 1
- StrictConvexSpace.sphere_subset_extremePoints_closedBallproof · cited by 0
- LinearIsometry.strictConvexSpaceproof · cited by 0