Iic_disjoint_Ioc

Mathlib.Order.Interval.Set.Disjoint

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

English

If a ≤ b, then for every c, Iic(a) is disjoint from Ioc(b,c).

Русский

Если a ≤ b, тогда для любого c Iic(a) и Ioc(b,c) не пересекаются.

LaTeX

$$$$ a \le b \implies \forall c, (Iic\,a) \cap (Ioc\,b\,c) = \emptyset. $$$$

Lean4

@[simp]
theorem Iic_disjoint_Ioc (h : a ≤ b) : Disjoint (Iic a) (Ioc b c) :=
  (Iic_disjoint_Ioi h).mono le_rfl Ioc_subset_Ioi_self

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

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

Разделы

Аффилиация

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