filter_ne' — Mathlib

English

A variant of the previous result with a prime-notation, stating the same equality.

Русский

Вариант предыдущего вывода с пометкой Prime, выражающий ту же равенство.

LaTeX

$$$\\operatorname{filter} (\\lambda a. a \\neq b)\\, s = s.erase b$$$

Lean4

theorem filter_ne' [DecidableEq β] (s : Finset β) (b : β) : (s.filter fun a => a ≠ b) = s.erase b :=
  _root_.trans (filter_congr fun _ _ => by simp_rw [@ne_comm _ b]) (filter_ne s b)

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