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.