iUnion_Ioc_left

Mathlib.Order.Interval.Set.Disjoint

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

← MathLib Explorer

English

Fix b. The union over a of the intervals (a, b] equals {x ≤ b}, i.e., Iic(b).

Русский

Зафиксируем правую границу b. Объединение по всем a интервалов (a, b] равно {x ≤ b}, т.е. Iic(b).

LaTeX

$$$$\bigcup_a Ioc(a,b) = Iic(b)$$$$

Lean4

@[simp]
theorem iUnion_Ioc_left [NoMinOrder α] (b : α) : ⋃ a, Ioc a b = Iic b := by
  simp only [← Ioi_inter_Iic, ← iUnion_inter, iUnion_Ioi, univ_inter]

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

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

Разделы

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

Аффилиация

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