is_linear_image — Mathlib

English

If hs is star-convex at x with respect to a set s and f is linear, then the image of s under f is star-convex at f(x).

Русский

Если s звездообразно относительно x, и f линейно, то образ s под действием f звездообразен относительно f(x).

LaTeX

$$$$StarConvex_{\mathbb{K}}(x,s) \Rightarrow StarConvex_{\mathbb{K}}(f(x), f''s).$$$$

Lean4

theorem is_linear_image (hs : StarConvex 𝕜 x s) {f : E → F} (hf : IsLinearMap 𝕜 f) : StarConvex 𝕜 (f x) (f '' s) :=
  hs.linear_image <| hf.mk' f

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