English
In a ordered module, the set {x ∈ β | x ≤ r} is convex for any r ∈ β.
Русский
В упорядоченном модуле множество {x ∈ β | x ≤ r} выпукло для любого $r$.
LaTeX
$$$\operatorname{Convex}_\mathbb{K}(\{x \in \beta : x \le r\})$$$
Lean4
theorem convex_Iic (r : β) : Convex 𝕜 (Iic r) := fun x hx y hy a b ha hb hab =>
calc
a • x + b • y ≤ a • r + b • r := add_le_add (smul_le_smul_of_nonneg_left hx ha) (smul_le_smul_of_nonneg_left hy hb)
_ = r := Convex.combo_self hab _