mk_surjective_eq_arrow_of_le — Mathlib

English

If α is infinite and |β| ≤ |α|, then the number of surjections from α to β 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_le (le : #β ≤ #α) : #{f : α → β | Surjective f} = #(α → β) :=
  mk_surjective_eq_arrow_of_lift_le (lift_le.mpr le)

Похожие утверждения