is_linear_preimage — Mathlib

English

If s is star-convex at f(x) for some map f, and f is an arbitrary linear map (IsLinearMap), then s preimage under f is star-convex at x.

Русский

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

LaTeX

$$$\text{If } hs: \mathrm{StarConvex}_{\mathbb{K}}(f(x),s) \text{ and } hf: \mathrm{IsLinearMap}_{\mathbb{K}}(f), \text{ then } \mathrm{StarConvex}_{\mathbb{K}}(x, f^{-1}(s)).$$$

Lean4

theorem is_linear_preimage {s : Set F} {f : E → F} (hs : StarConvex 𝕜 (f x) s) (hf : IsLinearMap 𝕜 f) :
    StarConvex 𝕜 x (preimage f s) :=
  hs.linear_preimage <| hf.mk' f

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