filter_disjiUnion — Mathlib

English

Filtering after a disjiUnion equals the disjiUnion of filtered fibers.

Русский

Фильтрация после disjiUnion равна disjiUnion отфильтрованных волокон.

LaTeX

$$$\\text{filter}_p (s.disjiUnion f h) = s.disjiUnion (\\lambda a => (f a).filter p) (\\text{pairwiseDisjoint_filter } h p)$$$

Lean4

theorem filter_disjiUnion (s : Finset α) (f : α → Finset β) (h) (p : β → Prop) [DecidablePred p] :
    (s.disjiUnion f h).filter p = s.disjiUnion (fun a ↦ (f a).filter p) (pairwiseDisjoint_filter h p) := by grind

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