zero_smul — Mathlib

English

If StarConvex 𝕜 0 s, then StarConvex 𝕜 0 (c•s) for any scalar c.

Русский

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

LaTeX

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

Lean4

theorem zero_smul (hs : StarConvex 𝕜 0 s) (c : 𝕜) : StarConvex 𝕜 0 (c • s) := by simpa using hs.smul c

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