diff options
Diffstat (limited to 'theories/Sets/Ensembles.v')
| -rw-r--r-- | theories/Sets/Ensembles.v | 103 |
1 files changed, 51 insertions, 52 deletions
diff --git a/theories/Sets/Ensembles.v b/theories/Sets/Ensembles.v index d71c96b0..c38a2fe1 100644 --- a/theories/Sets/Ensembles.v +++ b/theories/Sets/Ensembles.v @@ -24,72 +24,71 @@ (* in Summer 1995. Several developments by E. Ledinot were an inspiration. *) (****************************************************************************) -(*i $Id: Ensembles.v 8642 2006-03-17 10:09:02Z notin $ i*) +(*i $Id: Ensembles.v 9245 2006-10-17 12:53:34Z notin $ i*) Section Ensembles. -Variable U : Type. - -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 := + Variable U : Type. + + 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. + Leibniz equality. - 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)]. *) + 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 := + Inductive Singleton (x:U) : Ensemble := In_singleton : In (Singleton x) x. -Inductive Union (B C:Ensemble) : Ensemble := - | Union_introl : forall x:U, In B x -> In (Union B C) x - | 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 Union (B C:Ensemble) : Ensemble := + | Union_introl : forall x:U, In B x -> In (Union B C) x + | Union_intror : forall x:U, In C x -> In (Union B C) x. -Inductive Intersection (B C:Ensemble) : Ensemble := + 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. - -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 := + forall x:U, In B x -> In C x -> In (Intersection B C) x. + + 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 := + 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 *) -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. -Hint Resolve Extensionality_Ensembles. + Axiom Extensionality_Ensembles : forall A B:Ensemble, Same_set A B -> A = B. End Ensembles. @@ -98,4 +97,4 @@ Hint Unfold In Included Same_set Strict_Included Add Setminus Subtract: sets Hint Resolve Union_introl Union_intror Intersection_intro In_singleton Couple_l Couple_r Triple_l Triple_m Triple_r Disjoint_intro - Extensionality_Ensembles: sets v62.
\ No newline at end of file + Extensionality_Ensembles: sets v62. |