Ico_inter_Ico_of_le

Mathlib.Order.Interval.Multiset

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

← MathLib Explorer

English

For a ≤ b with DecidableEq, the intersection Icc(a,b) ∩ Ico(b,d) is empty.

Русский

Для a ≤ b иDecidableEq пересечение Icc(a,b) ∩ Ico(b,d) пусто.

LaTeX

$$$ [DecidableEq\ α] \{ a,b,c,d:\ α\}, b ≤ c \rightarrow Icc a b \cap Ico c d = 0 $$$

Lean4

@[simp]
theorem Ico_inter_Ico_of_le [DecidableEq α] {a b c d : α} (h : b ≤ c) : Ico a b ∩ Ico c d = 0 :=
  Multiset.inter_eq_zero_iff_disjoint.2 <| Ico_disjoint_Ico h

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

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

Разделы

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

Аффилиация

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