environ
vocabularies HIDDEN, PRE_TOPC, WAYBEL18, CARD_1, RCOMP_1, STRUCT_0, SUBSET_1, XBOOLE_0, TARSKI, REWRITE1, WAYBEL11, WAYBEL_9, FUNCTOR0, T_0TOPSP, YELLOW_9, CARD_3, FUNCOP_1, YELLOW_1, RELAT_1, RLVECT_2, FUNCT_1, ZFMISC_1, ORDERS_2, WAYBEL_0, CAT_1, TOPS_2, WELLORD1, ORDINAL2, GROUP_6, WAYBEL_1, FUNCT_3, BORSUK_1, EQREL_1, XXREAL_0, LATTICE3, YELLOW_0, WAYBEL_3, RELAT_2, PROB_1, BINOP_1, SEQM_3, WAYBEL24, FUNCT_2, NEWTON, FUNCT_6, YELLOW_2, ORDINAL1, CONNSP_2, TOPS_1, SEQ_2, YELLOW_8, SETFAM_1, WAYBEL25;
notations HIDDEN, TARSKI, XBOOLE_0, ENUMSET1, ZFMISC_1, SUBSET_1, RELAT_1, FUNCT_1, RELSET_1, PARTFUN1, FUNCT_2, ORDINAL1, NUMBERS, FUNCT_3, NATTRA_1, TOLER_1, QUANTAL1, CARD_3, PRALG_1, FUNCT_6, FUNCOP_1, WAYBEL18, DOMAIN_1, STRUCT_0, PRE_TOPC, CONNSP_2, TOPS_1, TOPS_2, COMPTS_1, BORSUK_1, TMAP_1, T_0TOPSP, BORSUK_3, ORDERS_2, LATTICE3, YELLOW_0, WAYBEL_0, YELLOW_2, WAYBEL_1, WAYBEL_2, YELLOW_6, WAYBEL_3, YELLOW_8, WAYBEL_9, WAYBEL11, YELLOW_9, WAYBEL17, YELLOW_1, WAYBEL24, YELLOW14;
definitions TARSKI, XBOOLE_0, PRE_TOPC, TOPS_2, ORDERS_2, RELAT_1, RELAT_2, STRUCT_0, WAYBEL_1, T_0TOPSP, WAYBEL18, LATTICE3, YELLOW_6, WAYBEL_0, WAYBEL_9, YELLOW14;
theorems TARSKI, PRE_TOPC, ZFMISC_1, ORDERS_2, T_0TOPSP, FUNCT_1, FUNCT_2, QUANTAL1, RELAT_1, FINSEQ_5, TEX_1, PRALG_1, FUNCOP_1, CARD_3, BORSUK_1, WAYBEL14, TOPS_1, TOPS_2, TOPS_3, YELLOW_0, YELLOW_1, YELLOW_2, YELLOW_4, YELLOW_6, YELLOW_9, YELLOW12, WAYBEL_0, WAYBEL_1, WAYBEL_2, WAYBEL_7, WAYBEL_9, WAYBEL11, WAYBEL10, WAYBEL13, WAYBEL15, WAYBEL17, WAYBEL18, WAYBEL20, WAYBEL24, CONNSP_2, WAYBEL_3, FUNCT_5, WAYBEL_8, TSEP_1, EQUATION, TOPGRP_1, WAYBEL21, ENUMSET1, YELLOW14, RELSET_1, XBOOLE_0, XBOOLE_1, FUNCT_6, YELLOW_8, PARTFUN1;
schemes FUNCT_2, RELSET_1;
registrations XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1, FUNCT_2, FUNCOP_1, STRUCT_0, PRE_TOPC, TOPS_1, BORSUK_1, LATTICE3, YELLOW_0, TEX_1, TSP_1, BORSUK_2, WAYBEL_0, YELLOW_1, WAYBEL_1, WAYBEL_2, WAYBEL_3, WAYBEL_8, WAYBEL10, WAYBEL17, YELLOW_9, WAYBEL18, WAYBEL19, WAYBEL21, WAYBEL24, YELLOW14, RELSET_1;
constructors HIDDEN, TOLER_1, FUNCT_6, TOPS_1, TOPS_2, NATTRA_1, BORSUK_1, TMAP_1, CANTOR_1, MONOID_0, QUANTAL1, ORDERS_3, WAYBEL_1, WAYBEL_8, YELLOW_8, WAYBEL17, YELLOW_9, BORSUK_3, WAYBEL24, YELLOW14, COMPTS_1, WAYBEL_2;
requirements HIDDEN, SUBSET, BOOLE, NUMERALS;
equalities SUBSET_1, RELAT_1, STRUCT_0, WAYBEL18, WAYBEL_0, YELLOW_2, WELLORD1;
expansions TARSKI, XBOOLE_0, PRE_TOPC, TOPS_2, ORDERS_2, WAYBEL_1, T_0TOPSP, WAYBEL18, LATTICE3, WAYBEL_0, WAYBEL_9, YELLOW_2;
definition
let T be
TopStruct ;
existence
ex b1 being strict TopRelStr st
( TopStruct(# the carrier of b1, the topology of b1 #) = TopStruct(# the carrier of T, the topology of T #) & ( for x, y being Element of b1 holds
( x <= y iff ex Y being Subset of T st
( Y = {y} & x in Cl Y ) ) ) )
uniqueness
for b1, b2 being strict TopRelStr st TopStruct(# the carrier of b1, the topology of b1 #) = TopStruct(# the carrier of T, the topology of T #) & ( for x, y being Element of b1 holds
( x <= y iff ex Y being Subset of T st
( Y = {y} & x in Cl Y ) ) ) & TopStruct(# the carrier of b2, the topology of b2 #) = TopStruct(# the carrier of T, the topology of T #) & ( for x, y being Element of b2 holds
( x <= y iff ex Y being Subset of T st
( Y = {y} & x in Cl Y ) ) ) holds
b1 = b2
end;
Lm1:
for T being TopStruct holds the carrier of T = the carrier of (Omega T)
Lm2:
for T being TopStruct
for x, y being Element of T
for X, Y being Subset of T st X = {x} & Y = {y} holds
( x in Cl Y iff Cl X c= Cl Y )
Lm3:
for S, T being non empty RelStr
for f being Function of S,S
for g being Function of T,T st RelStr(# the carrier of S, the InternalRel of S #) = RelStr(# the carrier of T, the InternalRel of T #) & f = g & f is projection holds
g is projection
by WAYBEL_9:1;
Lm4:
now for X, Y being non empty TopSpace
for N being net of ContMaps (X,(Omega Y)) holds the mapping of N in Funcs ( the carrier of N,(Funcs ( the carrier of X, the carrier of Y)))
let X,
Y be non
empty TopSpace;
for N being net of ContMaps (X,(Omega Y)) holds the mapping of N in Funcs ( the carrier of N,(Funcs ( the carrier of X, the carrier of Y)))let N be
net of
ContMaps (
X,
(Omega Y));
the mapping of N in Funcs ( the carrier of N,(Funcs ( the carrier of X, the carrier of Y)))A1:
the
carrier of
Y = the
carrier of
(Omega Y)
by Lm1;
the
carrier of
(ContMaps (X,(Omega Y))) c= Funcs ( the
carrier of
X, the
carrier of
Y)
then A2:
Funcs ( the
carrier of
N, the
carrier of
(ContMaps (X,(Omega Y))))
c= Funcs ( the
carrier of
N,
(Funcs ( the carrier of X, the carrier of Y)))
by FUNCT_5:56;
the
mapping of
N in Funcs ( the
carrier of
N, the
carrier of
(ContMaps (X,(Omega Y))))
by FUNCT_2:8;
hence
the
mapping of
N in Funcs ( the
carrier of
N,
(Funcs ( the carrier of X, the carrier of Y)))
by A2;
verum
end;
Lm5:
now for X, Y being non empty TopSpace
for N being net of ContMaps (X,(Omega Y))
for i being Element of N holds
( the mapping of N . i is Function of X,(Omega Y) & the mapping of N . i is Function of X,Y )
let X,
Y be non
empty TopSpace;
for N being net of ContMaps (X,(Omega Y))
for i being Element of N holds
( the mapping of N . i is Function of X,(Omega Y) & the mapping of N . i is Function of X,Y )let N be
net of
ContMaps (
X,
(Omega Y));
for i being Element of N holds
( the mapping of N . i is Function of X,(Omega Y) & the mapping of N . i is Function of X,Y )let i be
Element of
N;
( the mapping of N . i is Function of X,(Omega Y) & the mapping of N . i is Function of X,Y )thus
the
mapping of
N . i is
Function of
X,
(Omega Y)
by WAYBEL24:21;
the mapping of N . i is Function of X,Y
the
carrier of
Y = the
carrier of
(Omega Y)
by Lm1;
hence
the
mapping of
N . i is
Function of
X,
Y
by WAYBEL24:21;
verum
end;
Lm6:
now for X, Y being non empty TopSpace
for N being net of ContMaps (X,(Omega Y))
for x being Point of X holds dom the mapping of N = dom the mapping of (commute (N,x,(Omega Y)))
let X,
Y be non
empty TopSpace;
for N being net of ContMaps (X,(Omega Y))
for x being Point of X holds dom the mapping of N = dom the mapping of (commute (N,x,(Omega Y)))let N be
net of
ContMaps (
X,
(Omega Y));
for x being Point of X holds dom the mapping of N = dom the mapping of (commute (N,x,(Omega Y)))let x be
Point of
X;
dom the mapping of N = dom the mapping of (commute (N,x,(Omega Y)))
ContMaps (
X,
(Omega Y)) is
SubRelStr of
(Omega Y) |^ the
carrier of
X
by WAYBEL24:def 3;
then
the
carrier of
(ContMaps (X,(Omega Y))) c= the
carrier of
((Omega Y) |^ the carrier of X)
by YELLOW_0:def 13;
then A1:
RelStr(# the
carrier of
N, the
InternalRel of
N #)
= RelStr(# the
carrier of
(commute (N,x,(Omega Y))), the
InternalRel of
(commute (N,x,(Omega Y))) #)
by Def3;
thus dom the
mapping of
N =
the
carrier of
N
by FUNCT_2:def 1
.=
dom the
mapping of
(commute (N,x,(Omega Y)))
by A1, FUNCT_2:def 1
;
verum
end;
:: p.124 theorem 3.8 (i, part a)
:: p.126 exercise 3.14