English
If f : α → β is injective 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(\alpha) \le Nat.card(\beta)$$$
Lean4
/-- If `f` is injective, 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_injective' {f : α → β} (hf : Function.Injective 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_injective α β (Nat.finite_of_card_ne_zero h) f hf
