filter_union — Mathlib

English

For any finite S1,S2, filter p on their union equals the union of their filters: (S1 ∪ S2).filter p = S1.filter p ∪ S2.filter p.

Русский

Для любых конечных S1,S2: (S1 ∪ S2).filter p = S1.filter p ∪ S2.filter p.

LaTeX

$$$\\operatorname{filter}(p, S_1 \\cup S_2) = \\operatorname{filter}(p, S_1) \\cup \\operatorname{filter}(p, S_2)$$$

Lean4

theorem filter_union (s₁ s₂ : Finset α) : (s₁ ∪ s₂).filter p = s₁.filter p ∪ s₂.filter p := by grind

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