strictConvexSpace_iff — Mathlib

English

Two spaces E and F connected by a linear isometry are strictly convex spaces in tandem: StrictConvexSpace 𝕜 E holds iff StrictConvexSpace 𝕜 F holds.

Русский

Две пространства, связанные линейной изометрией, либо оба являются строго выпуклыми пространствами, либо нет.

LaTeX

$$$\\text{StrictConvexSpace}_{\\mathbb{K}}(E) \\iff \\text{StrictConvexSpace}_{\\mathbb{K}}(F)$, given a linear isometry $e:E\\to F$.$$

Lean4

protected theorem strictConvexSpace_iff (e : E ≃ₗᵢ[𝕜] F) : StrictConvexSpace 𝕜 E ↔ StrictConvexSpace 𝕜 F := by
  simp only [strictConvexSpace_iff, ← map_zero e, ← e.image_closedBall, e.strictConvex_image]

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