mk_surjective_eq_zero_iff — Mathlib

English

The cardinal of surjective functions α → β equals zero iff α < β or (α ≠ 0 and β = 0).

Русский

Кардинал множества сюръективных отображений α → β равен нулю тогда и только тогда, когда α меньше β или (α ≠ 0 и β = 0).

LaTeX

$$$ #{f:\\\\alpha \\\\to \\\\beta} = 0 \\iff #a < #b \\lor (#a \\neq 0 \\land #b = 0) $$$

Lean4

theorem mk_surjective_eq_zero_iff : #{f : α → β | Surjective f} = 0 ↔ #α < #β ∨ (#α ≠ 0 ∧ #β = 0) := by
  rw [mk_surjective_eq_zero_iff_lift, lift_lt]

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