bijective_of_nat_card_le — Mathlib

English

If surjective f and Nat.card α ≤ Nat.card β with [Finite α], then Bijective f.

Русский

Если surjective f и Nat.card α ≤ Nat.card β при конечном α, тогда f биективно.

LaTeX

$$$ [\mathrm{Finite}\,\alpha] (f : \alpha \to \beta) \rightarrow (\mathrm{Surjective}\,f \rightarrow \mathrm{Bijective}\,f) $$$

Lean4

theorem _root_.Function.Surjective.bijective_of_nat_card_le [Finite α] {f : α → β} (surj : Surjective f)
    (hc : Nat.card α ≤ Nat.card β) : Bijective f :=
  (Nat.bijective_iff_surjective_and_card f).mpr ⟨surj, hc.antisymm (card_le_card_of_surjective f surj)⟩

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