uIoo_of_not_le

Mathlib.Order.Interval.Set.UnorderedInterval

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

English

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

Русский

Если не выполняется a ≤ b, то uIoo(a,b) = Ioo(b,a).

LaTeX

$$$ \neg(a \le b) \Rightarrow uIoo(a,b) = Ioo(b,a) $$$

Lean4

theorem uIoo_of_not_le (h : ¬a ≤ b) : uIoo a b = Ioo b a :=
  uIoo_of_gt <| lt_of_not_ge h

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

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

Разделы

Аффилиация

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