smul — Mathlib

English

If a set s is star-convex at x with respect to 𝕜, then the scaled set c•s is star-convex at c•x.

Русский

Если множество s звёздочно выпукло относительно точки x, то умноженная на скаляр множество c•s звёздочно выпукло относительно c•x.

LaTeX

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

Lean4

theorem smul (hs : StarConvex 𝕜 x s) (c : 𝕜) : StarConvex 𝕜 (c • x) (c • s) :=
  hs.linear_image <| LinearMap.lsmul _ _ c

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