iUnion_unionComplToSubordinate_boxes

English

The iUnion of the union-complement subordinate partition equals I.

Русский

Объединение iUnion разбиения unionComplToSubordinate равно I.

LaTeX

$$$ (\\pi_1.\\mathrm{unionComplToSubordinate}(\\pi_2,hU,r)).\\mathrm{iUnion} = I $$$

Lean4

@[simp]
theorem iUnion_unionComplToSubordinate_boxes (π₁ : TaggedPrepartition I) (π₂ : Prepartition I)
    (hU : π₂.iUnion = ↑I \ π₁.iUnion) (r : (ι → ℝ) → Ioi (0 : ℝ)) : (π₁.unionComplToSubordinate π₂ hU r).iUnion = I :=
  (isPartition_unionComplToSubordinate _ _ _ _).iUnion_eq

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