Ico_disjoint_Ico

Mathlib.Order.Interval.Multiset

URI: https://scilib.ai/kg/mathlib#Multiset.Ico_disjoint_Ico

← MathLib Explorer

English

If b ≤ c, then the intersection Ico(a,b) ∩ Ico(c,d) is empty.

Русский

Если b ≤ c, то пересечение Ico(a,b) и Ico(c,d) пусто.

LaTeX

$$$ b \le c \rightarrow Ico\ a\ b \cap Ico\ c\ d = 0 $$$

Lean4

theorem Ico_disjoint_Ico {a b c d : α} (h : b ≤ c) : Disjoint (Ico a b) (Ico c d) :=
  disjoint_left.mpr fun hab hbc => by
    rw [mem_Ico] at hab hbc
    exact hab.2.not_ge (h.trans hbc.1)

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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