iUnion_split

Mathlib.Analysis.BoxIntegral.Partition.Split

URI: https://scilib.ai/kg/mathlib#BoxIntegral.Prepartition.iUnion_split

← MathLib Explorer

English

The iUnion of the boxes in split I i x equals I.

Русский

Объединение по iUnion коробок из split I i x равно I.

LaTeX

$$$\\mathrm{split}\\ I\\ i\\ x\\,\\mathrm{iUnion} = I$$$

Lean4

@[simp]
theorem iUnion_split (I : Box ι) (i : ι) (x : ℝ) : (split I i x).iUnion = I := by
  simp [split, ← inter_union_distrib_left, ← setOf_or, le_or_gt]

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

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

Разделы

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

Аффилиация

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