uIoo_subset_uIcc — Mathlib

English

The unordered open interval lies inside the unordered closed interval with the same endpoints.

Русский

Неупорядоченный открытый интервал вложен в неупорядоченный закрытый интервал с теми же концами.

LaTeX

$$$ uIoo(a,b) \subseteq uIcc(a,b) $$$

Lean4

theorem uIoo_subset_uIcc {α : Type*} [LinearOrder α] (a : α) (b : α) : uIoo a b ⊆ uIcc a b := by
  simp [uIoo, uIcc, Ioo_subset_Icc_self]

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