Equivalence_of_Mappings_between_Sets_of_Same_Cardinality
Provedbijectionsinjectionsproofwikisurjections
Let and be finite sets such that . Let be a mapping. Then the following statements are equivalent is bijective is injective is surjective.
Preamble
import Mathlib.Data.Fintype.Card
Formal statement
theorem Equivalence_of_Mappings_between_Sets_of_Same_Cardinality {S T : Type _} [Fintype S] [Fintype T] (h : Fintype.card S = Fintype.card T) (f : S → T) : Function.Bijective f ↔ Function.Injective f := by sorrySource