Ioi_disjoint_Iio_of_le

Mathlib.Order.Interval.Set.Disjoint

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

English

If a ≤ b, then Disjoint (Ioi b) (Iio a).

Русский

Если a ≤ b, то Ioi(b) и Iio(a) не пересекаются.

LaTeX

$$$$ a \le b \implies Disjoint (Ioi\,b) (Iio\,a). $$$$

Lean4

theorem Ioi_disjoint_Iio_of_le (h : a ≤ b) : Disjoint (Ioi b) (Iio a) :=
  Ioi_disjoint_Iio_of_not_lt (not_lt_of_ge h)

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

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

Разделы

Аффилиация

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