environ
vocabularies HIDDEN, XBOOLE_0, ORDERS_2, YELLOW_0, NEWTON, ZFMISC_1, FUNCT_1, WAYBEL27, FUNCT_2, RELAT_1, STRUCT_0, SUBSET_1, FUNCOP_1, FUNCT_5, TARSKI, CAT_1, SEQM_3, XXREAL_0, PRE_TOPC, SETFAM_1, WAYBEL11, WAYBEL_0, WAYBEL19, WAYBEL24, EQREL_1, ORDINAL2, RCOMP_1, WAYBEL26, XBOOLEAN, CARD_3, LATTICE3, WAYBEL_9, FUNCTOR0, REWRITE1, YELLOW_9, YELLOW16, WAYBEL_3, PBOOLE, LATTICES, FINSET_1, FUNCT_4, RELAT_2, WAYBEL25, PRELAMB, CARD_FIL, YELLOW_1, T_0TOPSP, CONNSP_2, WELLORD1, LATTICE5, WAYBEL18, CARD_1, FUNCT_3, PROB_1, FUNCT_6, RLVECT_2, WELLORD2, RLVECT_3, TOPS_1, YELLOW_6, WAYBEL29;
notations HIDDEN, TARSKI, XBOOLE_0, ENUMSET1, ZFMISC_1, XTUPLE_0, SUBSET_1, SETFAM_1, RELAT_1, FUNCT_1, PBOOLE, RELSET_1, PARTFUN1, FUNCT_2, BINOP_1, FUNCT_3, FINSET_1, CARD_3, ORDINAL1, NUMBERS, FUNCT_6, FUNCOP_1, ORDERS_1, STRUCT_0, PRE_TOPC, TOPS_1, T_0TOPSP, CONNSP_2, CANTOR_1, FUNCT_4, FUNCT_5, FUNCT_7, PRALG_1, WELLORD1, ORDERS_2, LATTICE3, TOPS_2, YELLOW_0, WAYBEL_0, YELLOW_1, WAYBEL_1, YELLOW_3, WAYBEL_3, WAYBEL_5, WAYBEL_9, YELLOW_6, WAYBEL11, YELLOW_9, BORSUK_1, WAYBEL18, WAYBEL19, WAYBEL24, WAYBEL25, YELLOW16, WAYBEL26, WAYBEL27;
definitions TARSKI, RELAT_1, LATTICE3, YELLOW_0, WAYBEL_0, WAYBEL_1, WAYBEL_3, PRE_TOPC, WAYBEL11, WAYBEL27, XBOOLE_0;
theorems TARSKI, ZFMISC_1, GRCAT_1, WELLORD2, SETFAM_1, ENUMSET1, RELAT_1, FUNCT_1, FUNCT_2, FUNCT_3, FUNCT_5, PRE_TOPC, TOPS_1, TOPS_2, CONNSP_2, CANTOR_1, FUNCT_4, FUNCT_7, FINSET_1, BORSUK_1, FUNCOP_1, CARD_3, ORDERS_2, YELLOW_0, YELLOW_1, YELLOW_2, YELLOW_3, YELLOW_9, YELLOW12, YELLOW14, YELLOW16, WAYBEL_0, WAYBEL_3, WAYBEL_8, WAYBEL11, WAYBEL13, WAYBEL15, WAYBEL17, WAYBEL18, WAYBEL20, WAYBEL21, WAYBEL24, WAYBEL25, WAYBEL26, WAYBEL27, XBOOLE_0, XBOOLE_1, FUNCT_6, PARTFUN1, XTUPLE_0;
schemes FUNCT_1, PBOOLE;
registrations SUBSET_1, FUNCT_1, FUNCT_2, FUNCOP_1, FINSET_1, STRUCT_0, PRE_TOPC, TOPS_1, BORSUK_1, LATTICE3, YELLOW_0, BORSUK_2, WAYBEL_0, YELLOW_1, WAYBEL_1, YELLOW_3, WAYBEL_3, WAYBEL10, WAYBEL11, WAYBEL14, YELLOW_9, WAYBEL18, WAYBEL19, TOPGRP_1, WAYBEL24, YELLOW14, WAYBEL25, YELLOW16, WAYBEL26, WAYBEL27, ZFMISC_1, RELSET_1, FUNCT_5;
constructors HIDDEN, TOLER_1, FUNCT_7, TOPS_1, TOPS_2, BORSUK_1, T_0TOPSP, CANTOR_1, MONOID_0, ORDERS_3, WAYBEL_5, WAYBEL11, YELLOW_9, WAYBEL18, WAYBEL24, YELLOW16, WAYBEL26, WAYBEL27, WAYBEL20, XTUPLE_0;
requirements HIDDEN, BOOLE, SUBSET;
equalities RELAT_1, WAYBEL_3, WAYBEL11, XBOOLE_0, BINOP_1, STRUCT_0, ORDINAL1;
expansions TARSKI, LATTICE3, WAYBEL_0, WAYBEL_1, WAYBEL_3, PRE_TOPC, WAYBEL11, WAYBEL27, XBOOLE_0;
theorem Th10:
for
S1,
S2 being
TopStruct st
TopStruct(# the
carrier of
S1, the
topology of
S1 #)
= TopStruct(# the
carrier of
S2, the
topology of
S2 #) holds
for
T1,
T2 being non
empty TopRelStr st
TopRelStr(# the
carrier of
T1, the
InternalRel of
T1, the
topology of
T1 #)
= TopRelStr(# the
carrier of
T2, the
InternalRel of
T2, the
topology of
T2 #) holds
ContMaps (
S1,
T1)
= ContMaps (
S2,
T2)
definition
let X,
Y be non
empty TopSpace;
existence
ex b1 being Function of (InclPoset the topology of [:X,Y:]),(ContMaps (X,(Sigma (InclPoset the topology of Y)))) st
for W being open Subset of [:X,Y:] holds b1 . W = (W, the carrier of X) *graph
correctness
uniqueness
for b1, b2 being Function of (InclPoset the topology of [:X,Y:]),(ContMaps (X,(Sigma (InclPoset the topology of Y)))) st ( for W being open Subset of [:X,Y:] holds b1 . W = (W, the carrier of X) *graph ) & ( for W being open Subset of [:X,Y:] holds b2 . W = (W, the carrier of X) *graph ) holds
b1 = b2;
end;
defpred S1[ T_0-TopSpace] means for X being non empty TopSpace
for L being Scott continuous complete TopLattice
for T being Scott TopAugmentation of ContMaps ($1,L) ex f being Function of (ContMaps (X,T)),(ContMaps ([:X,$1:],L)) ex g being Function of (ContMaps ([:X,$1:],L)),(ContMaps (X,T)) st
( f is uncurrying & f is V7() & f is onto & g is currying & g is V7() & g is onto );
defpred S2[ T_0-TopSpace] means for X being non empty TopSpace
for L being Scott continuous complete TopLattice
for T being Scott TopAugmentation of ContMaps ($1,L) ex f being Function of (ContMaps (X,T)),(ContMaps ([:X,$1:],L)) ex g being Function of (ContMaps ([:X,$1:],L)),(ContMaps (X,T)) st
( f is uncurrying & f is isomorphic & g is currying & g is isomorphic );
defpred S3[ T_0-TopSpace] means for X being non empty TopSpace holds Theta (X,$1) is isomorphic ;
defpred S4[ T_0-TopSpace] means for X being non empty TopSpace
for T being Scott TopAugmentation of InclPoset the topology of $1
for f being continuous Function of X,T holds *graph f is open Subset of [:X,$1:];
defpred S5[ T_0-TopSpace] means for T being Scott TopAugmentation of InclPoset the topology of $1 holds { [W,y] where W is open Subset of $1, y is Element of $1 : y in W } is open Subset of [:T,$1:];
defpred S6[ T_0-TopSpace] means for S being Scott TopAugmentation of InclPoset the topology of $1
for y being Element of $1
for V being open a_neighborhood of y ex H being open Subset of S st
( V in H & meet H is a_neighborhood of y );
Lm1:
for T being T_0-TopSpace holds
( S1[T] iff S2[T] )
definition
let M be non
empty set ;
let X,
Y be non
empty TopSpace;
uniqueness
for b1, b2 being Function of (oContMaps (X,(M -TOP_prod (M => Y)))),((oContMaps (X,Y)) |^ M) st ( for f being continuous Function of X,(M -TOP_prod (M => Y)) holds b1 . f = commute f ) & ( for f being continuous Function of X,(M -TOP_prod (M => Y)) holds b2 . f = commute f ) holds
b1 = b2
existence
ex b1 being Function of (oContMaps (X,(M -TOP_prod (M => Y)))),((oContMaps (X,Y)) |^ M) st
for f being continuous Function of X,(M -TOP_prod (M => Y)) holds b1 . f = commute f
end;
Lm2:
for T being T_0-TopSpace st S3[T] holds
S4[T]
Lm3:
for T being T_0-TopSpace st S4[T] holds
S3[T]
Lm4:
for T being T_0-TopSpace st S4[T] holds
S5[T]
Lm5:
for T being T_0-TopSpace st S5[T] holds
S6[T]
Lm6:
for T being T_0-TopSpace st S6[T] holds
S4[T]
Lm7:
for T being T_0-TopSpace st S6[T] holds
InclPoset the topology of T is continuous
Lm8:
for T being T_0-TopSpace st InclPoset the topology of T is continuous holds
S6[T]
theorem
for
Y being
T_0-TopSpace holds
( ( for
X being non
empty TopSpace for
L being
Scott continuous complete TopLattice for
T being
Scott TopAugmentation of
ContMaps (
Y,
L) ex
f being
Function of
(ContMaps (X,T)),
(ContMaps ([:X,Y:],L)) ex
g being
Function of
(ContMaps ([:X,Y:],L)),
(ContMaps (X,T)) st
(
f is
uncurrying &
f is
V7() &
f is
onto &
g is
currying &
g is
V7() &
g is
onto ) ) iff for
X being non
empty TopSpace for
L being
Scott continuous complete TopLattice for
T being
Scott TopAugmentation of
ContMaps (
Y,
L) ex
f being
Function of
(ContMaps (X,T)),
(ContMaps ([:X,Y:],L)) ex
g being
Function of
(ContMaps ([:X,Y:],L)),
(ContMaps (X,T)) st
(
f is
uncurrying &
f is
isomorphic &
g is
currying &
g is
isomorphic ) )
by Lm1;
defpred S7[ complete LATTICE] means InclPoset (sigma $1) is continuous ;
defpred S8[ complete LATTICE] means for SL being Scott TopAugmentation of $1
for S being complete LATTICE
for SS being Scott TopAugmentation of S holds sigma [:S,$1:] = the topology of [:SS,SL:];
defpred S9[ complete LATTICE] means for SL being Scott TopAugmentation of $1
for S being complete LATTICE
for SS being Scott TopAugmentation of S
for SSL being Scott TopAugmentation of [:S,$1:] holds TopStruct(# the carrier of SSL, the topology of SSL #) = [:SS,SL:];
Lm9:
for L being complete LATTICE holds
( S8[L] iff S9[L] )
Lm10:
for L being complete LATTICE st S7[L] holds
S8[L]
Lm11:
for L being complete LATTICE st S8[L] holds
S7[L]