add_smul — Mathlib

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

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