iUnion_splitMany

Mathlib.Analysis.BoxIntegral.Partition.Split

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

English

The iUnion of the boxes in splitMany I s equals I.

Русский

Объединение по iUnion коробок в splitMany I s равно I.

LaTeX

$$$(\\mathrm{splitMany}\\ I\\ s).\\mathrm{iUnion} = I$$$

Lean4

@[simp]
theorem iUnion_splitMany (I : Box ι) (s : Finset (ι × ℝ)) : (splitMany I s).iUnion = I :=
  (isPartition_splitMany I s).iUnion_eq

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

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

Разделы

Аффилиация

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