具有双射的两个“finType”的基数相等

Question

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

语句为：

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 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.

具有双射的两个“finType”的基数相等

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

coq

ssreflect