English
For every p in Fin(n), the map p.predAbove: Fin(n) → Fin(n+1) is surjective; equivalently, for every y in Fin(n+1) there exists x in Fin(n) with p.predAbove(x) = y.
Русский
Для любого p ∈ Fin(n) отображение p.predAbove: Fin(n) → Fin(n+1) сюръектно; эквивалентно: для каждого y ∈ Fin(n+1) существует x ∈ Fin(n) такое, что p.predAbove(x) = y.
LaTeX
$$$\forall p \in \mathrm{Fin}(n),\ \forall y \in \mathrm{Fin}(n+1),\ \exists x \in \mathrm{Fin}(n),\ p\ predAbove(x) = y$$$
Lean4
theorem predAbove_surjective {n : ℕ} (p : Fin n) : Function.Surjective p.predAbove :=
by
intro i
by_cases hi : i ≤ p
· exact ⟨i.castSucc, predAbove_castSucc_of_le p i hi⟩
· rw [Fin.not_le] at hi
exact ⟨i.succ, predAbove_succ_of_le p i (Fin.le_of_lt hi)⟩
