Iio_disjoint_Ici

Mathlib.Order.Interval.Set.Disjoint

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

English

If a ≤ b, then the closed upper? lower? interval Iio(a) and the closed lower? Ici(b) are disjoint.

Русский

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

LaTeX

$$$$ a \le b \implies (Iio\,a) \cap (Ici\,b) = \emptyset. $$$$

Lean4

@[simp]
theorem Iio_disjoint_Ici (h : a ≤ b) : Disjoint (Iio a) (Ici b) :=
  disjoint_left.mpr fun _ ha hb => (h.trans_lt' ha).not_ge hb

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

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

Разделы

Аффилиация

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