biUnionPrepartition — Mathlib

English

If π is a tagged partition and each πi J is a prepartition with its own partition property, then the biUnionPrepartition is partition.

Русский

Если π — тэггированное разбиение и каждое πi J — предразбиение с собственным свойством разбиения, то biUnionPrepartition является разбиением.

LaTeX

$$$ IsPartition(\\pi.biUnionPrepartition πi) $$$

Lean4

theorem biUnionPrepartition {π : TaggedPrepartition I} (h : IsPartition π) {πi : ∀ J, Prepartition J}
    (hi : ∀ J ∈ π, (πi J).IsPartition) : (π.biUnionPrepartition πi).IsPartition :=
  h.biUnion hi

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