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.