# Library CoLoR.Util.Set.InfSet

CoLoR, a Coq library on rewriting and termination. See the COPYRIGHTS and LICENSE files.
• Frederic Blanqui, 2014-12-11
Infinite sets

Set Implicit Arguments.

Section S.

Variable A : Type.

# Definition of infinite sets

Definition infinite (P : set A) := ~finite P.

# Properties of infinite.

Global Instance infinite_subset : Proper (subset ==> impl) infinite.

Global Instance infinite_equiv : Proper (equiv ==> iff) infinite.

A set P is infinite if there is an injection from nat to P.

# Set constructors preserve infiniteness.

Lemma infinite_rem a P : infinite (rem a P) <-> infinite P.

Lemma infinite_union P Q : infinite (union P Q) <-> infinite P \/ infinite Q.

Lemma infinite_diff P Q : infinite (diff P Q) -> infinite P.

Lemma infinite_diff_finite P Q (Q_dec : forall x, {Q x}+{~Q x}) :
infinite P -> finite Q -> infinite (diff P Q).

Lemma infinite_not_empty P : infinite P -> exists x, mem x P.

# Type for infinite subsets of some set P

Definition Pinf P := {Q | Q [<=] P /\ infinite Q}.

Definition mk_Pinf P Q : Q [<=] P -> infinite Q -> Pinf P.

Definition Pinf_val P (Q : Pinf P) := proj1_sig Q.

Definition Pinf_sub P (Q : Pinf P) : Q [<=] P.

Definition Pinf_inf P (Q : Pinf P) : infinite Q.

Definition Pinf_subset P Q : P [<=] Q -> Pinf P -> Pinf Q.

Definition Pinf_self P (Q : Pinf P) : Pinf Q.

An infinite set contains finite subsets of every cardinality.

Section Pcard_of_inf.

Variable W : set A.

Lemma Pcard_of_inf_spec (P : Pinf W) :
forall n, exists X : Pf A, X [<=] P /\ card X = S n.

Definition Pcard_of_inf (P : Pinf W) n : Pcard P (S n).

End Pcard_of_inf.

End S.