unionComplToSubordinate_boxes — Mathlib

English

The boxes of the union-complement subordinate partition equal the union of π1.boxes and (π2.toSubordinate r).boxes.

Русский

Множество коробок разбиения, полученного unionComplToSubordinate, равно объединению π1.boxes и (π2.toSubordinate r).boxes.

LaTeX

$$$ (\\pi_1.\\mathrm{unionComplToSubordinate}(\\pi_2,hU,r)).\\mathrm{boxes} = \\pi_1.\\mathrm{boxes} \\cup (\\pi_2.\\mathrm{toSubordinate} r).\\mathrm{boxes} $$$

Lean4

@[simp]
theorem unionComplToSubordinate_boxes (π₁ : TaggedPrepartition I) (π₂ : Prepartition I)
    (hU : π₂.iUnion = ↑I \ π₁.iUnion) (r : (ι → ℝ) → Ioi (0 : ℝ)) :
    (π₁.unionComplToSubordinate π₂ hU r).boxes = π₁.boxes ∪ (π₂.toSubordinate r).boxes :=
  rfl

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