filter_ne — Mathlib

English

For a Finset s and an element b, filtering by inequality to b yields the same as erasing b: (s.filter (fun a => b ≠ a)) = s.erase b.

Русский

Для конечного множества s и элемента b фильтрация по неравенству b даёт то же, что стирание b: (s.filter (b ≠ a)) = s.erase b.

LaTeX

$$$(s.filter (\\lambda a. b \\neq a)) = s.erase b$$$

Lean4

theorem filter_ne [DecidableEq β] (s : Finset β) (b : β) : (s.filter fun a => b ≠ a) = s.erase b := by grind

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