card_le_card_of_injective — Mathlib

English

If f : α → β is injective and [Finite β], Nat.card α ≤ Nat.card β.

Русский

Если отображение инъективно и β конечно, то Nat.card α ≤ Nat.card β.

LaTeX

$$$ \forall {\alpha\, \beta}, [\mathrm{Finite}\,\beta] (f : \alpha \to \beta), \mathrm{Injective}\,f \rightarrow \mathrm{Nat.card}\alpha \le \mathrm{Nat.card}\beta $$$

Lean4

theorem card_le_card_of_injective {α : Type u} {β : Type v} [Finite β] (f : α → β) (hf : Injective f) :
    Nat.card α ≤ Nat.card β := by simpa using toNat_le_toNat (lift_mk_le_lift_mk_of_injective hf) (by simp)

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