diff options
Diffstat (limited to 'theories/Sets/Ensembles.v')
-rw-r--r-- | theories/Sets/Ensembles.v | 38 |
1 files changed, 19 insertions, 19 deletions
diff --git a/theories/Sets/Ensembles.v b/theories/Sets/Ensembles.v index c38a2fe1..0fa9c74a 100644 --- a/theories/Sets/Ensembles.v +++ b/theories/Sets/Ensembles.v @@ -24,27 +24,27 @@ (* in Summer 1995. Several developments by E. Ledinot were an inspiration. *) (****************************************************************************) -(*i $Id: Ensembles.v 9245 2006-10-17 12:53:34Z notin $ i*) +(*i $Id$ i*) Section Ensembles. Variable U : Type. - - Definition Ensemble := U -> Prop. + + Definition Ensemble := U -> Prop. Definition In (A:Ensemble) (x:U) : Prop := A x. - + Definition Included (B C:Ensemble) : Prop := forall x:U, In B x -> In C x. - + Inductive Empty_set : Ensemble :=. - + Inductive Full_set : Ensemble := Full_intro : forall x:U, In Full_set x. -(** NB: The following definition builds-in equality of elements in [U] as - Leibniz equality. +(** NB: The following definition builds-in equality of elements in [U] as + Leibniz equality. - This may have to be changed if we replace [U] by a Setoid on [U] - with its own equality [eqs], with + This may have to be changed if we replace [U] by a Setoid on [U] + with its own equality [eqs], with [In_singleton: (y: U)(eqs x y) -> (In (Singleton x) y)]. *) Inductive Singleton (x:U) : Ensemble := @@ -55,7 +55,7 @@ Section Ensembles. | Union_intror : forall x:U, In C x -> In (Union B C) x. Definition Add (B:Ensemble) (x:U) : Ensemble := Union B (Singleton x). - + Inductive Intersection (B C:Ensemble) : Ensemble := Intersection_intro : forall x:U, In B x -> In C x -> In (Intersection B C) x. @@ -63,29 +63,29 @@ Section Ensembles. Inductive Couple (x y:U) : Ensemble := | Couple_l : In (Couple x y) x | Couple_r : In (Couple x y) y. - + Inductive Triple (x y z:U) : Ensemble := | Triple_l : In (Triple x y z) x | Triple_m : In (Triple x y z) y | Triple_r : In (Triple x y z) z. - + Definition Complement (A:Ensemble) : Ensemble := fun x:U => ~ In A x. - + Definition Setminus (B C:Ensemble) : Ensemble := fun x:U => In B x /\ ~ In C x. - + Definition Subtract (B:Ensemble) (x:U) : Ensemble := Setminus B (Singleton x). - + Inductive Disjoint (B C:Ensemble) : Prop := Disjoint_intro : (forall x:U, ~ In (Intersection B C) x) -> Disjoint B C. Inductive Inhabited (B:Ensemble) : Prop := Inhabited_intro : forall x:U, In B x -> Inhabited B. - + Definition Strict_Included (B C:Ensemble) : Prop := Included B C /\ B <> C. - + Definition Same_set (B C:Ensemble) : Prop := Included B C /\ Included C B. - + (** Extensionality Axiom *) Axiom Extensionality_Ensembles : forall A B:Ensemble, Same_set A B -> A = B. |