erase_mem_compression_of_mem_compression

English

If s ∈ 𝓓 a 𝒜 and s is of the form s = insert a t with t ∈ 𝒜, then t ∈ 𝓓 a 𝒜.

Русский

Если s лежит в 𝓓 a 𝒜 и имеет вид s = insert a t, с t ∈ 𝒜, то t ∈ 𝓓 a 𝒜.

LaTeX

$$$\\text{If } s \\in 𝓓(a,\\mathcal{A}) \\text{ and } s = \\text{insert } a \\, t \\text{ with } t \\in \\mathcal{A}, \\text{ then } t \\in 𝓓(a,\\mathcal{A}).$$$

Lean4

theorem erase_mem_compression_of_mem_compression : s ∈ 𝓓 a 𝒜 → s.erase a ∈ 𝓓 a 𝒜 :=
  by
  simp_rw [mem_compression, erase_idem]
  refine Or.imp (fun h => ⟨h.2, h.2⟩) fun h => ?_
  rwa [erase_eq_of_notMem (insert_ne_self.1 <| ne_of_mem_of_not_mem h.2 h.1)]

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