surjective_decode_iget — Mathlib

English

For any α with Encodable α and inhabited α, the map n ↦ (decode n).iget: α is surjective.

Русский

Пусть α кодируем, и имеем непустый α; отображение n ↦ (decode n).iget: α сюрьективно на α.

LaTeX

$$$\operatorname{Surjective}\;\big(\lambda n, (\operatorname{decode} n)\!\text{.iget} : α\big)$$$

Lean4

theorem surjective_decode_iget (α : Type*) [Encodable α] [Inhabited α] :
    Surjective fun n => ((Encodable.decode n).iget : α) := fun x => ⟨Encodable.encode x, by simp_rw [Encodable.encodek]⟩

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