compress_mem_compression_of_mem_compression

English

If a is in 𝓒 u v s, then compress u v a is again in 𝓒 u v s; compression is closed under compression of its own outputs.

Русский

Если a ∈ 𝓒_{u,v}(s), то 𝒞_{u,v}(a) ∈ 𝓒_{u,v}(s); сжатие замкнуто относительно своих результатов.

LaTeX

$$a \\in 𝓒_{u,v}(s) \\Rightarrow 𝒞_{u,v}(a) ∈ 𝓒_{u,v}(s)$$

Lean4

theorem compress_mem_compression_of_mem_compression (ha : a ∈ 𝓒 u v s) : compress u v a ∈ 𝓒 u v s :=
  by
  rw [mem_compression] at ha ⊢
  simp only [compress_idem]
  obtain ⟨_, ha⟩ | ⟨_, b, hb, rfl⟩ := ha
  · exact Or.inl ⟨ha, ha⟩
  · exact Or.inr ⟨by rwa [compress_idem], b, hb, (compress_idem _ _ _).symm⟩

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