Library Coq.Sets.Powerset_Classical_facts
Require Export Ensembles.
Require Export Constructive_sets.
Require Export Relations_1.
Require Export Relations_1_facts.
Require Export Partial_Order.
Require Export Cpo.
Require Export Powerset.
Require Export Powerset_facts.
Require Export Classical_Type.
Require Export Classical_sets.
Section Sets_as_an_algebra.
Variable U :
Type.
Lemma sincl_add_x :
forall (
A B:Ensemble
U) (
x:U),
~
In U A x ->
Strict_Included U (
Add U A x) (
Add U B x) ->
Strict_Included U A B.
Lemma incl_soustr_in :
forall (
X:Ensemble
U) (
x:U),
In U X x ->
Included U (
Subtract U X x)
X.
Lemma incl_soustr :
forall (
X Y:Ensemble
U) (
x:U),
Included U X Y ->
Included U (
Subtract U X x) (
Subtract U Y x).
Lemma incl_soustr_add_l :
forall (
X:Ensemble
U) (
x:U),
Included U (
Subtract U (
Add U X x)
x)
X.
Lemma incl_soustr_add_r :
forall (
X:Ensemble
U) (
x:U),
~
In U X x ->
Included U X (
Subtract U (
Add U X x)
x).
Hint Resolve incl_soustr_add_r:
sets v62.
Lemma add_soustr_2 :
forall (
X:Ensemble
U) (
x:U),
In U X x ->
Included U X (
Add U (
Subtract U X x)
x).
Lemma add_soustr_1 :
forall (
X:Ensemble
U) (
x:U),
In U X x ->
Included U (
Add U (
Subtract U X x)
x)
X.
Lemma add_soustr_xy :
forall (
X:Ensemble
U) (
x y:U),
x <>
y ->
Subtract U (
Add U X x)
y =
Add U (
Subtract U X y)
x.
Lemma incl_st_add_soustr :
forall (
X Y:Ensemble
U) (
x:U),
~
In U X x ->
Strict_Included U (
Add U X x)
Y ->
Strict_Included U X (
Subtract U Y x).
Lemma Sub_Add_new :
forall (
X:Ensemble
U) (
x:U), ~
In U X x ->
X =
Subtract U (
Add U X x)
x.
Lemma Simplify_add :
forall (
X X0:Ensemble
U) (
x:U),
~
In U X x -> ~
In U X0 x ->
Add U X x =
Add U X0 x ->
X =
X0.
Lemma Included_Add :
forall (
X A:Ensemble
U) (
x:U),
Included U X (
Add U A x) ->
Included U X A \/ (
exists A' :
_,
X =
Add U A' x /\
Included U A' A).
Lemma setcover_inv :
forall A x y:Ensemble
U,
covers (
Ensemble U) (
Power_set_PO U A)
y x ->
Strict_Included U x y /\
(
forall z:Ensemble
U,
Included U x z ->
Included U z y ->
x =
z \/
z =
y).
Theorem Add_covers :
forall A a:Ensemble
U,
Included U a A ->
forall x:U,
In U A x ->
~
In U a x ->
covers (
Ensemble U) (
Power_set_PO U A) (
Add U a x)
a.
Theorem covers_Add :
forall A a a':Ensemble
U,
Included U a A ->
Included U a' A ->
covers (
Ensemble U) (
Power_set_PO U A)
a' a ->
exists x :
_,
a' =
Add U a x /\
In U A x /\ ~
In U a x.
Theorem covers_is_Add :
forall A a a':Ensemble
U,
Included U a A ->
Included U a' A ->
(
covers (
Ensemble U) (
Power_set_PO U A)
a' a <->
(
exists x :
_,
a' =
Add U a x /\
In U A x /\ ~
In U a x)).
Theorem Singleton_atomic :
forall (
x:U) (
A:Ensemble
U),
In U A x ->
covers (
Ensemble U) (
Power_set_PO U A) (
Singleton U x) (
Empty_set U).
Lemma less_than_singleton :
forall (
X:Ensemble
U) (
x:U),
Strict_Included U X (
Singleton U x) ->
X =
Empty_set U.
End Sets_as_an_algebra.
Hint Resolve incl_soustr_in:
sets v62.
Hint Resolve incl_soustr:
sets v62.
Hint Resolve incl_soustr_add_l:
sets v62.
Hint Resolve incl_soustr_add_r:
sets v62.
Hint Resolve add_soustr_1 add_soustr_2:
sets v62.
Hint Resolve add_soustr_xy:
sets v62.