coq - 具有双射的两个`finType`的基数相等

Question

我有两个finTypes，它们之间有一个双射。目前，我需要它们具有相同的基数这一事实。但是，我找不到这个引理，也找不到可以轻松证明该陈述的其他引理。在我看来，证明应该不难。

声明是：

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

任何帮助表示赞赏！

Answer 1

Cyril Cohen在这里提供了一个非常好的证明：

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.