Iic_disjoint_Ioc

Mathlib.Order.Interval.Finset.Basic

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

← MathLib Explorer

English

If a ≤ b, the sets Iic(a) and Ioc(b,c) are disjoint.

Русский

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

LaTeX

$$Disjoint(Iic(a), Ioc(b,c)) \text{ when } a \le b$$

Lean4

theorem Iic_disjoint_Ioc (h : a ≤ b) : Disjoint (Iic a) (Ioc b c) :=
  disjoint_left.2 fun _ hax hbcx ↦ (mem_Iic.1 hax).not_gt <| lt_of_le_of_lt h (mem_Ioc.1 hbcx).1

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

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

Разделы

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

Аффилиация

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