iUnion_biUnionTagged — Mathlib

English

The iUnion of the biUnionTagged πi is the union, over J in π, of the iUnion of πi(J).

Русский

Объединение iUnion(πbiUnionTagged(πi)) есть объединение по J в π от iUnion(πi(J)).

LaTeX

$$$ (\\pi.biUnionTagged πi).iUnion = \\bigcup_{J \\in \\pi} (\\pi_i(J)).iUnion $$$

Lean4

@[simp]
theorem iUnion_biUnionTagged (π : Prepartition I) (πi : ∀ J, TaggedPrepartition J) :
    (π.biUnionTagged πi).iUnion = ⋃ J ∈ π, (πi J).iUnion :=
  iUnion_biUnion _ _

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