filter_union_right — Mathlib

English

Filter distributes over union via or: s.filter p ∪ s.filter q = s.filter (p ∨ q).

Русский

Фильтр распределяется через объединение по логическому or: s.filter p ∪ s.filter q = s.filter (p ∨ q).

LaTeX

$$$\\operatorname{filter}(p, S) \\cup \\operatorname{filter}(q, S) = \\operatorname{filter}(\\lambda x. p(x) \\lor q(x), S)$$$

Lean4

theorem filter_union_right (s : Finset α) : s.filter p ∪ s.filter q = s.filter fun x => p x ∨ q x := by grind

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