Library Coq.Sets.Classical_sets
Require Export Ensembles.
Require Export Constructive_sets.
Require Export Classical_Type.
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 v62.