card_le_card_of_injective — Mathlib

English

If f : α → β is injective, then ENat.card α ≤ ENat.card β.

Русский

Если f : α → β инъективна, то ENat.card α ≤ ENat.card β.

LaTeX

$$$\operatorname{ENat}.card(\alpha) \le \operatorname{ENat}.card(\beta)$$$

Lean4

theorem card_le_card_of_injective {α β : Type*} {f : α → β} (hf : Injective f) : card α ≤ card β :=
  by
  rw [← card_ulift α, ← card_ulift β]
  exact Cardinal.gciENat.gc.monotone_u <| Cardinal.lift_mk_le_lift_mk_of_injective hf

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