preimage_smul — Mathlib

English

If s is star-convex at c·x, then the preimage of s under z ↦ c·z is star-convex at x.

Русский

Если s звёздочно выпукло относительно c·x, то предобраз множества s по отображению z ↦ c·z звёздочно выпукл относительно x.

LaTeX

$$$\\text{StarConvex}_{\\mathbb{K}}(c\\cdot x, s) \\Rightarrow \\text{StarConvex}_{\\mathbb{K}}(x, \\{z: c\\cdot z \\in s\\})$$$

Lean4

theorem preimage_smul {c : 𝕜} (hs : StarConvex 𝕜 (c • x) s) : StarConvex 𝕜 x ((fun z => c • z) ⁻¹' s) :=
  hs.linear_preimage (LinearMap.lsmul _ _ c)

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