Iio_disjoint_Ioi_of_not_lt

Mathlib.Order.Interval.Set.Disjoint

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

English

Iio and Ioi are disjoint if not a < b, equivalence with the previous identity.

Русский

Iio и Ioi дизjoint, если не выполняется a < b; эквивалентно предыдущему равенству.

LaTeX

$$$$ Iio\,a \cap Ioi\,b = \emptyset \quad\text{если } \neg(a < b). $$$$

Lean4

theorem Iio_disjoint_Ioi_of_not_lt (h : ¬a < b) : Disjoint (Iio b) (Ioi a) :=
  disjoint_comm.mp (Ioi_disjoint_Iio_of_not_lt h)

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

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

Разделы

Аффилиация

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