Ico_disjoint_Ico_same

Mathlib.Order.Interval.Set.Disjoint

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

English

Disjoint (Ico a b) (Ico b c).

Русский

Пересечение Ico(a,b) и Ico(b,c) пусто.

LaTeX

$$$$ (Ico\,a\,b) \cap (Ico\,b\,c) = \emptyset. $$$$

Lean4

@[simp]
theorem Ico_disjoint_Ico_same : Disjoint (Ico a b) (Ico b c) :=
  disjoint_left.mpr fun _ hab hbc => hab.2.not_ge hbc.1

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

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

Разделы

Аффилиация

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