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.