filter_congr_decidable — Mathlib

English

If predicates p and q agree on every element of s, then filtering by p and by q yields equal Finsets.

Русский

Если предикаты p и q дают одинаковые значения на каждом элементе s, то фильтрация по p и по q даёт одинаковые множества.

LaTeX

$$$\\forall s:\\, (\\forall x \\in s, p x \\iff q x) \\Rightarrow s.filter p = s.filter q$$$

Lean4

theorem filter_congr_decidable (s : Finset α) (p : α → Prop) (h : DecidablePred p) [DecidablePred p] :
    @filter α p h s = s.filter p := by congr

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