card_le_card_of_surjective — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

theorem card_le_card_of_surjective {α : Type u} {β : Type v} [Finite α] (f : α → β) (hf : Surjective f) :
    Nat.card β ≤ Nat.card α :=
  by
  have : lift.{u} #β ≤ lift.{v} #α := mk_le_of_surjective (ULift.map_surjective.2 hf)
  simpa using toNat_le_toNat this (by simp)

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