Library Coq.Sets.Powerset
Require Export Ensembles.
Require Export Relations_1.
Require Export Relations_1_facts.
Require Export Partial_Order.
Require Export Cpo.
Section The_power_set_partial_order.
Variable U :
Type.
Inductive Power_set (
A:
Ensemble U) :
Ensemble (
Ensemble U) :=
Definition_of_Power_set :
forall X:
Ensemble U,
Included U X A -> In (
Ensemble U) (
Power_set A)
X.
Hint Resolve Definition_of_Power_set :
core.
Theorem Empty_set_minimal :
forall X:
Ensemble U,
Included U (
Empty_set U)
X.
Hint Resolve Empty_set_minimal :
core.
Theorem Power_set_Inhabited :
forall X:
Ensemble U,
Inhabited (
Ensemble U) (
Power_set X).
Hint Resolve Power_set_Inhabited :
core.
Theorem Inclusion_is_an_order :
Order (
Ensemble U) (
Included U).
Hint Resolve Inclusion_is_an_order :
core.
Theorem Inclusion_is_transitive :
Transitive (
Ensemble U) (
Included U).
Hint Resolve Inclusion_is_transitive :
core.
Definition Power_set_PO :
Ensemble U -> PO (
Ensemble U).
Defined.
Hint Unfold Power_set_PO :
core.
Theorem Strict_Rel_is_Strict_Included :
same_relation (
Ensemble U) (
Strict_Included U)
(
Strict_Rel_of (
Ensemble U) (
Power_set_PO (
Full_set U))).
Hint Resolve Strict_Rel_Transitive Strict_Rel_is_Strict_Included :
core.
Lemma Strict_inclusion_is_transitive_with_inclusion :
forall x y z:
Ensemble U,
Strict_Included U x y -> Included U y z -> Strict_Included U x z.
Lemma Strict_inclusion_is_transitive_with_inclusion_left :
forall x y z:
Ensemble U,
Included U x y -> Strict_Included U y z -> Strict_Included U x z.
Lemma Strict_inclusion_is_transitive :
Transitive (
Ensemble U) (
Strict_Included U).
Theorem Empty_set_is_Bottom :
forall A:
Ensemble U,
Bottom (
Ensemble U) (
Power_set_PO A) (
Empty_set U).
Hint Resolve Empty_set_is_Bottom :
core.
Theorem Union_minimal :
forall a b X:
Ensemble U,
Included U a X -> Included U b X -> Included U (
Union U a b)
X.
Hint Resolve Union_minimal :
core.
Theorem Intersection_maximal :
forall a b X:
Ensemble U,
Included U X a -> Included U X b -> Included U X (
Intersection U a b).
Theorem Union_increases_l :
forall a b:
Ensemble U,
Included U a (
Union U a b).
Theorem Union_increases_r :
forall a b:
Ensemble U,
Included U b (
Union U a b).
Theorem Intersection_decreases_l :
forall a b:
Ensemble U,
Included U (
Intersection U a b)
a.
Theorem Intersection_decreases_r :
forall a b:
Ensemble U,
Included U (
Intersection U a b)
b.
Hint Resolve Union_increases_l Union_increases_r Intersection_decreases_l
Intersection_decreases_r :
core.
Theorem Union_is_Lub :
forall A a b:
Ensemble U,
Included U a A ->
Included U b A ->
Lub (
Ensemble U) (
Power_set_PO A) (
Couple (
Ensemble U)
a b) (
Union U a b).
Theorem Intersection_is_Glb :
forall A a b:
Ensemble U,
Included U a A ->
Included U b A ->
Glb (
Ensemble U) (
Power_set_PO A) (
Couple (
Ensemble U)
a b)
(
Intersection U a b).
End The_power_set_partial_order.
Hint Resolve Empty_set_minimal:
sets.
Hint Resolve Power_set_Inhabited:
sets.
Hint Resolve Inclusion_is_an_order:
sets.
Hint Resolve Inclusion_is_transitive:
sets.
Hint Resolve Union_minimal:
sets.
Hint Resolve Union_increases_l:
sets.
Hint Resolve Union_increases_r:
sets.
Hint Resolve Intersection_decreases_l:
sets.
Hint Resolve Intersection_decreases_r:
sets.
Hint Resolve Empty_set_is_Bottom:
sets.
Hint Resolve Strict_inclusion_is_transitive:
sets.