linearIsometry_preimage — Mathlib

English

A strict convexity property is preserved by preimages under linear isometries: if S is strictly convex, then its preimage under a linear isometry is strictly convex, and conversely.

Русский

Строгоя выпуклость сохраняется при прообразе по линейной изометрии: если S строго выпукло, то его прообраз строго выпукл; наоборот.

LaTeX

$$$\\text{StrictConvex}_{\\mathbb{K}}(S) \\iff \\text{StrictConvex}_{\\mathbb{K}}(e^{-1}[S])$ для линейной изометрии $e$.$$

Lean4

theorem linearIsometry_preimage [NormedAddCommGroup E] [NormedSpace 𝕜 E] [SeminormedAddCommGroup F] [NormedSpace 𝕜 F]
    {s : Set F} (hs : StrictConvex 𝕜 s) (e : E →ₗᵢ[𝕜] F) : StrictConvex 𝕜 (e ⁻¹' s) :=
  hs.linear_preimage _ e.continuous e.injective

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