compl_erase — Mathlib

English

The complement of removing a from s equals inserting a into the complement of s: (s \\ {a})ᶜ = sᶜ ∪ {a}.

Русский

Дополнение удаления a из s равно дополнению sᶜ с добавлением a: (s \\ {a})ᶜ = sᶜ ∪ {a}.

LaTeX

$$$ (s \\\\{a\\\\})^{c} = s^{c} \\\\cup \\\\{a\\\\}$$$

Lean4

@[simp]
theorem compl_erase : (s.erase a)ᶜ = insert a sᶜ := by
  ext
  simp only [or_iff_not_imp_left, mem_insert, not_and, mem_compl, mem_erase]

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