Iic_disjoint_Ioi

Mathlib.Order.Interval.Set.Disjoint

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

English

If a ≤ b, then the closed lower interval Iic(a) and the open upper interval Ioi(b) are disjoint.

Русский

Если a ≤ b, то пересечение ⋂ между Iic(a) и Ioi(b) пусто: Iic(a) ∩ Ioi(b) = ∅.

LaTeX

$$$$ a \le b \implies (Iic\,a) \cap (Ioi\,b) = \emptyset. $$$$

Lean4

@[simp]
theorem Iic_disjoint_Ioi (h : a ≤ b) : Disjoint (Iic a) (Ioi b) :=
  disjoint_left.mpr fun _ ha hb => (h.trans_lt hb).not_ge ha

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

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

Разделы

Аффилиация

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