openSegment_eq_Ioo' — Mathlib

English

The segment [x -[𝕜] y] equals uIcc x y for all x,y.

Русский

Сегмент [x -[𝕜] y] равен uIcc x y для любых x,y.

LaTeX

$$$ [x -[\mathbb{k}] y] = uIcc(x,y) $$$

Lean4

theorem openSegment_eq_Ioo' (hxy : x ≠ y) : openSegment 𝕜 x y = Ioo (min x y) (max x y) :=
  by
  rcases hxy.lt_or_gt with h | h
  · rw [openSegment_eq_Ioo h, max_eq_right h.le, min_eq_left h.le]
  · rw [openSegment_symm, openSegment_eq_Ioo h, max_eq_left h.le, min_eq_right h.le]

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