English
If S and T are disjoint, then filter p on their disjUnion equals the disjoint union of their filters: filter p (disjUnion S T H) = disjUnion (filter p S) (filter p T) (disjoint_filter_filter h).
Русский
Если S и T непересекаются, то фильтр по p на их объединении равен объединению фильтров: filter p (disjUnion S T H) = disjUnion (filter p S) (filter p T) (disjoint_filter_filter H).
LaTeX
$$$\\operatorname{filter}(p, \\mathrm{disjUnion}(S,T,H)) = \\mathrm{disjUnion}(\\operatorname{filter}(p,S), \\operatorname{filter}(p,T), \\operatorname{disjoint\\_filter\\_filter}(H))$$$
Lean4
theorem filter_disjUnion (s : Finset α) (t : Finset α) (h : Disjoint s t) :
filter p (disjUnion s t h) = (filter p s).disjUnion (filter p t) (disjoint_filter_filter h) :=
eq_of_veq <| Multiset.filter_add _ _ _
