convex_Iic — Mathlib

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 _

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