mk_surjective_eq_zero_iff_lift — Mathlib

English

The cardinal of surjective functions α → β' is zero iff lift(#α) < lift(#β') or (α ≠ ∅ and β' = ∅).

Русский

Кардинал множества сюръективных отображений α → β' равен нулю тогда и только тогда, когда lift(#α) < lift(#β') или (α непусто и β' пусто).

LaTeX

$$$ #{f:\\\\alpha \\\\to \\\\beta' | Surjective f} = 0 \\iff lift(#α) < lift(#β') \\lor (#α \\neq 0 \\land #β' = 0) $$$

Lean4

theorem mk_surjective_eq_zero_iff_lift :
    #{f : α → β' | Surjective f} = 0 ↔ lift.{v} #α < lift.{u} #β' ∨ (#α ≠ 0 ∧ #β' = 0) :=
  by
  rw [← not_iff_not, not_or, not_lt, lift_mk_le', ← Ne, not_and_or, not_ne_iff, and_comm]
  simp_rw [mk_ne_zero_iff, mk_eq_zero_iff, nonempty_coe_sort, Set.Nonempty, mem_setOf, exists_surjective_iff,
    nonempty_fun]

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