English
For any n, there exists a list a such that a ∈ decodeList n and encodeList a = n.
Русский
Для любого n существует список a, такой что a ∈ decodeList n и encodeList a = n.
LaTeX
$$$\\forall n, \\exists a \\in \\decodeList n, \\; \\encodeList a = n$$$
Lean4
@[nolint unusedHavesSuffices] -- This is a false positive in the unusedHavesSuffices linter.
theorem denumerable_list_aux : ∀ n : ℕ, ∃ a ∈ @decodeList α _ n, encodeList a = n
| 0 => by rw [decodeList]; exact ⟨_, rfl, rfl⟩
| succ v => by
rcases e : unpair v with ⟨v₁, v₂⟩
have h := unpair_right_le v
rw [e] at h
rcases
have : v₂ < succ v := lt_succ_of_le h
denumerable_list_aux v₂ with
⟨a, h₁, h₂⟩
rw [Option.mem_def] at h₁
use ofNat α v₁ :: a
simp [decodeList, e, h₂, h₁, encodeList, pair_eq_of_unpair_eq e]
