mem_compression_of_insert_mem_compression

English

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

Русский

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

LaTeX

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

Lean4

theorem mem_compression_of_insert_mem_compression (h : insert a s ∈ 𝓓 a 𝒜) : s ∈ 𝓓 a 𝒜 :=
  by
  by_cases ha : a ∈ s
  · rwa [insert_eq_of_mem ha] at h
  · rw [← erase_insert ha]
    exact erase_mem_compression_of_mem_compression h

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