erase_mem_compression — Mathlib

English

If s ∈ 𝒜, then s.erase a ∈ 𝓓 a 𝒜.

Русский

Если s принадлежит 𝒜, то s удаление a принадлежит 𝓓 a 𝒜.

LaTeX

$$$s \\in 𝒜 \\Rightarrow s \\setminus \\{a\\} \\in 𝓓 a 𝒜$$$

Lean4

theorem erase_mem_compression (hs : s ∈ 𝒜) : s.erase a ∈ 𝓓 a 𝒜 :=
  by
  simp_rw [mem_compression, erase_idem, and_self_iff]
  refine (em _).imp_right fun h => ⟨h, ?_⟩
  rwa [insert_erase (erase_ne_self.1 (ne_of_mem_of_not_mem hs h).symm)]
    -- This is a special case of `erase_mem_compression` once we have `compression_idem`.

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