Ioi_disjoint_Iio_of_not_lt

Mathlib.Order.Interval.Set.Disjoint

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

English

If not a < b, then Disjoint (Ioi a) (Iio b).

Русский

Если не выполняется a < b, то Ioi(a) и Iio(b) дизjoint.

LaTeX

$$$$ \neg(a < b) \implies Disjoint (Ioi a) (Iio b). $$$$

Lean4

theorem Ioi_disjoint_Iio_of_not_lt (h : ¬a < b) : Disjoint (Ioi a) (Iio b) :=
  disjoint_left.mpr fun _ hx hy ↦ h (hx.trans hy)

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

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

Разделы

Аффилиация

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