bijective function between types of equal cardinality

Stream: Is there code for X?

[Eric Wieser]

Did you forget to include the signature you're asking about? (edit: I renamed the thread now that you've posted your actual question)

[Joseph O]

Oh yeah i forgot.

theorem card_a_eq_card_b_iff_bijective {α β : Type} (f : α → β) : #α = #β ↔ function.bijective f :=
begin
  sorry,
end

[Joseph O]

I really just want a better name for this.

[Kyle Miller]

That theorem's not true -- f doesn't have to be bijective if the cardinalities of the domain and codomain are the same.

[Eric Wieser]

Example: set α = β = ℕ and f = 0

[Eric Wieser]

I would guess the statement you want is docs#cardinal.eq, which is essentially true by definition

[Eric Wieser]

Turn an equiv into a bijective function is easy and not really a useful thing to do anyway