openSegment_subset_Ioo — Mathlib

English

If x < y, then openSegment 𝕜 x y is contained in Ioo x y.

Русский

Если x < y, то открытый сегмент 𝕜 x y содержится в Ioo x y.

LaTeX

$$$ x < y \implies openSegment_{\mathbb{k}}(x,y) \subseteq \mathrm{Ioo}(x,y) $$$

Lean4

theorem openSegment_subset_Ioo (h : x < y) : openSegment 𝕜 x y ⊆ Ioo 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 _

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