filter_or — Mathlib

English

Let p and q be predicates on α. Then filtering by p ∨ q is the union of filtering by p and filtering by q: s.filter (fun a => p a ∨ q a) = s.filter p ∪ s.filter q.

Русский

Пусть p и q — предикаты на α. Тогда фильтрация по p ∨ q равна объединению фильтраций по p и по q: s.filter (p ∨ q) = s.filter p ∪ s.filter q.

LaTeX

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

Lean4

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

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