Ssreflect Users Discussion List

[Christian Doczkal <>]

Hello

Today I needed the following lemma with, surprisingly, I could not find
in the ssreflect component:

Lemma card_set (T:finType) : #|{set T}| = 2^#|T|.

I have a proof (see below), but the proof seems overly complicated.
Specifically, I did not manage to exploit that {set T} is defined in
terms of finite function types for which a cardinality lemma exists.

Can someone show me a simpler proof that exploits the definition of
set_type?

Cheers
Christian

------------------------------------------------------------------------

Require Import mathcomp.ssreflect.ssreflect.
From mathcomp Require Import all_ssreflect.

Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.

Lemma inj_leq_card (T T' : finType) (f : T -> T') :
  injective f -> #|T| <= #|T'|.
Proof. move => inj_f. by rewrite -(card_imset predT inj_f) max_card. Qed.

Lemma bij_card {X Y : finType} (f : X->Y): bijective f -> #|X| = #|Y|.
Proof.
  case => g /can_inj Hf /can_inj Hg. apply/eqP.
  by rewrite eqn_leq (inj_leq_card Hf) (inj_leq_card Hg).
Qed.

Lemma card_set (T:finType) : #|{set T}| = 2^#|T|.
Proof.
  suff H: #|{set T}| = #|{ffun pred T}|
    by rewrite H card_ffun card_bool.
  pose f (X:{set T}) := [ffun x => x \in X].
  pose g (F:{ffun pred T}) := [set x | F x].
  apply : (bij_card (f := f)). apply: (Bijective (g := g)).
  - move => X. rewrite /f /g. apply/setP => x. by rewrite inE ffunE.
  - move => F. rewrite /f /g. apply/ffunP => x. by rewrite ffunE inE.
Qed.