convex_Iio — Mathlib

English

In an ordered module, the open lower set Iio(r) = {w | w < r} is convex.

Русский

В упорядоченном модуле открытое нижнее множество Iio(r) выпукло.

LaTeX

$$$\operatorname{Convex}_\mathbb{K}(\{w\in\beta : w

Lean4

theorem convex_Iio (r : β) : Convex 𝕜 (Iio r) :=
  by
  intro x hx y hy a b ha hb hab
  obtain rfl | ha' := ha.eq_or_lt
  · rw [zero_add] at hab
    rwa [zero_smul, zero_add, hab, one_smul]
  rw [mem_Iio] at hx hy
  calc
    a • x + b • y < a • r + b • r :=
      add_lt_add_of_lt_of_le (smul_lt_smul_of_pos_left hx ha') (smul_le_smul_of_nonneg_left hy.le hb)
    _ = r := Convex.combo_self hab _

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