iUnion — Mathlib

English

The iUnion of a prepartition π is the part of I covered by the boxes of π.

Русский

Объединение iUnion предразбиения π представляет собой ту часть пространства, которая покрывается коробками π.

LaTeX

$$\text{protected def } \mathrm{iUnion} : Set(ι→ℝ) := ⋃ J ∈ π, ↑J$$

Lean4

/-- Given a prepartition `π : BoxIntegral.Prepartition I`, `π.iUnion` is the part of `I` covered by
the boxes of `π`. -/
protected def iUnion : Set (ι → ℝ) :=
  ⋃ J ∈ π, ↑J

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