English
Let C: ℕ → Sort*, n ≤ m, next with each next, and Hnext surjective; then leRecOn is surjective from C n to C m.
Русский
Пусть C: ℕ → Sort*, n ≤ m, next; если каждый next сюръективен, то леRecOn сюръективен из C n в C m.
LaTeX
$$$\forall z \in C(m), \exists y \in C(n): \; \mathrm{leRecOn}\ C\ n\ m\ hnm\ next\ y = z$$$
Lean4
theorem leRecOn_surjective {C : ℕ → Sort*} {n m} (hnm : n ≤ m) (next : ∀ {k}, C k → C (k + 1))
(Hnext : ∀ n, Surjective (@next n)) : Surjective (@leRecOn C n m hnm next) := by
induction hnm with
| refl =>
intro x
refine ⟨x, ?_⟩
rw [leRecOn_self]
| step hnm ih =>
intro x
obtain ⟨w, rfl⟩ := Hnext _ x
obtain ⟨x, rfl⟩ := ih w
refine ⟨x, ?_⟩
rw [leRecOn_succ]
