isPartition_unionComplToSubordinate

English

For π1: TaggedPrepartition I, π2: Prepartition I, hU: π2.iUnion = I \\ π1.iUnion, then π1.unionComplToSubordinate π2 hU r is a partition.

Русский

Для π1: TaggedPrepartition I и π2: Prepartition I при заданном hU, тогда π1.unionComplToSubordinate π2 hU r является разбиением.

LaTeX

$$$ \\mathrm{IsPartition}(\\pi_1.\\mathrm{unionComplToSubordinate}(\\pi_2,hU,r)) $$$

Lean4

theorem isPartition_unionComplToSubordinate (π₁ : TaggedPrepartition I) (π₂ : Prepartition I)
    (hU : π₂.iUnion = ↑I \ π₁.iUnion) (r : (ι → ℝ) → Ioi (0 : ℝ)) : IsPartition (π₁.unionComplToSubordinate π₂ hU r) :=
  Prepartition.isPartitionDisjUnionOfEqDiff ((π₂.iUnion_toSubordinate r).trans hU)

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