smul_mem — Mathlib

English

If a set s is star-convex at x, then for any c, the set c•s is star-convex at c•x.

Русский

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

LaTeX

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

Lean4

theorem smul_mem (hs : StarConvex 𝕜 0 s) (hx : x ∈ s) {t : 𝕜} (ht₀ : 0 ≤ t) (ht₁ : t ≤ 1) : t • x ∈ s := by
  simpa using hs.add_smul_mem (by simpa using hx) ht₀ ht₁

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