erase_eq_empty_iff — Mathlib

English

For any finite S ⊆ α and a ∈ α, S \\ {a} = ∅ if and only if S = ∅ or S = {a}.

Русский

Пусть S ⊆ α — конечное множество и a ∈ α. Тогда S \\ {a} = ∅ тогда и только тогда, когда S = ∅ или S = {a}.

LaTeX

$$$S \\setminus \\{a\\} = \\emptyset \\iff S = \\emptyset \\lor S = \\{a\\}$$$

Lean4

theorem erase_eq_empty_iff (s : Finset α) (a : α) : s.erase a = ∅ ↔ s = ∅ ∨ s = { a } := by
  rw [← sdiff_singleton_eq_erase, sdiff_eq_empty_iff_subset, subset_singleton_iff]
    --TODO@Yaël: Kill lemmas duplicate with `BooleanAlgebra`

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