segment_eq_Icc — Mathlib

English

For x ≤ y, the segment [x -[𝕜] y] equals Icc x y; for the reverse order, symmetry gives the same equality with min/max.

Русский

При x ≤ y сегмент [x -[𝕜] y] равен Icc x y; в обратном порядке через симметрию получаем то же равенство с min и max.

LaTeX

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

Lean4

@[simp]
theorem segment_eq_Icc (h : x ≤ y) : [x -[𝕜] y] = Icc x y :=
  (segment_subset_Icc h).antisymm Icc_subset_segment

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