strictConvex_image — Mathlib

English

For a linear isomorphism e, a set s has strict convexity if and only if its image under e is strictly convex: StrictConvex 𝕜 (e '' s) ↔ StrictConvex 𝕜 s.

Русский

Пусть e — линейное эквивалентное отображение; множество сохраняет строгую выпуклость по изображению: StrictConvex 𝕜 (e'' s) ⇔ StrictConvex 𝕜 s.

LaTeX

$$$$\\text{StrictConvex}_{\\mathbb{K}}(e'' s) \\iff \\text{StrictConvex}_{\\mathbb{K}}(s).$$$$

Lean4

@[simp]
theorem strictConvex_image {s : Set E} (e : E ≃L[𝕜] F) : StrictConvex 𝕜 (e '' s) ↔ StrictConvex 𝕜 s := by
  rw [e.image_eq_preimage, e.symm.strictConvex_preimage]

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