Library Coq.Sets.Finite_sets_facts

Require Export Finite_sets.
Require Export Constructive_sets.
Require Export Classical.
Require Export Classical_sets.
Require Export Powerset.
Require Export Powerset_facts.
Require Export Powerset_Classical_facts.
Require Export Gt.
Require Export Lt.

Section Finite_sets_facts.
  Variable U : Type.

  Lemma finite_cardinal :
    forall X:Ensemble U, Finite U X -> exists n : nat, cardinal U X n.

  Lemma cardinal_finite :
    forall (X:Ensemble U) (n:nat), cardinal U X n -> Finite U X.

  Theorem Add_preserves_Finite :
    forall (X:Ensemble U) (x:U), Finite U X -> Finite U (Add U X x).

  Theorem Singleton_is_finite : forall x:U, Finite U (Singleton U x).

  Theorem Union_preserves_Finite :
    forall X Y:Ensemble U, Finite U X -> Finite U Y -> Finite U (Union U X Y).

  Lemma Finite_downward_closed :
    forall A:Ensemble U,
      Finite U A -> forall X:Ensemble U, Included U X A -> Finite U X.

  Lemma Intersection_preserves_finite :
    forall A:Ensemble U,
      Finite U A -> forall X:Ensemble U, Finite U (Intersection U X A).

  Lemma cardinalO_empty :
    forall X:Ensemble U, cardinal U X 0 -> X = Empty_set U.

  Lemma inh_card_gt_O :
    forall X:Ensemble U, Inhabited U X -> forall n:nat, cardinal U X n -> n > 0.

  Lemma card_soustr_1 :
    forall (X:Ensemble U) (n:nat),
      cardinal U X n ->
      forall x:U, In U X x -> cardinal U (Subtract U X x) (pred n).

  Lemma cardinal_is_functional :
    forall (X:Ensemble U) (c1:nat),
      cardinal U X c1 ->
      forall (Y:Ensemble U) (c2:nat), cardinal U Y c2 -> X = Y -> c1 = c2.

  Lemma cardinal_Empty : forall m:nat, cardinal U (Empty_set U) m -> 0 = m.

  Lemma cardinal_unicity :
    forall (X:Ensemble U) (n:nat),
      cardinal U X n -> forall m:nat, cardinal U X m -> n = m.

  Lemma card_Add_gen :
    forall (A:Ensemble U) (x:U) (n n':nat),
      cardinal U A n -> cardinal U (Add U A x) n' -> n' <= S n.

  Lemma incl_st_card_lt :
    forall (X:Ensemble U) (c1:nat),
      cardinal U X c1 ->
      forall (Y:Ensemble U) (c2:nat),
        cardinal U Y c2 -> Strict_Included U X Y -> c2 > c1.

  Lemma incl_card_le :
    forall (X Y:Ensemble U) (n m:nat),
      cardinal U X n -> cardinal U Y m -> Included U X Y -> n <= m.

  Lemma G_aux :
    forall P:Ensemble U -> Prop,
      (forall X:Ensemble U,
        Finite U X ->
        (forall Y:Ensemble U, Strict_Included U Y X -> P Y) -> P X) ->
      P (Empty_set U).

  Lemma Generalized_induction_on_finite_sets :
    forall P:Ensemble U -> Prop,
      (forall X:Ensemble U,
        Finite U X ->
        (forall Y:Ensemble U, Strict_Included U Y X -> P Y) -> P X) ->
      forall X:Ensemble U, Finite U X -> P X.

End Finite_sets_facts.