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.