uIcc_of_ge

Mathlib.Order.Interval.Set.UnorderedInterval

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

English

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

Русский

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

LaTeX

$$$$ \,[\!a,b\!] = Icc(b,a) \quad \text{если } b \le a. $$$$

Lean4

@[simp]
theorem uIcc_of_ge (h : b ≤ a) : [[a, b]] = Icc b a := by rw [uIcc, inf_eq_right.2 h, sup_eq_left.2 h]

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

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

Разделы

Аффилиация

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