is_linear_image — Mathlib

English

If s is strictly convex, the image of s under a linear map is strictly convex.

Русский

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

LaTeX

$$$StrictConvex 𝕜 s \Rightarrow \forall {f : E \to F}, IsLinearMap 𝕜 f \Rightarrow IsOpenMap f \Rightarrow StrictConvex 𝕜 (Set.image f s)$$$

Lean4

theorem is_linear_image (hs : StrictConvex 𝕜 s) {f : E → F} (h : IsLinearMap 𝕜 f) (hf : IsOpenMap f) :
    StrictConvex 𝕜 (f '' s) :=
  hs.linear_image (h.mk' f) hf

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