card_eq_zero_of_injective — Mathlib

English

If α is nonempty and f : α → β is injective, then Nat.card β = 0 implies 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_injective [Nonempty α] {f : α → β} (hf : Function.Injective f) (h : Nat.card α = 0) :
    Nat.card β = 0 :=
  card_eq_zero_of_surjective (Function.invFun_surjective hf) h

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