smul_mem_of_zero_mem — Mathlib

English

From convexity and a point in the set, scaled points stay in the set for t ∈ [0,1].

Русский

Из выпуклости следует, что масштабированные точки остаются в множестве при t ∈ [0,1].

LaTeX

$$$$ t \\cdot x ∈ s \\quad (t ∈ [0,1], x ∈ s) $$$$

Lean4

theorem smul_mem_of_zero_mem (hs : Convex 𝕜 s) {x : E} (zero_mem : (0 : E) ∈ s) (hx : x ∈ s) {t : 𝕜}
    (ht : t ∈ Icc (0 : 𝕜) 1) : t • x ∈ s := by simpa using hs.add_smul_mem zero_mem (by simpa using hx) ht

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