strictConvexSpace_range — Mathlib

English

If E is strictly convex, then its range under a linear isometry is strictly convex as well (as an instance).

Русский

Если пространство E строго выпукло, то образ линейной изометрии также строго выпукл.

LaTeX

$$$[StrictConvexSpace_{\\mathbb{K}}(E)] \\Rightarrow [StrictConvexSpace_{\\mathbb{K}}(\\operatorname{LinearMap.range} e)].$$$

Lean4

instance strictConvexSpace_range [StrictConvexSpace 𝕜 E] (e : E →ₗᵢ[𝕜] F) : StrictConvexSpace 𝕜 (LinearMap.range e) :=
  e.strictConvexSpace_range_iff.mpr ‹_›

Похожие утверждения