segment_subset_Icc — Mathlib

English

If x ≤ y, then the closed convex segment [x -[𝕜] y] is contained in the closed interval Icc x y.

Русский

Если x ≤ y, то замкнутый выпуклый сегмент [x -[𝕜] y] содержится в замкнутом интервале Icc x y.

LaTeX

$$$ x \le y \implies [x -[\mathbb{k}] y] \subseteq \mathrm{Icc}(x,y) $$$

Lean4

theorem segment_subset_Icc (h : x ≤ y) : [x -[𝕜] y] ⊆ Icc x y :=
  by
  rintro z ⟨a, b, ha, hb, hab, rfl⟩
  constructor
  ·
    calc
      x = a • x + b • x := (Convex.combo_self hab _).symm
      _ ≤ a • x + b • y := by gcongr
  ·
    calc
      a • x + b • y ≤ a • y + b • y := by gcongr
      _ = y := Convex.combo_self hab _

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