uIoo_of_ge

Mathlib.Order.Interval.Set.UnorderedInterval

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

English

If b ≤ a, then uIoo(a, b) = Ioo(b, a).

Русский

Если b ≤ a, то uIoo(a, b) = Ioo(b, a).

LaTeX

$$$ b \le a \Longrightarrow uIoo(a,b) = Ioo(b,a) $$$

Lean4

@[simp]
theorem uIoo_of_ge (h : b ≤ a) : uIoo a b = Ioo b a := by rw [uIoo, inf_eq_right.2 h, sup_eq_left.2 h]

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

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

Разделы

Аффилиация

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