English
If f : α → β is surjective and Nat.card α = 0 implies Nat.card β = 0, then Nat.card β ≤ Nat.card α.
Русский
Если f : α → β сюръективно отображает и Nat.card α = 0 ⇒ Nat.card β = 0, то Nat.card β ≤ Nat.card α.
LaTeX
$$$Nat.card(\beta) \le Nat.card(\alpha)$$$
Lean4
/-- If `f` is surjective, then `Nat.card β ≤ Nat.card α`. We must also assume
`Nat.card α = 0 → Nat.card β = 0` since `Nat.card` is defined to be `0` for infinite types. -/
theorem card_le_of_surjective' {f : α → β} (hf : Function.Surjective f) (h : Nat.card α = 0 → Nat.card β = 0) :
Nat.card β ≤ Nat.card α :=
(or_not_of_imp h).casesOn (fun h => le_of_eq_of_le h (Nat.zero_le _)) fun h =>
@Nat.card_le_card_of_surjective α β (Nat.finite_of_card_ne_zero h) f hf
