#A; #U; #V; #x; #x'; #H; #p; napply (. (H^-1‡#)); nassumption.
nqed.
*)
+*)
ndefinition image: ∀A,B. (carr A → carr B) → Ω^A → Ω^B ≝
λA,B:setoid.λf:carr A → carr B.λSa:Ω^A.
nqed.
ndefinition surjective ≝
- λA,B.λS: qpowerclass A.λT: qpowerclass B.λf:unary_morphism A B.
+ λA,B.λS: ext_powerclass A.λT: ext_powerclass B.λf:unary_morphism A B.
∀y. y ∈ T → ∃x. x ∈ S ∧ f x = y.
ndefinition injective ≝
- λA,B.λS: qpowerclass A.λf:unary_morphism A B.
+ λA,B.λS: ext_powerclass A.λf:unary_morphism A B.
∀x,x'. x ∈ S → x' ∈ S → f x = f x' → x = x'.
nlemma first_omomorphism_theorem_functions2:
#A; #B; #f; nwhd; #x; #x'; #Hx; #Hx'; #K; nassumption.
nqed.
-nrecord isomorphism (A, B : setoid) (S: qpowerclass A) (T: qpowerclass B) : Type[0] ≝
+nrecord isomorphism (A, B : setoid) (S: ext_powerclass A) (T: ext_powerclass B) : Type[0] ≝
{ iso_f:> unary_morphism A B;
f_closed: ∀x. x ∈ S → iso_f x ∈ T;
f_sur: surjective … S T iso_f;
;
}.
*)
-*)
\ No newline at end of file