filter_union_filter_of_codisjoint

English

If p and q are codisjoint, then filtering by p and by q covers all of s: s.filter p ∪ s.filter q = s.

Русский

Если p и q кодиспариваются (codisjoint), тогда фильтрации по p и по q охватывают всё s: s.filter p ∪ s.filter q = s.

LaTeX

$$$s^{\\filter} p \\cup s^{\\filter} q = s$$$

Lean4

theorem filter_union_filter_of_codisjoint (s : Finset α) (h : Codisjoint p q) : s.filter p ∪ s.filter q = s :=
  (filter_or _ _ _).symm.trans <| filter_true_of_mem fun x _ => h.top_le x trivial

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