filter_and — Mathlib

English

Let s be a finite set and p, q predicates. Then s.filter (fun a => p a ∧ q a) equals s.filter p ∩ s.filter q.

Русский

Пусть s — конечное множество, а p и q — предикаты. Тогда s.filter (p ∧ q) = s.filter p ∩ s.filter q.

LaTeX

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

Lean4

theorem filter_and (s : Finset α) : (s.filter fun a => p a ∧ q a) = s.filter p ∩ s.filter q := by grind

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