isHenstock_biUnionTagged — Mathlib

English

The iUnion of the biUnionTagged construction equals the union over J in π of the iUnion of πi(J).

Русский

Объединение iUnion конструкции biUnionTagged равно объединению по J в π от iUnion(πi(J)).

LaTeX

$$$ (\\pi.biUnionTagged πi).iUnion = ⋃_{J \\in \\pi} (π_i(J)).iUnion $$$

Lean4

@[simp]
theorem isHenstock_biUnionTagged {π : Prepartition I} {πi : ∀ J, TaggedPrepartition J} :
    IsHenstock (π.biUnionTagged πi) ↔ ∀ J ∈ π, (πi J).IsHenstock :=
  π.forall_biUnionTagged (fun x J => x ∈ Box.Icc J) πi

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