iUnion_filter_not — Mathlib

English

The iUnion of π.filter (not p) equals the difference π.iUnion minus (π.filter p).iUnion.

Русский

Объединение по iUnion предразбиения π.filter (не p) равно разности π.iUnion и (π.filter p).iUnion.

LaTeX

$$$ (π.filter \neg p).iUnion = π.iUnion \ (π.filter p).iUnion. $$$

Lean4

@[simp]
theorem iUnion_filter_not (π : Prepartition I) (p : Box ι → Prop) :
    (π.filter fun J => ¬p J).iUnion = π.iUnion \ (π.filter p).iUnion :=
  by
  simp only [Prepartition.iUnion]
  convert (@Set.biUnion_diff_biUnion_eq (ι → ℝ) (Box ι) π.boxes (π.filter p).boxes (↑) _).symm using 4
  · simp +contextual
  · rw [Set.PairwiseDisjoint]
    convert π.pairwiseDisjoint
    rw [Set.union_eq_left, filter_boxes, coe_filter]
    exact fun _ ⟨h, _⟩ => h

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