iUnion

Mathlib.Analysis.BoxIntegral.Partition.Tagged

URI: https://scilib.ai/kg/mathlib#BoxIntegral.TaggedPrepartition.iUnion

English

The iUnion of a tagged prepartition π is defined as the iUnion of its underlying prepartition.

Русский

iUnion тэгированного предразбиения π определяется как iUnion базового предразбиения.

LaTeX

$$$ \\mathrm{iUnion} = \\mathrm{toPrepartition}(\\pi).\\mathrm{iUnion}$$$

Lean4

/-- Union of all boxes of a tagged prepartition. -/
def iUnion : Set (ι → ℝ) :=
  π.toPrepartition.iUnion

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

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

Разделы

Аффилиация

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