bijective_iff_injective_and_card — Mathlib

English

Bijective f if and only if Injective f and Nat.card α = Nat.card β, assuming [Finite β].

Русский

Биекция эквивалентна инъективности и равенству кардиналов, при условии, что β конечен.

LaTeX

$$$ [\mathrm{Finite}\,\beta] (f : \alpha \to \beta) : \mathrm{Bijective}\,f \iff (\mathrm{Injective}\,f \land \mathrm{Nat.card}\alpha = \mathrm{Nat.card}\beta) $$$

Lean4

protected theorem bijective_iff_injective_and_card [Finite β] (f : α → β) :
    Bijective f ↔ Injective f ∧ Nat.card α = Nat.card β :=
  by
  rw [Bijective, and_congr_right_iff]
  intro h
  have := Fintype.ofFinite β
  have := Fintype.ofInjective f h
  revert h
  rw [← and_congr_right_iff, ← Bijective, card_eq_fintype_card, card_eq_fintype_card,
    Fintype.bijective_iff_injective_and_card]

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