Library mathcomp.analysis.cardinality

(* mathcomp analysis (c) 2017 Inria and AIST. License: CeCILL-C.              *)
From HB Require Import structures.
From mathcomp Require Import all_ssreflect finmap ssralg ssrnum ssrint rat.
From mathcomp Require Import finset.
Require Import boolp mathcomp_extra classical_sets functions.

Set Implicit Arguments.

Reserved Notation "A '#<=' B" (at level 79, format "A '#<=' B").
Reserved Notation "A '#>=' B" (at level 79, format "A '#>=' B").
Reserved Notation "A '#=' B" (at level 79, format "A '#=' B").
Reserved Notation "A '#!=' B" (at level 79, format "A '#!=' B").

Import Order.Theory GRing.Theory.

Local Open Scope classical_set_scope.
Local Open Scope ring_scope.
Local Open Scope function_scope.

Declare Scope card_scope.
Delimit Scope card_scope with card.
Local Open Scope card_scope.

Definition card_le T U (A : set T) (B : set U) :=
  `[< $|{injfun [set: A] >-> [set: B]}| >].
Notation "A '#<=' B" := (card_le A B) : card_scope.
Notation "A '#>=' B" := (card_le B A) (only parsing) : card_scope.

Definition card_eq T U (A : set T) (B : set U) :=
  `[< $|{bij [set: A] >-> [set: B]}| >].
Notation "A '#=' B" := (card_eq A B) : card_scope.
Notation "A '#!=' B" := (~~ (card_eq A B)) : card_scope.

Definition finite_set {T} (A : set T) := ∃ n, A #= `I_n.
Notation infinite_set A := (¬ finite_set A).

Lemma injPex {T U} {A : set T} :
   $|{inj A >-> U}| ↔ ∃ f : T → U, set_inj A f.

Lemma surjPex {T U} {A : set T} {B : set U} :
  $|{surj A >-> B}| ↔ ∃ f, set_surj A B f.

Lemma bijPex {T U} {A : set T} {B : set U} :
  $|{bij A >-> B}| ↔ ∃ f, set_bij A B f.

Lemma surjfunPex {T U} {A : set T} {B : set U} :
  $|{surjfun A >-> B}| ↔ ∃ f, B = f @` A.

Lemma injfunPex {T U} {A : set T} {B : set U}:
   $|{injfun A >-> B}| ↔ exists2 f : T → U, set_fun A B f & set_inj A f.

Lemma card_leP {T U} {A : set T} {B : set U} :
  reflect $|{injfun [set: A] >-> [set: B]}| (A #<= B).

Lemma inj_card_le {T U} {A : set T} {B : set U} : {injfun A >-> B} → (A #<= B).

Lemma pcard_leP {T} {U : pointedType} {A : set T} {B : set U} :
   reflect $|{injfun A >-> B}| (A #<= B).

Lemma pcard_leTP {T} {U : pointedType} {A : set T} :
  reflect $|{inj A >-> U}| (A #<= [set: U]).

Lemma pcard_injP {T} {U : pointedType} {A : set T} :
  reflect (∃ f : T → U, {in A &, injective f}) (A #<= [set: U]).

Lemma ppcard_leP {T U : pointedType} {A : set T} {B : set U} :
   reflect $|{splitinjfun A >-> B}| (A #<= B).

Lemma card_ge0 T U (S : set U) : @set0 T #<= S.
#[global] Hint Resolve card_ge0 : core.

Lemma card_le0P T U (A : set T) : reflect (A = set0) (A #<= @set0 U).

Lemma card_le0 T U (A : set T) : (A #<= @set0 U) = (A == set0).

Lemma card_eqP {T U} {A : set T} {B : set U} :
  reflect $|{bij [set: A] >-> [set: B]}| (A #= B).

Lemma pcard_eq {T U} {A : set T} {B : set U} : {bij A >-> B} → A #= B.

Lemma pcard_eqP {T} {U : pointedType} {A : set T} {B : set U} :
   reflect $| {bij A >-> B} | (A #= B).

Lemma card_bijP {T U} {A : set T} {B : set U} :
   reflect (∃ f : A → B, bijective f) (A #= B).

Lemma card_eqVP {T U} {A : set T} {B : set U} :
   reflect $|{splitbij [set: A] >-> [set: B]}| (A #= B).

Lemma card_set_bijP {T} {U : pointedType} {A : set T} {B : set U} :
   reflect (∃ f, set_bij A B f) (A #= B).

Lemma ppcard_eqP {T U : pointedType} {A : set T} {B : set U} :
   reflect $| {splitbij A >-> B} | (A #= B).

Lemma card_eqxx T (A : set T) : A #= A.
#[global] Hint Resolve card_eqxx : core.

Lemma card_eq00 T U : @set0 T #= @set0 U.
#[global] Hint Resolve card_eq00 : core.

Section empty1.
Implicit Types (T : emptyType).
Lemma empty_eq0 T : all_equal_to (set0 : set T).
Lemma card_le_emptyl T U (A : set T) (B : set U) : A #<= B.
Lemma card_le_emptyr T U (A : set T) (B : set U) : (B #<= A) = (B == set0).

Definition emptyE_subdef := (empty_eq0, card_le_emptyl, card_le_emptyr, eq_opE).
End empty1.

Theorem Cantor_Bernstein T U (A : set T) (B : set U) :
  A #<= B → B #<= A → A #= B.

Lemma card_esym T U (A : set T) (B : set U) : A #= B → B #= A.

Lemma card_eq_le T U (A : set T) (B : set U) :
  (A #= B) = (A #<= B) && (B #<= A).

Lemma card_eqPle T U (A : set T) (B : set U) :
  (A #= B) ↔ (A #<= B) ∧ (B #<= A).

Lemma card_lexx T (A : set T) : A #<= A.
#[global] Hint Resolve card_lexx : core.

Lemma card_leT T (S : set T) : S #<= [set: T].

Lemma subset_card_le T (A B : set T) : A `<=` B → A #<= B.

Lemma card_image_le {T U} (f : T → U) (A : set T) : f @` A #<= A.

Lemma inj_card_eq {T U} {A} {f : T → U} : {in A &, injective f} → f @` A #= A.
Arguments inj_card_eq {T U A f}.

Lemma card_some {T} {A : set T} : some @` A #= A.

Lemma card_image {T U} {A : set T} (f : {inj A >-> U}) : f @` A #= A.

Lemma card_imsub {T U} (A : set T) (f : {inj A >-> U}) X : X `<=` A → f @` X #= X.

Lemma card_le_trans (T U V : Type) (B : set U) (A : set T) (C : set V) :
  A #<= B → B #<= C → A #<= C.

Lemma card_eq_sym T U (A : set T) (B : set U) : (A #= B) = (B #= A).

Lemma card_eq_trans T U V (A : set T) (B : set U) (C : set V) :
  A #= B → B #= C → A #= C.

Lemma card_le_eql T T' T'' (A : set T) (B : set T') [C : set T''] :
   A #= B → (A #<= C) = (B #<= C).

Lemma card_le_eqr T T' T'' (A : set T) (B : set T') [C : set T''] :
   A #= B → (C #<= A) = (C #<= B).

Lemma card_eql T T' T'' (A : set T) (B : set T') [C : set T''] :
   A #= B → (A #= C) = (B #= C).

Lemma card_eqr T T' T'' (A : set T) (B : set T') [C : set T''] :
   A #= B → (C #= A) = (C #= B).

Lemma card_ge_image {T U V} {A : set T} (f : {inj A >-> U}) X (Y : set V) :
  X `<=` A → (f @` X #<= Y) = (X #<= Y).

Lemma card_le_image {T U V} {A : set T} (f : {inj A >-> U}) X (Y : set V) :
  X `<=` A → (Y #<= f @` X) = (Y #<= X).

Lemma card_le_image2 {T U} (A : set T) (f : {inj A >-> U}) X Y :
   X `<=` A → Y `<=` A →
   (f @` X #<= f @` Y) = (X #<= Y).

Lemma card_eq_image {T U V} {A : set T} (f : {inj A >-> U}) X (Y : set V) :
  X `<=` A → (f @` X #= Y) = (X #= Y).

Lemma card_eq_imager {T U V} {A : set T} (f : {inj A >-> U}) X (Y : set V) :
  X `<=` A → (Y #= f @` X) = (Y #= X).

Lemma card_eq_image2 {T U} (A : set T) (f : {inj A >-> U}) X Y :
   X `<=` A → Y `<=` A →
   (f @` X #= f @` Y) = (X #= Y).

Lemma card_ge_some {T T'} {A : set T} {B : set T'} :
  (some @` A #<= B) = (A #<= B).

Lemma card_le_some {T T'} {A : set T} {B : set T'} :
  (A #<= some @` B) = (A #<= B).

Lemma card_le_some2 {T T'} {A : set T} {B : set T'} :
  (some @` A #<= some @` B) = (A #<= B).

Lemma card_eq_somel {T T'} {A : set T} {B : set T'} :
  (some @` A #= B) = (A #= B).

Lemma card_eq_somer {T T'} {A : set T} {B : set T'} :
  (A #= some @` B) = (A #= B).

Lemma card_eq_some2 {T T'} {A : set T} {B : set T'} :
  (some @` A #= some @` B) = (A #= B).

Lemma card_eq0 {T U} {A : set T} : (A #= @set0 U) = (A == set0).

Lemma card_eq_emptyr (T : emptyType) U (A : set T) (B : set U) :
  (B #= A) = (B == set0).

Lemma card_eq_emptyl (T : emptyType) U (A : set T) (B : set U) :
  (A #= B) = (B == set0).

Definition emptyE := (emptyE_subdef, card_eq_emptyr, card_eq_emptyl).

Lemma card_setT T (A : set T) : [set: A] #= A.
#[global] Hint Resolve card_setT : core.

Lemma card_setT_sym T (A : set T) : A #= [set: A].
#[global] Hint Resolve card_setT : core.

Lemma surj_card_ge {T U} {A : set T} {B : set U} : {surj B >-> A} → A #<= B.
Arguments surj_card_ge {T U A B} g.

Lemma pcard_surjP {T : pointedType} {U} {A : set T} {B : set U} :
  reflect (∃ g, set_surj B A g) (A #<= B).

Lemma pcard_geP {T : pointedType} {U} {A : set T} {B : set U} :
  reflect $|{surj B >-> A}| (A #<= B).

Lemma ocard_geP {T U} {A : set T} {B : set U} :
  reflect $|{surj B >-> some @` A}| (A #<= B).

Lemma pfcard_geP {T U} {A : set T} {B : set U} :
  reflect (A = set0 ∨ $|{surjfun B >-> A}|) (A #<= B).

Lemma card_le_II n m : (`I_n #<= `I_m) = (n ≤ m)%N.

Lemma ocard_eqP {T U} {A : set T} {B : set U} :
  reflect $|{bij A >-> some @` B}| (A #= B).

Lemma oocard_eqP {T U} {A : set T} {B : set U} :
  reflect $|{splitbij some @` A >-> some @` B}| (A #= B).

Lemma card_eq_II {n m} : reflect (n = m) (`I_n #= `I_m).

Lemma sub_setP {T} {A : set T} (X : set A) : set_val @` X `<=` A.
Arguments sub_setP {T A}.
Arguments image_subset {aT rT} f [A B].

Lemma card_subP T U (A : set T) (B : set U) :
  reflect (exists2 C, C #= A & C `<=` B) (A #<= B).

Lemma pigeonhole m n (f : nat → nat) : {in `I_m &, injective f} →
  f @` `I_m `<=` `I_n → (m ≤ n)%N.

Definition countable T (A : set T) := A #<= @setT nat.

Lemma eq_countable T U (A : set T) (B : set U) :
  A #= B → countable A = countable B.

Lemma countable_setT_countMixin (T : Type) :
  countable (@setT T) → Countable.mixin_of T.

Lemma countableP (T : countType) (A : set T) : countable A.
#[global] Hint Resolve countableP : core.

Lemma countable0 T : countable (@set0 T).
#[global] Hint Resolve countable0 : core.

Lemma countable_injP T (A : set T) :
  reflect (∃ f : T → nat, {in A &, injective f}) (countable A).

Lemma sub_countable T U (A : set T) (B : set U) : A #<= B →
  countable B → countable A.

Lemma finite_setP T (A : set T) : finite_set A ↔ ∃ n, A #= `I_n.

Lemma finite_II n : finite_set `I_n.
#[global] Hint Resolve finite_II : core.

Lemma card_II {n} : `I_n #= [set: 'I_n].

Lemma finite_fsetP {T : choiceType} {A : set T} :
  finite_set A ↔ ∃ X : {fset T}, A = [set` X].

Lemma finite_subfset {T : choiceType} (X : {fset T}) {A : set T} :
  A `<=` [set` X] → finite_set A.
Arguments finite_subfset {T} X {A}.

Lemma finite_set0 T : finite_set (set0 : set T).
#[global] Hint Resolve finite_set0 : core.

Lemma finite_seqP {T : eqType} A :
   finite_set A ↔ ∃ s : seq T, A = [set` s].

Lemma finite_seq {T : eqType} (s : seq T) : finite_set [set` s].
#[global] Hint Resolve finite_seq : core.

Lemma finite_fset {T : choiceType} (X : {fset T}) : finite_set [set` X].
#[global] Hint Resolve finite_fset : core.

Lemma finite_finpred {T : finType} {pT : predType T} (P : pT) :
  finite_set [set` P].
#[global]
Hint Extern 0 (finite_set [set` _]) ⇒ solve [apply: finite_finpred] : core.

Lemma finite_finset {T : finType} {X : set T} : finite_set X.
#[global] Hint Resolve finite_finset : core.

Lemma finite_set_countable T (A : set T) : finite_set A → countable A.

Lemma infiniteP T (A : set T) : infinite_set A ↔ [set: nat] #<= A.

Lemma finite_setPn T (A : set T) : finite_set A ↔ ¬ ([set: nat] #<= A).

Lemma card_le_finite T U (A : set T) (B : set U) :
  A #<= B → finite_set B → finite_set A.

Lemma sub_finite_set T (A B : set T) : A `<=` B →
  finite_set B → finite_set A.

Lemma finite_set_leP T (A : set T) : finite_set A ↔ ∃ n, A #<= `I_n.

Lemma card_ge_preimage {T U} (B : set U) (f : T → U) :
  {in f @^-1` B &, injective f} → f @^-1` B #<= B.

Corollary finite_preimage {T U} (B : set U) (f : T → U) :
  {in f @^-1` B &, injective f} → finite_set B → finite_set (f @^-1` B).

Lemma eq_finite_set T U (A : set T) (B : set U) :
  A #= B → finite_set A = finite_set B.

Lemma card_le_setD T (A B : set T) : A `\` B #<= A.

Lemma finite_image T T' A (f : T → T') : finite_set A → finite_set (f @` A).

Lemma finite_set1 T (x : T) : finite_set [set x].
#[global] Hint Resolve finite_set1 : core.

Lemma finite_setD T (A B : set T) : finite_set A → finite_set (A `\` B).

Lemma finite_setU T (A B : set T) :
  finite_set (A `|` B) = (finite_set A ∧ finite_set B).

Lemma finite_set2 T (x y : T) : finite_set [set x; y].
#[global] Hint Resolve finite_set2 : core.

Lemma finite_set3 T (x y z : T) : finite_set [set x; y; z].
#[global] Hint Resolve finite_set3 : core.

Lemma finite_set4 T (x y z t : T) : finite_set [set x; y; z; t].
#[global] Hint Resolve finite_set4 : core.

Lemma finite_set5 T (x y z t u : T) : finite_set [set x; y; z; t; u].
#[global] Hint Resolve finite_set5 : core.

Lemma finite_set6 T (x y z t u v : T) : finite_set [set x; y; z; t; u; v].
#[global] Hint Resolve finite_set6 : core.

Lemma finite_set7 T (x y z t u v w : T) : finite_set [set x; y; z; t; u; v; w].
#[global] Hint Resolve finite_set7 : core.

Lemma finite_setI T (A B : set T) :
  (finite_set A ∨ finite_set B) → finite_set (A `&` B).

Lemma finite_setIl T (A B : set T) : finite_set A → finite_set (A `&` B).

Lemma finite_setIr T (A B : set T) : finite_set B → finite_set (A `&` B).

Lemma finite_setM T T' (A : set T) (B : set T') :
  finite_set A → finite_set B → finite_set (A `*` B).

Lemma finite_image2 [aT bT rT : Type] [A : set aT] [B : set bT] (f : aT → bT → rT) :
  finite_set A → finite_set B → finite_set [set f x y | x in A & y in B]%classic.

Lemma finite_image11 [xT aT bT rT : Type] [X : set xT]
    (g : aT → bT → rT) (fa : xT → aT) (fb : xT → bT) :
    finite_set (fa @` X) → finite_set (fb @` X) →
  finite_set [set g (fa x) (fb x) | x in X]%classic.

Definition fset_set (T : choiceType) (A : set T) :=
  if pselect (finite_set A) is left Afin
  then projT1 (cid (finite_fsetP.1 Afin)) else fset0.

Lemma fset_setK (T : choiceType) (A : set T) : finite_set A →
  [set` fset_set A] = A.

Lemma in_fset_set (T : choiceType) (A : set T) : finite_set A →
  fset_set A =i A.

Lemma fset_set_sub (T : choiceType) (A B : set T) :
  finite_set A → finite_set B → A `<=` B = (fset_set A `<=` fset_set B)%fset.

Lemma fset_set_set0 (T : choiceType) (A : set T) : finite_set A →
  fset_set A = fset0 → A = set0.

Lemma fset_set0 {T : choiceType} : fset_set (set0 : set T) = fset0.

Lemma fset_set1 {T : choiceType} (x : T) : fset_set [set x] = [fset x]%fset.

Lemma fset_setU {T : choiceType} (A B : set T) :
  finite_set A → finite_set B →
  fset_set (A `|` B) = (fset_set A `|` fset_set B)%fset.

Lemma fset_setI {T : choiceType} (A B : set T) :
  finite_set A → finite_set B →
  fset_set (A `&` B) = (fset_set A `&` fset_set B)%fset.

Lemma fset_setU1 {T : choiceType} (x : T) (A : set T) :
  finite_set A → fset_set (x |` A) = (x |` fset_set A)%fset.

Lemma fset_setD {T : choiceType} (A B : set T) :
  finite_set A → finite_set B →
  fset_set (A `\` B) = (fset_set A `\` fset_set B)%fset.

Lemma fset_setD1 {T : choiceType} (x : T) (A : set T) :
  finite_set A → fset_set (A `\ x) = (fset_set A `\ x)%fset.

Lemma fset_setM {T1 T2 : choiceType} (A : set T1) (B : set T2) :
    finite_set A → finite_set B →
  fset_set (A `*` B) = (fset_set A `*` fset_set B)%fset.

Definition fst_fset (T1 T2 : choiceType) (A : {fset (T1 × T2)}) : {fset T1} :=
  [fset x.1 | x in A]%fset.
Definition snd_fset (T1 T2 : choiceType) (A : {fset (T1 × T2)}) : {fset T2} :=
  [fset x.2 | x in A]%fset.
Notation "A .`1" := (fst_fset A) : fset_scope.
Notation "A .`2" := (snd_fset A) : fset_scope.

Lemma finite_set_fst (T1 T2 : choiceType) (A : set (T1 × T2)) :
  finite_set A → finite_set A.`1.

Lemma finite_set_snd (T1 T2 : choiceType) (A : set (T1 × T2)) :
  finite_set A → finite_set A.`2.

Lemma bigcup_finite {I T} (D : set I) (F : I → set T) :
    finite_set D → (∀ i, D i → finite_set (F i)) →
  finite_set (\bigcup_(i in D) F i).

Lemma trivIset_sum_card (T : choiceType) (F : nat → set T) n :
  (∀ n, finite_set (F n)) → trivIset [set: nat] F →
  (\sum_(i < n) #|` fset_set (F i)| =
   #|` fset_set (\big[setU/set0]_(k < n) F k)|)%N.

Lemma finite_setMR (T T' : choiceType) (A : set T) (B : T → set T') :
  finite_set A → (∀ x, A x → finite_set (B x)) → finite_set (A `*`` B).

Lemma finite_setML (T T' : choiceType) (A : T' → set T) (B : set T') :
  (∀ x, B x → finite_set (A x)) → finite_set B → finite_set (A ``*` B).

Lemma fset_set_II n : fset_set `I_n = [fset val i | i in 'I_n]%fset.

Lemma set_fsetK (T : choiceType) (A : {fset T}) : fset_set [set` A] = A.

Lemma fset_set_image {T U : choiceType} (f : T → U) (A : set T) :
  finite_set A → fset_set (f @` A) = (f @` fset_set A)%fset.

Lemma fset_set_inj {T : choiceType} (A B : set T) :
  finite_set A → finite_set B → fset_set A = fset_set B → A = B.

Lemma bigsetU_fset_set T (I : choiceType) (A : set I) (F : I → set T) :
  finite_set A → \big[setU/set0]_(i <- fset_set A) F i =\bigcup_(i in A) F i.

#[deprecated(note="Use -bigsetU_fset_set instead")]
Lemma bigcup_fset_set T (I : choiceType) (A : set I) (F : I → set T) :
  finite_set A → \bigcup_(i in A) F i = \big[setU/set0]_(i <- fset_set A) F i.

Lemma bigsetU_fset_set_cond T (I : choiceType) (A : set I) (F : I → set T)
    (P : pred I) : finite_set A →
  \big[setU/set0]_(i <- fset_set A | P i) F i = \bigcup_(i in A `&` P) F i.

#[deprecated(note="Use -bigsetU_fset_set_cond instead")]
Lemma bigcup_fset_set_cond T (I : choiceType) (A : set I) (F : I → set T)
    (P : pred I) : finite_set A →
  \bigcup_(i in A `&` P) F i = \big[setU/set0]_(i <- fset_set A | P i) F i.

Lemma bigsetI_fset_set T (I : choiceType) (A : set I) (F : I → set T) :
  finite_set A → \big[setI/setT]_(i <- fset_set A) F i =\bigcap_(i in A) F i.

#[deprecated(note="Use -bigsetI_fset_set instead")]
Lemma bigcap_fset_set T (I : choiceType) (A : set I) (F : I → set T) :
  finite_set A → \bigcap_(i in A) F i = \big[setI/setT]_(i <- fset_set A) F i.

Lemma bigsetI_fset_set_cond T (I : choiceType) (A : set I) (F : I → set T)
    (P : pred I) : finite_set A →
  \big[setI/setT]_(i <- fset_set A | P i) F i = \bigcap_(i in A `&` P) F i.

Lemma super_bij T U (X A : set T) (Y B : set U) (f : {bij X >-> Y}) :
  X `<=` A → Y `<=` B → A `\` X #= B `\` Y →
  ∃ g : {bij A >-> B}, {in X, g =1 f}.

Lemma card_eq_fsetP {T : choiceType} {A : {fset T}} {n} :
  reflect (#|` A| = n) ([set` A] #= `I_n).

Lemma card_fset_set {T : choiceType} (A : set T) n :
  A #= `I_n → #|`fset_set A| = n.

Lemma geq_card_fset_set {T : choiceType} (A : set T) n :
  A #<= `I_n → (#|`fset_set A| ≤ n)%N.

Lemma leq_card_fset_set {T : choiceType} (A : set T) n :
  finite_set A → A #>= `I_n → (#|`fset_set A| ≥ n)%N.

Lemma infinite_set_fset {T : choiceType} (A : set T) (n : nat) :
  infinite_set A →
    exists2 B : {fset T}, [set` B] `<=` A & (#|` B| ≥ n)%N.

Lemma infinite_set_fsetP {T : choiceType} (A : set T) :
  infinite_set A ↔
   ∀ n, exists2 B : {fset T}, [set` B] `<=` A & (#|` B| ≥ n)%N.

Lemma fcard_eq {T T' : choiceType} (A : set T) (B : set T') :
    finite_set A → finite_set B →
  reflect (#|`fset_set A| = #|`fset_set B|) (A #= B).

Lemma card_IID {n k} : `I_n `\` `I_k #= `I_(n - k)%N.

Lemma finite_set_bij T (A : set T) n S : A != set0 →
    A #= `I_n → S `<=` A →
  ∃ (f : {bij `I_n >-> A}) k, (k ≤ n)%N ∧ `I_n `&` (f @^-1` S) = `I_k.

#[deprecated(note="use countable0 instead")]
Notation countable_set0 := countable0.

Lemma countable1 T (x : T) : countable [set x].
#[global] Hint Resolve countable1 : core.

Lemma countable_fset (T : choiceType) (X : {fset T}) : countable [set` X].
#[global] Hint Resolve countable_fset : core.

Lemma countable_finpred (T : finType) (pT : predType T) (P : pT) : countable [set` P].
#[global] Hint Extern 0 (is_true (countable [set` _])) ⇒ solve [apply: countable_finpred] : core.

Lemma eq_card_nat T (A : set T):
  countable A → ¬ finite_set A → A #= [set: nat].

Lemma infinite_nat : ¬ finite_set [set: nat].

Lemma infinite_prod_nat : infinite_set [set: nat × nat].

Lemma card_nat2 : [set: nat × nat] #= [set: nat].

Canonical rat_pointedType := PointedType rat 0.

Lemma infinite_rat : infinite_set [set: rat].

Lemma card_rat : [set: rat] #= [set: nat].

Lemma choicePcountable {T : choiceType} : countable [set: T] →
  {T' : countType | T = T' :> Type}.

Lemma eqPcountable {T : eqType} : countable [set: T] →
  {T' : countType | T = T' :> Type}.

Lemma Pcountable {T : Type} : countable [set: T] →
  {T' : countType | T = T' :> Type}.

Lemma bigcup_countable {I T} (D : set I) (F : I → set T) :
    countable D → (∀ i, D i → countable (F i)) →
  countable (\bigcup_(i in D) F i).

Lemma countableMR T T' (A : set T) (B : T → set T') :
  countable A → (∀ i, A i → countable (B i)) → countable (A `*`` B).

Lemma countableM T1 T2 (D1 : set T1) (D2 : set T2) :
  countable D1 → countable D2 → countable (D1 `*` D2).

Lemma countableML T T' (A : T' → set T) (B : set T') :
  countable B → (∀ i, B i → countable (A i)) → countable (A ``*` B).

Lemma infiniteMRl T T' (A : set T) (B : T → set T') :
  infinite_set A → (∀ i, B i !=set0) → infinite_set (A `*`` B).

Lemma cardMR_eq_nat T T' (A : set T) (B : T → set T') :
    (A #= [set: nat] → (∀ i, countable (B i) ∧ B i !=set0) →
   A `*`` B #= [set: nat])%card.


Reserved Notation "{ 'fimfun' aT >-> T }"
  (at level 0, format "{ 'fimfun' aT >-> T }").
Reserved Notation "[ 'fimfun' 'of' f ]"
  (at level 0, format "[ 'fimfun' 'of' f ]").
Notation "{ 'fimfun' aT >-> T }" := (@FImFun.type aT T) : form_scope.
Notation "[ 'fimfun' 'of' f ]" := [the {fimfun _ >-> _} of f] : form_scope.
#[global] Hint Resolve fimfunP : core.

Lemma fimfun_inP {aT rT} (f : {fimfun aT >-> rT}) (D : set aT) :
  finite_set (f @` D).

#[global] Hint Resolve fimfun_inP : core.

Section fimfun_pred.
Context {aT rT : Type}.
Definition fimfun : {pred aT → rT} := mem [set f | finite_set (range f)].
Definition fimfun_key : pred_key fimfun.
Canonical fimfun_keyed := KeyedPred fimfun_key.
End fimfun_pred.

Section fimfun.
Context {aT rT : Type}.
Notation T := {fimfun aT >-> rT}.
Notation fimfun := (@fimfun aT rT).
Section Sub.
Context (f : aT → rT) (fP : f \in fimfun).
Definition fimfun_Sub_subproof := @FiniteImage.Build aT rT f (set_mem fP).
#[local] HB.instance Definition _ := fimfun_Sub_subproof.
Definition fimfun_Sub := [fimfun of f].
End Sub.

Lemma fimfun_rect (K : T → Type) :
  (∀ f (Pf : f \in fimfun), K (fimfun_Sub Pf)) → ∀ u : T, K u.

Lemma fimfun_valP f (Pf : f \in fimfun) : fimfun_Sub Pf = f :> (_ → _).

Canonical fimfun_subType := SubType T _ _ fimfun_rect fimfun_valP.
End fimfun.

Lemma fimfuneqP aT rT (f g : {fimfun aT >-> rT}) :
  f = g ↔ f =1 g.

Definition fimfuneqMixin aT (rT : eqType) :=
  [eqMixin of {fimfun aT >-> rT} by <:].
Canonical fimfuneqType aT (rT : eqType) :=
  EqType {fimfun aT >-> rT} (fimfuneqMixin aT rT).
Definition fimfunchoiceMixin aT (rT : choiceType) :=
  [choiceMixin of {fimfun aT >-> rT} by <:].
Canonical fimfunchoiceType aT (rT : choiceType) :=
  ChoiceType {fimfun aT >-> rT} (fimfunchoiceMixin aT rT).

Lemma finite_image_cst {aT rT : Type} (x : rT) :
  finite_set (range (cst x : aT → _)).

Lemma cst_fimfun_subproof aT rT x : @FiniteImage aT rT (cst x).
Definition cst_fimfun {aT rT} x := [the {fimfun aT >-> rT} of cst x].

Lemma fimfun_cst aT rT x : @cst_fimfun aT rT x =1 cst x.

Lemma comp_fimfun_subproof aT rT sT
   (f : {fimfun aT >-> rT}) (g : rT → sT) : @FiniteImage aT sT (g \o f).

Section zmod.
Context (aT : Type) (rT : zmodType).
Lemma fimfun_zmod_closed : zmod_closed (@fimfun aT rT).
Canonical fimfun_add := AddrPred fimfun_zmod_closed.
Canonical fimfun_zmod := ZmodPred fimfun_zmod_closed.
Definition fimfun_zmodMixin := [zmodMixin of {fimfun aT >-> rT} by <:].
Canonical fimfun_zmodType := ZmodType {fimfun aT >-> rT} fimfun_zmodMixin.

Implicit Types (f g : {fimfun aT >-> rT}).

Lemma fimfunD f g : f + g = f \+ g :> (_ → _).
Lemma fimfunN f : - f = \- f :> (_ → _).
Lemma fimfunB f g : f - g = f \- g :> (_ → _).
Lemma fimfun0 : (0 : {fimfun aT >-> rT}) = cst 0 :> (_ → _).
Lemma fimfun_sum I r (P : {pred I}) (f : I → {fimfun aT >-> rT}) (x : aT) :
  (\sum_(i <- r | P i) f i) x = \sum_(i <- r | P i) f i x.

End zmod.