Library Coq.Sets.Powerset_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.
Section Sets_as_an_algebra.
Variable U :
Type.
Theorem Empty_set_zero :
forall X:
Ensemble U,
Union U (
Empty_set U)
X = X.
Theorem Empty_set_zero' :
forall x:
U,
Add U (
Empty_set U)
x = Singleton U x.
Lemma less_than_empty :
forall X:
Ensemble U,
Included U X (
Empty_set U) ->
X = Empty_set U.
Theorem Union_commutative :
forall A B:
Ensemble U,
Union U A B = Union U B A.
Theorem Union_associative :
forall A B C:
Ensemble U,
Union U (
Union U A B)
C = Union U A (
Union U B C).
Theorem Union_idempotent :
forall A:
Ensemble U,
Union U A A = A.
Lemma Union_absorbs :
forall A B:
Ensemble U,
Included U B A ->
Union U A B = A.
Theorem Couple_as_union :
forall x y:
U,
Union U (
Singleton U x) (
Singleton U y)
= Couple U x y.
Theorem Triple_as_union :
forall x y z:
U,
Union U (
Union U (
Singleton U x) (
Singleton U y)) (
Singleton U z)
=
Triple U x y z.
Theorem Triple_as_Couple :
forall x y:
U,
Couple U x y = Triple U x x y.
Theorem Triple_as_Couple_Singleton :
forall x y z:
U,
Triple U x y z = Union U (
Couple U x y) (
Singleton U z).
Theorem Intersection_commutative :
forall A B:
Ensemble U,
Intersection U A B = Intersection U B A.
Theorem Distributivity :
forall A B C:
Ensemble U,
Intersection U A (
Union U B C)
=
Union U (
Intersection U A B) (
Intersection U A C).
Theorem Distributivity' :
forall A B C:
Ensemble U,
Union U A (
Intersection U B C)
=
Intersection U (
Union U A B) (
Union U A C).
Theorem Union_add :
forall (
A B:
Ensemble U) (
x:
U),
Add U (
Union U A B)
x = Union U A (
Add U B x).
Theorem Non_disjoint_union :
forall (
X:
Ensemble U) (
x:
U),
In U X x ->
Add U X x = X.
Theorem Non_disjoint_union' :
forall (
X:
Ensemble U) (
x:
U),
~ In U X x ->
Subtract U X x = X.
Lemma singlx :
forall x y:
U,
In U (
Add U (
Empty_set U)
x)
y ->
x = y.
Lemma incl_add :
forall (
A B:
Ensemble U) (
x:
U),
Included U A B ->
Included U (
Add U A x) (
Add U B x).
Lemma incl_add_x :
forall (
A B:
Ensemble U) (
x:
U),
~ In U A x ->
Included U (
Add U A x) (
Add U B x) ->
Included U A B.
Lemma Add_commutative :
forall (
A:
Ensemble U) (
x y:
U),
Add U (
Add U A x)
y = Add U (
Add U A y)
x.
Lemma Add_commutative' :
forall (
A:
Ensemble U) (
x y z:
U),
Add U (
Add U (
Add U A x)
y)
z = Add U (
Add U (
Add U A z)
x)
y.
Lemma Add_distributes :
forall (
A B:
Ensemble U) (
x y:
U),
Included U B A ->
Add U (
Add U A x)
y = Union U (
Add U A x) (
Add U B y).
Lemma setcover_intro :
forall (
U:
Type) (
A x y:
Ensemble U),
Strict_Included U x y ->
~ (exists z :
_, Strict_Included U x z /\ Strict_Included U z y) ->
covers (
Ensemble U) (
Power_set_PO U A)
y x.
End Sets_as_an_algebra.
Hint Resolve Empty_set_zero Empty_set_zero' Union_associative Union_add
singlx incl_add:
sets v62.