iUnion_filter_not — Mathlib

English

If we filter by the negation of p, the iUnion is the difference between the original iUnion and the iUnion of the p-filter.

Русский

Если отфильтровать по отрицанию p, то iUnion равен разности исходного iUnion и iUnion отфильтрованного по p.

LaTeX

$$$ \\operatorname{iUnion}(\\pi.filter(\\lambda J, \\neg p J)) = \\operatorname{iUnion}(\\pi) \\setminus \\operatorname{iUnion}(\\pi.filter p) $$$

Lean4

@[simp]
theorem iUnion_filter_not (π : TaggedPrepartition I) (p : Box ι → Prop) :
    (π.filter fun J => ¬p J).iUnion = π.iUnion \ (π.filter p).iUnion :=
  π.toPrepartition.iUnion_filter_not p

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