English
Let α be a type, m,n ∈ ℕ. If hn : m+n ≤ ENat.card α, then the map x ↦ (Fin.castAddEmb n).trans x is surjective from Fin (m+n) ↪ α to Fin n ↪ α.
Русский
Пусть α — множество, m+n ≤ ENat.card α. Тогда отображение x ↦ (Fin.castAddEmb n).trans x направляет все вложения Fin(m+n) ↪ α на вложения Fin n ↪ α и нацело образует всю область.
LaTeX
$$$m+n \\le ENat.card \\alpha \\Rightarrow \\operatorname{Surjective}\\left(\\lambda x : Fin(m+n) \\hookrightarrow \\alpha, (Fin.castAddEmb n).trans x\\right).$$$
Lean4
theorem restrictSurjective_of_add_le_ENatCard (hn : m + n ≤ ENat.card α) :
Surjective (fun (x : Fin (m + n) ↪ α) ↦ (Fin.castAddEmb n).trans x) :=
by
intro x
obtain ⟨y, hxy⟩ :=
exists_embedding_disjoint_range_of_add_le_ENat_card (s := range x)
(by simpa [← Nat.card_coe_set_eq, Nat.card_range_of_injective x.injective])
use append hxy
ext i
simp [trans_apply, coe_castAddEmb, append]
