mem_diff_iff — Mathlib

English

For decidable equality, membership in l1.diff l2 is equivalent to membership in l1 and not in l2.

Русский

При разрешённом равенстве членство в l1.diff l2 эквивалентно членству в l1 и отсутствию в l2.

LaTeX

$$$ [\\DecidableEq \\ α] \\\\ (hl_1) : a \\in l_1.diff l_2 \\iff a \\in l_1 \\land a \\notin l_2. $$$

Lean4

theorem mem_diff_iff [DecidableEq α] (hl₁ : l₁.Nodup) : a ∈ l₁.diff l₂ ↔ a ∈ l₁ ∧ a ∉ l₂ := by
  rw [hl₁.diff_eq_filter, mem_filter, decide_eq_true_iff]

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