filter_congr — Mathlib

English

If for all x in s, p x ↔ q x, then filter p s = filter q s.

Русский

Если для каждого x ∈ s выполняется p x ↔ q x, тогда фильтование p s равняется фильтованию q s.

LaTeX

$$$\\forall x \\in s, p x \\leftrightarrow q x \\Rightarrow s.filter p = s.filter q$$$

Lean4

theorem filter_congr {s : Finset α} (H : ∀ x ∈ s, p x ↔ q x) : filter p s = filter q s :=
  eq_of_veq <| Multiset.filter_congr H

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