Structures · Analysis
StrictConvexSpace
A strictly convex space is a normed space where the closed balls are strictly convex. We only
require balls of positive radius with center at the origin to be strictly convex in the definition,
then prove that any closed ball is strictly convex in strictConvex_closedBall below.
See also StrictConvexSpace.of_strictConvex_unitClosedBall.
- Shape
- 2 explicit arguments · adds strictConvex_closedBall
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by0
Nothing extends this class yet.
Concrete types that are instances1
- Real
How is a type an instance?
Loading the hierarchy index…
Assumed by51
- strictConvex_closedBall
- eq_of_norm_eq_of_norm_add_eq
- dist_add_dist_eq_iff
- sameRay_iff_norm_add
- combo_mem_ball_of_ne
- norm_add_lt_of_not_sameRay
- Complex.eqOn_of_isPreconnected_of_isMaxOn_norm
- Collinear.wbtw_of_dist_eq_of_dist_le
- Complex.affine_of_mapsTo_ball_of_norm_dslope_eq_div
- Isometry.affineIsometryOfStrictConvexSpace
- Sbtw.dist_lt_max_dist
- lt_norm_sub_of_not_sameRay
- sameRay_iff_norm_sub
- threeAPFree_sphere
- dist_affineCombination_lt_of_strictConvexSpace
- norm_sum_lt_of_strictConvexSpace
- Affine.Simplex.dist_lt_of_mem_closedInterior_of_strictConvexSpace
- ae_eq_const_or_norm_average_lt_of_norm_le_const
- norm_combo_lt_of_ne
- sum_mem_ball_of_strictConvexSpace
- StrictConvexSpace.strictConvex_closedBall
- Complex.eq_of_isMaxOn_of_ball_subset
- not_sameRay_iff_norm_add_lt
- Collinear.sbtw_of_dist_eq_of_dist_lt
- Complex.eq_const_of_exists_max
- Complex.eqOn_closedBall_of_isMaxOn_norm
- eq_lineMap_of_dist_eq_mul_of_dist_eq_mul
- abs_lt_norm_sub_of_not_sameRay
- ae_eq_const_or_norm_integral_lt_of_norm_le_const
- Complex.eventually_eq_of_isLocalMax_norm
- centerMass_mem_ball_of_strictConvexSpace
- Affine.Simplex.dist_lt_of_mem_interior_of_strictConvexSpace
- StrictConvexSpace.extremePoints_closedBall_eq_sphere
- Isometry.coe_affineIsometryOfStrictConvexSpace
- Complex.eq_const_of_exists_le
- not_sameRay_iff_abs_lt_norm_sub
- ae_eq_const_or_norm_setIntegral_lt_of_norm_le_const
- openSegment_subset_ball_of_ne
- norm_midpoint_lt_iff
- LinearIsometry.strictConvexSpace_range
- dist_lt_dist_add_dist_iff
- MDifferentiableOn.eqOn_of_isPreconnected_of_isMaxOn_norm
- eq_midpoint_of_dist_eq_half
- LinearIsometry.strictConvexSpace
- Wbtw.dist_le_max_dist
- Complex.affine_of_mapsTo_ball_of_exists_norm_dslope_eq_div
- Submodule.instStrictConvexSpace
- StrictConvexSpace.sphere_subset_extremePoints_closedBall
- Complex.eqOn_closure_of_isPreconnected_of_isMaxOn_norm
- Isometry.affineIsometryOfStrictConvexSpace_apply
Ancestors0
No ancestors.