English
Let α be infinite and suppose the codomain β' has cardinality at most that of α (in the lifted sense). Then the number of surjections from α onto β' equals the number of all functions from α to β'.
Русский
Пусть α бесконечно, и если кардинальность β' не превосходит кардинальности α (после подъёма по лифту). Тогда число сюръекций из α на β' равно числу всех отображений α → β'.
LaTeX
$$$\\left|\\{ f: \\alpha \\to \\beta' \\;|\\; \\text{Surjective}(f) \\}\\right| = |\\alpha \\to \\beta'|$$$
Lean4
theorem mk_surjective_eq_arrow_of_lift_le (lle : lift.{u} #β' ≤ lift.{v} #α) :
#{f : α → β' | Surjective f} = #(α → β') :=
(mk_set_le _).antisymm <|
have ⟨e⟩ : Nonempty (α ≃ α ⊕ β') :=
by
simp_rw [← lift_mk_eq', mk_sum, lift_add, lift_lift]; rw [lift_umax.{u, v}, eq_comm]
exact add_eq_left (aleph0_le_lift.mpr <| aleph0_le_mk α) lle
⟨⟨fun f ↦ ⟨fun a ↦ (e a).elim f id, fun b ↦ ⟨e.symm (.inr b), congr_arg _ (e.right_inv _)⟩⟩, fun f g h ↦
funext fun a ↦ by simpa only [e.apply_symm_apply] using congr_fun (Subtype.ext_iff.mp h) (e.symm <| .inl a)⟩⟩
