Iio_disjoint_Ioi_of_le

Mathlib.Order.Interval.Set.Disjoint

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

English

Iio and Ioi are disjoint when a ≤ b implies the symmetric version.

Русский

Iio и Ioi дизjoint, если a ≤ b, соответствующая симметричная формула верна.

LaTeX

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

Lean4

theorem Iio_disjoint_Ioi_of_le (h : a ≤ b) : Disjoint (Iio a) (Ioi b) :=
  disjoint_comm.mp (Ioi_disjoint_Iio_of_le h)

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

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

Разделы

Аффилиация

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