diff options
Diffstat (limited to 'theories/Classes/Functions.v')
| -rw-r--r-- | theories/Classes/Functions.v | 14 |
1 files changed, 7 insertions, 7 deletions
diff --git a/theories/Classes/Functions.v b/theories/Classes/Functions.v index 28fa55ee1..4750df639 100644 --- a/theories/Classes/Functions.v +++ b/theories/Classes/Functions.v @@ -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 [ m : Morphism (A -> B) (RA ++> RB) f ] => Injective : 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 [ m : Morphism (A -> B) (eqA ++> eqB) ] => MonoMorphism := monic :> Injective m. -Class [ m : ! Morphism (A -> B) (eqA ++> eqB) ] => EpiMorphism := +Class [ m : Morphism (A -> B) (eqA ++> eqB) ] => EpiMorphism := epic :> Surjective m. -Class [ m : ! Morphism (A -> B) (eqA ++> eqB) ] => IsoMorphism := +Class [ m : Morphism (A -> B) (eqA ++> eqB) ] => IsoMorphism := 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. |