Library Coq.Sets.Classical_sets
Require Export Ensembles.
Require Export Constructive_sets.
Require Export Classical.
Section Ensembles_classical.
Variable U :
Type.
Lemma not_included_empty_Inhabited :
forall A:
Ensemble U,
~ Included U A (
Empty_set U)
-> Inhabited U A.
Lemma not_empty_Inhabited :
forall A:
Ensemble U,
A <> Empty_set U -> Inhabited U A.
Lemma Inhabited_Setminus :
forall X Y:
Ensemble U,
Included U X Y -> ~ Included U Y X -> Inhabited U (
Setminus U Y X).
Lemma Strict_super_set_contains_new_element :
forall X Y:
Ensemble U,
Included U X Y -> X <> Y -> Inhabited U (
Setminus U Y X).
Lemma Subtract_intro :
forall (
A:
Ensemble U) (
x y:
U),
In U A y -> x <> y -> In U (
Subtract U A x)
y.
Hint Resolve Subtract_intro :
sets.
Lemma Subtract_inv :
forall (
A:
Ensemble U) (
x y:
U),
In U (
Subtract U A x)
y -> In U A y /\ x <> y.
Lemma Included_Strict_Included :
forall X Y:
Ensemble U,
Included U X Y -> Strict_Included U X Y \/ X = Y.
Lemma Strict_Included_inv :
forall X Y:
Ensemble U,
Strict_Included U X Y -> Included U X Y /\ Inhabited U (
Setminus U Y X).
Lemma not_SIncl_empty :
forall X:
Ensemble U,
~ Strict_Included U X (
Empty_set U).
Lemma Complement_Complement :
forall A:
Ensemble U,
Complement U (
Complement U A)
= A.
End Ensembles_classical.
Hint Resolve Strict_super_set_contains_new_element Subtract_intro
not_SIncl_empty:
sets.