English
If S is convex, then for any nonnegative p,q, the dilation distributes: (p+q)·S = p·S + q·S.
Русский
Если S выпукло, то для неотрицательных p,q выполняется (p+q)·S = p·S + q·S (множество суммы масштабированных копий S).
LaTeX
$$$\operatorname{Convex}_{\mathbb{K}}(S) \Rightarrow (p+q)\,S = p\,S + q\,S\quad (p,q \ge 0).$$$
Lean4
protected theorem add_smul (h_conv : Convex 𝕜 s) {p q : 𝕜} (hp : 0 ≤ p) (hq : 0 ≤ q) : (p + q) • s = p • s + q • s :=
(add_smul_subset _ _ _).antisymm <|
by
rintro _ ⟨_, ⟨v₁, h₁, rfl⟩, _, ⟨v₂, h₂, rfl⟩, rfl⟩
exact h_conv.exists_mem_add_smul_eq h₁ h₂ hp hq