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.