Library Coq.Sets.Constructive_sets
Require Export Ensembles.
Section Ensembles_facts.
Variable U :
Type.
Lemma Extension :
forall B C:
Ensemble U,
B = C ->
Same_set U B C.
Lemma Noone_in_empty :
forall x:
U,
~ In U (
Empty_set U)
x.
Lemma Included_Empty :
forall A:
Ensemble U,
Included U (
Empty_set U)
A.
Lemma Add_intro1 :
forall (
A:
Ensemble U) (
x y:
U),
In U A y ->
In U (
Add U A x)
y.
Lemma Add_intro2 :
forall (
A:
Ensemble U) (
x:
U),
In U (
Add U A x)
x.
Lemma Inhabited_add :
forall (
A:
Ensemble U) (
x:
U),
Inhabited U (
Add U A x).
Lemma Inhabited_not_empty :
forall X:
Ensemble U,
Inhabited U X ->
X <> Empty_set U.
Lemma Add_not_Empty :
forall (
A:
Ensemble U) (
x:
U),
Add U A x <> Empty_set U.
Lemma not_Empty_Add :
forall (
A:
Ensemble U) (
x:
U),
Empty_set U <> Add U A x.
Lemma Singleton_inv :
forall x y:
U,
In U (
Singleton U x)
y ->
x = y.
Lemma Singleton_intro :
forall x y:
U,
x = y ->
In U (
Singleton U x)
y.
Lemma Union_inv :
forall (
B C:
Ensemble U) (
x:
U),
In U (
Union U B C)
x ->
In U B x \/ In U C x.
Lemma Add_inv :
forall (
A:
Ensemble U) (
x y:
U),
In U (
Add U A x)
y ->
In U A y \/ x = y.
Lemma Intersection_inv :
forall (
B C:
Ensemble U) (
x:
U),
In U (
Intersection U B C)
x ->
In U B x /\ In U C x.
Lemma Couple_inv :
forall x y z:
U,
In U (
Couple U x y)
z ->
z = x \/ z = y.
Lemma Setminus_intro :
forall (
A B:
Ensemble U) (
x:
U),
In U A x ->
~ In U B x ->
In U (
Setminus U A B)
x.
Lemma Strict_Included_intro :
forall X Y:
Ensemble U,
Included U X Y /\ X <> Y ->
Strict_Included U X Y.
Lemma Strict_Included_strict :
forall X:
Ensemble U,
~ Strict_Included U X X.
End Ensembles_facts.
Hint Resolve Singleton_inv Singleton_intro Add_intro1 Add_intro2
Intersection_inv Couple_inv Setminus_intro Strict_Included_intro
Strict_Included_strict Noone_in_empty Inhabited_not_empty Add_not_Empty
not_Empty_Add Inhabited_add Included_Empty:
sets v62.