mem_erase_iff — Mathlib

English

In a nodup multiset, membership after erasing b is equivalent to a ≠ b and membership in the original.

Русский

В нодуп-мультисете членство после стирания b эквивалентно a ≠ b и членству в исходном.

LaTeX

$$$ l.Nodup \\rightarrow (a \\in l.erase b) \\iff (a \\neq b) \\wedge (a \\in l) $$$

Lean4

theorem mem_erase_iff [DecidableEq α] {a b : α} {l} (d : Nodup l) : a ∈ l.erase b ↔ a ≠ b ∧ a ∈ l := by
  rw [d.erase_eq_filter b, mem_filter, and_comm]

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