English
Let S be a convex subset of a vector space E over a field 𝕜. If 0 ∈ S and x ∈ S and t ∈ 𝕜 satisfies 1 ≤ t, then x ∈ t · S, i.e., x is a t-scalar multiple of some element of S.
Русский
Пусть S — выпуклое подмножество векторного пространства E над полем 𝕜. Если 0 ∈ S и x ∈ S и t ∈ 𝕜 удовлетворяет 1 ≤ t, то x ∈ t · S, то есть x является произведением t на некоторый элемент S.
LaTeX
$$$\forall S \subset E,\ \operatorname{Convex}_{\mathbb{K}}(S) \wedge 0 \in S \wedge x \in S \wedge 1 \le t \Rightarrow x \in t\,S,$$$
Lean4
theorem mem_smul_of_zero_mem (h : Convex 𝕜 s) {x : E} (zero_mem : (0 : E) ∈ s) (hx : x ∈ s) {t : 𝕜} (ht : 1 ≤ t) :
x ∈ t • s := by
rw [mem_smul_set_iff_inv_smul_mem₀ (zero_lt_one.trans_le ht).ne']
exact h.smul_mem_of_zero_mem zero_mem hx ⟨inv_nonneg.2 (zero_le_one.trans ht), inv_le_one_of_one_le₀ ht⟩
