uIcc_of_le

Mathlib.Order.Interval.Set.UnorderedInterval

URI: https://scilib.ai/kg/mathlib#Set.uIcc_of_le

English

If a ≤ b, then uIcc(a,b) coincides with Icc(a,b).

Русский

Если a ≤ b, то uIcc(a,b) совпадает с Icc(a,b).

LaTeX

$$$$ \uparrow \text{uIcc}(a,b) = Icc(a,b) \quad \text{если } a \le b. $$$$

Lean4

@[simp]
theorem uIcc_of_le (h : a ≤ b) : [[a, b]] = Icc a b := by rw [uIcc, inf_eq_left.2 h, sup_eq_right.2 h]

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru