iUnion_biUnion_partition — Mathlib

English

For π, πi, with each πi(J) a partition, the iUnion of the biUnion equals the iUnion of π.

Русский

Для разбиения π и семейства πi с каждым πi(J) разбиением выполняется равенство iUnion(π.biUnion πi) = iUnion(π).

LaTeX

$$$ (\\pi).iUnion = (π.biUnion πi).iUnion$$$

Lean4

theorem iUnion_biUnion_partition (h : ∀ J ∈ π, (πi J).IsPartition) : (π.biUnion πi).iUnion = π.iUnion :=
  (iUnion_biUnion _ _).trans <|
    iUnion_congr_of_surjective id surjective_id fun J =>
      iUnion_congr_of_surjective id surjective_id fun hJ => (h J hJ).iUnion_eq

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