diff options
author | glondu <glondu@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2009-09-17 15:58:14 +0000 |
---|---|---|
committer | glondu <glondu@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2009-09-17 15:58:14 +0000 |
commit | 61ccbc81a2f3b4662ed4a2bad9d07d2003dda3a2 (patch) | |
tree | 961cc88c714aa91a0276ea9fbf8bc53b2b9d5c28 /theories/Sets/Ensembles.v | |
parent | 6d3fbdf36c6a47b49c2a4b16f498972c93c07574 (diff) |
Delete trailing whitespaces in all *.{v,ml*} files
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12337 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/Sets/Ensembles.v')
-rw-r--r-- | theories/Sets/Ensembles.v | 36 |
1 files changed, 18 insertions, 18 deletions
diff --git a/theories/Sets/Ensembles.v b/theories/Sets/Ensembles.v index 339298572..0fa9c74a8 100644 --- a/theories/Sets/Ensembles.v +++ b/theories/Sets/Ensembles.v @@ -28,23 +28,23 @@ 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. |