Search code examples
coqssreflect

Equality of cardinalities of two `finType`s with a bijection

I have two finTypes with a bijection between them. At the moment, I need the fact that they have equal cardinalities. However, I cannot find this lemma, nor other lemmas with which the statement can be easily proven. It seems to me that the proof shouldn't be hard.

The statement is:

From mathcomp Require Import ssrfun ssrbool eqtype fintype.
Lemma bij_card_eq (T T' : finType) (f : T -> T') : bijective f -> #|T| = #|T'|.
Proof.
Admitted.

Any help is appreciated!

Solution

  • There is a really nice proof of this fact by Cyril Cohen here:

    From mathcomp Require Import all_ssreflect.

Section BijCard.

Variables U V : finType.
Variable f : U -> V.

Lemma bij_card : bijective f -> #|U| = #|V|.
Proof.
move=> [g fgK gfK]; rewrite -(card_image (can_inj fgK)).
by apply/eq_card=> x; apply/imageP; exists (g x).
Qed.

End BijCard.