diff options
| author |  Stephane Glondu <steph@glondu.net> | 2008-08-08 13:18:42 +0200 |
|---|---|---|
| committer | Stephane Glondu <steph@glondu.net> | 2008-08-08 13:18:42 +0200 |
| commit | 870075f34dd9fa5792bfbf413afd3b96f17e76a0 (patch) | |
| tree | 0c647056de1832cf1dba5ba58758b9121418e4be /theories/Classes/Functions.v | |
| parent | a0cfa4f118023d35b767a999d5a2ac4b082857b4 (diff) | |
Imported Upstream version 8.2~beta4+dfsgupstream/8.2.beta4+dfsg
Diffstat (limited to 'theories/Classes/Functions.v')
| -rw-r--r-- | theories/Classes/Functions.v | 16 |
1 files changed, 8 insertions, 8 deletions
diff --git a/theories/Classes/Functions.v b/theories/Classes/Functions.v index 49fc4f89..4c844911 100644 --- a/theories/Classes/Functions.v +++ b/theories/Classes/Functions.v @@ -13,7 +13,7 @@ Institution: LRI, CNRS UMR 8623 - UniversitĂcopyright Paris Sud 91405 Orsay, France *) -(* $Id: Functions.v 10739 2008-04-01 14:45:20Z herbelin $ *) +(* $Id: Functions.v 11282 2008-07-28 11:51:53Z msozeau $ *) Require Import Coq.Classes.RelationClasses. Require Import Coq.Classes.Morphisms. @@ -21,22 +21,22 @@ Require Import Coq.Classes.Morphisms. Set Implicit Arguments. Unset Strict Implicit. -Class [ m : Morphism (A -> B) (RA ++> RB) f ] => Injective : Prop := +Class Injective ((m : Morphism (A -> B) (RA ++> RB) f)) : Prop := injective : forall x y : A, RB (f x) (f y) -> RA x y. -Class [ m : Morphism (A -> B) (RA ++> RB) f ] => Surjective : Prop := +Class ((m : Morphism (A -> B) (RA ++> RB) f)) => Surjective : Prop := surjective : forall y, exists x : A, RB y (f x). -Definition Bijective [ m : Morphism (A -> B) (RA ++> RB) (f : A -> B) ] := +Definition Bijective ((m : Morphism (A -> B) (RA ++> RB) (f : A -> B))) := Injective m /\ Surjective m. -Class [ m : Morphism (A -> B) (eqA ++> eqB) ] => MonoMorphism := +Class MonoMorphism (( m : Morphism (A -> B) (eqA ++> eqB) )) := monic :> Injective m. -Class [ m : Morphism (A -> B) (eqA ++> eqB) ] => EpiMorphism := +Class EpiMorphism ((m : Morphism (A -> B) (eqA ++> eqB))) := epic :> Surjective m. -Class [ m : Morphism (A -> B) (eqA ++> eqB) ] => IsoMorphism := +Class IsoMorphism ((m : Morphism (A -> B) (eqA ++> eqB))) := monomorphism :> MonoMorphism m ; epimorphism :> EpiMorphism m. -Class [ m : Morphism (A -> A) (eqA ++> eqA), ! IsoMorphism m ] => AutoMorphism. +Class ((m : Morphism (A -> A) (eqA ++> eqA))) [ ! IsoMorphism m ] => AutoMorphism. |