card_eq_zero_of_surjective — Mathlib

English

If f : α → β is surjective and Nat.card β = 0, then Nat.card α = 0.

Русский

Если f : α → β сюръективно и Nat.card β = 0, то Nat.card α = 0.

LaTeX

$$$Nat.card(\beta) = 0 \Rightarrow Nat.card(\alpha) = 0$$$

Lean4

/-- NB: `Nat.card` is defined to be `0` for infinite types. -/
theorem card_eq_zero_of_surjective {f : α → β} (hf : Function.Surjective f) (h : Nat.card β = 0) : Nat.card α = 0 :=
  by
  cases finite_or_infinite β
  · haveI := card_eq_zero_iff.mp h
    haveI := Function.isEmpty f
    exact Nat.card_of_isEmpty
  · haveI := Infinite.of_surjective f hf
    exact Nat.card_eq_zero_of_infinite

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