segment_subset_uIcc — Mathlib

English

The segment [x -[𝕜] y] is contained in the semi-closed interval uIcc x y, and equality holds when x ≤ y or y ≤ x via symmetry.

Русский

Сегмент [x -[𝕜] y] содержится в полусуженном интервале uIcc x y; равенство выполняется при x ≤ y или y ≤ x через симметрию.

LaTeX

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

Lean4

theorem segment_subset_uIcc (x y : E) : [x -[𝕜] y] ⊆ uIcc x y :=
  by
  rcases le_total x y with h | h
  · rw [uIcc_of_le h]
    exact segment_subset_Icc h
  · rw [uIcc_of_ge h, segment_symm]
    exact segment_subset_Icc h

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