bijective_iff_surjective_and_card

English

Bijective f iff Surjective f and Nat.card α = Nat.card β, assuming [Finite α].

Русский

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

LaTeX

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

Lean4

protected theorem bijective_iff_surjective_and_card [Finite α] (f : α → β) :
    Bijective f ↔ Surjective f ∧ Nat.card α = Nat.card β := by
  classical
  rw [_root_.and_comm, Bijective, and_congr_left_iff]
  intro h
  have := Fintype.ofFinite α
  have := Fintype.ofSurjective f h
  revert h
  rw [← and_congr_left_iff, ← Bijective, ← and_comm, card_eq_fintype_card, card_eq_fintype_card,
    Fintype.bijective_iff_surjective_and_card]

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