strictConvex_image — Mathlib

English

Strict convexity is preserved by linear isometries: for any linear isometry e, a set S has strict convexity if and only if its image e[S] does, i.e., S is strictly convex iff e[S] is strictly convex.

Русский

Строгоя выпуклость сохраняется под линейной изометрией: для отображения e имеем эквивалентность: S строго выпукло тогда и только тогда, когда e[S] строго выпукло.

LaTeX

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

Lean4

@[simp]
theorem strictConvex_image {s : Set E} (e : E ≃ₗᵢ[𝕜] F) : StrictConvex 𝕜 (e '' s) ↔ StrictConvex 𝕜 s :=
  e.toContinuousLinearEquiv.strictConvex_image

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