let T be TopSpace; for n being non zero Nat
for F being Element of n -tuples_on (Funcs ( the carrier of T, the carrier of R^1)) st ( for i being Nat st i in dom F holds
for h being Function of T,R^1 st h = F . i holds
h is continuous ) holds
<:F:> is continuous
let n be non zero Nat; for F being Element of n -tuples_on (Funcs ( the carrier of T, the carrier of R^1)) st ( for i being Nat st i in dom F holds
for h being Function of T,R^1 st h = F . i holds
h is continuous ) holds
<:F:> is continuous
let F be Element of n -tuples_on (Funcs ( the carrier of T, the carrier of R^1)); ( ( for i being Nat st i in dom F holds
for h being Function of T,R^1 st h = F . i holds
h is continuous ) implies <:F:> is continuous )
assume A1:
for i being Nat st i in dom F holds
for h being Function of T,R^1 st h = F . i holds
h is continuous
; <:F:> is continuous
set TR = TOP-REAL n;
set FF = <:F:>;
A2:
for Y being Subset of (TOP-REAL n) st Y is open holds
<:F:> " Y is open
proof
let Y be
Subset of
(TOP-REAL n);
( Y is open implies <:F:> " Y is open )
set E =
Euclid n;
A3:
TopStruct(# the
carrier of
(TOP-REAL n), the
topology of
(TOP-REAL n) #)
= TopSpaceMetr (Euclid n)
by EUCLID:def 8;
then reconsider YY =
Y as
Subset of
(TopSpaceMetr (Euclid n)) ;
assume
Y is
open
;
<:F:> " Y is open
then
Y in the
topology of
(TOP-REAL n)
;
then reconsider YY =
YY as
open Subset of
(TopSpaceMetr (Euclid n)) by PRE_TOPC:def 2, A3;
A4:
dom <:F:> = the
carrier of
T
by FUNCT_2:def 1;
for
x being
set holds
(
x in <:F:> " Y iff ex
Q being
Subset of
T st
(
Q is
open &
Q c= <:F:> " Y &
x in Q ) )
proof
let x be
set ;
( x in <:F:> " Y iff ex Q being Subset of T st
( Q is open & Q c= <:F:> " Y & x in Q ) )
len F = n
by CARD_1:def 7;
then A5:
dom F = Seg n
by FINSEQ_1:def 3;
hereby ( ex Q being Subset of T st
( Q is open & Q c= <:F:> " Y & x in Q ) implies x in <:F:> " Y )
assume A6:
x in <:F:> " Y
;
ex M being Element of bool the carrier of T st
( M is open & M c= <:F:> " Y & x in M )then A7:
<:F:> . x in Y
by FUNCT_1:def 7;
then reconsider FFx =
<:F:> . x as
Point of
(Euclid n) by EUCLID:67;
consider m being
Real such that A8:
m > 0
and A9:
OpenHypercube (
FFx,
m)
c= YY
by A7, Lm2;
defpred S1[
Nat,
object ]
means ex
h being
Function of
T,
R^1 st
(
h = F . $1 & $2
= h " ].((FFx . $1) - m),((FFx . $1) + m).[ );
A10:
for
k being
Nat st
k in Seg n holds
ex
x being
object st
S1[
k,
x]
proof
let k be
Nat;
( k in Seg n implies ex x being object st S1[k,x] )
assume A11:
k in Seg n
;
ex x being object st S1[k,x]
F . k in rng F
by A5, A11, FUNCT_1:def 3;
then consider h being
Function such that A12:
F . k = h
and A13:
dom h = the
carrier of
T
and A14:
rng h c= the
carrier of
R^1
by FUNCT_2:def 2;
reconsider h =
h as
Function of
T,
R^1 by A13, A14, FUNCT_2:2;
take
h " ].((FFx . k) - m),((FFx . k) + m).[
;
S1[k,h " ].((FFx . k) - m),((FFx . k) + m).[]
thus
S1[
k,
h " ].((FFx . k) - m),((FFx . k) + m).[]
by A12;
verum
end; consider p being
FinSequence such that A15:
(
dom p = Seg n & ( for
k being
Nat st
k in Seg n holds
S1[
k,
p . k] ) )
from FINSEQ_1:sch 1(A10);
A16:
for
Y being
set st
Y in rng p holds
x in Y
proof
let Y be
set ;
( Y in rng p implies x in Y )
assume
Y in rng p
;
x in Y
then consider k being
object such that A17:
k in dom p
and A18:
p . k = Y
by FUNCT_1:def 3;
reconsider k =
k as
Nat by A17;
consider h being
Function of
T,
R^1 such that A19:
h = F . k
and A20:
p . k = h " ].((FFx . k) - m),((FFx . k) + m).[
by A17, A15;
A21:
dom h = the
carrier of
T
by FUNCT_2:def 1;
A22:
FFx . k > (FFx . k) - m
by A8, XREAL_1:44;
(FFx . k) + m > FFx . k
by A8, XREAL_1:39;
then A23:
FFx . k in ].((FFx . k) - m),((FFx . k) + m).[
by A22, XXREAL_1:4;
h . x = FFx . k
by A19, Th20;
hence
x in Y
by A21, A6, A23, A20, A18, FUNCT_1:def 7;
verum
end;
rng p c= bool the
carrier of
T
then reconsider R =
rng p as
finite Subset-Family of
T ;
take M =
meet R;
( M is open & M c= <:F:> " Y & x in M )now for A being Subset of T st A in R holds
A is open let A be
Subset of
T;
( A in R implies A is open )A26:
[#] R^1 = REAL
by TOPMETR:17;
assume
A in R
;
A is open then consider k being
object such that A27:
k in dom p
and A28:
p . k = A
by FUNCT_1:def 3;
reconsider k =
k as
Nat by A27;
consider h being
Function of
T,
R^1 such that A29:
h = F . k
and A30:
p . k = h " ].((FFx . k) - m),((FFx . k) + m).[
by A27, A15;
reconsider P =
].((FFx . k) - m),((FFx . k) + m).[ as
Subset of
R^1 by TOPMETR:17;
A31:
P is
open
by JORDAN6:35;
h is
continuous
by A1, A5, A27, A29, A15;
hence
A is
open
by A31, A26, TOPS_2:43, A28, A30;
verum end; hence
M is
open
by TOPS_2:def 1, TOPS_2:20;
( M c= <:F:> " Y & x in M )thus
M c= <:F:> " Y
x in Mproof
let q be
object ;
TARSKI:def 3 ( not q in M or q in <:F:> " Y )
set I =
Intervals (
FFx,
m);
A32:
dom (Intervals (FFx,m)) = dom FFx
by EUCLID_9:def 3;
assume A33:
q in M
;
q in <:F:> " Y
then reconsider q =
q as
Point of
T ;
<:F:> . q in rng <:F:>
by A4, A33, FUNCT_1:def 3;
then reconsider FFq =
<:F:> . q as
Point of
(TOP-REAL n) ;
len FFx = n
by CARD_1:def 7;
then A34:
dom FFx = Seg n
by FINSEQ_1:def 3;
A35:
for
y being
object st
y in dom (Intervals (FFx,m)) holds
FFq . y in (Intervals (FFx,m)) . y
proof
let y be
object ;
( y in dom (Intervals (FFx,m)) implies FFq . y in (Intervals (FFx,m)) . y )
assume A36:
y in dom (Intervals (FFx,m))
;
FFq . y in (Intervals (FFx,m)) . y
then reconsider i =
y as
Nat ;
consider h being
Function of
T,
R^1 such that A37:
h = F . i
and A38:
p . i = h " ].((FFx . i) - m),((FFx . i) + m).[
by A36, A15, A34, A32;
A39:
h . q = FFq . i
by A37, Th20;
p . i in rng p
by A36, A34, A32, A15, FUNCT_1:def 3;
then
meet (rng p) c= p . i
by SETFAM_1:3;
then
h . q in ].((FFx . i) - m),((FFx . i) + m).[
by A38, A33, FUNCT_1:def 7;
hence
FFq . y in (Intervals (FFx,m)) . y
by A39, A32, A36, EUCLID_9:def 3;
verum
end;
len FFq = n
by CARD_1:def 7;
then
dom FFq = Seg n
by FINSEQ_1:def 3;
then
FFq in product (Intervals (FFx,m))
by A35, CARD_3:def 5, A32, A34;
then
FFq in OpenHypercube (
FFx,
m)
by EUCLID_9:def 4;
hence
q in <:F:> " Y
by A9, A4, A33, FUNCT_1:def 7;
verum
end;
rng p <> {}
by A15, RELAT_1:42;
hence
x in M
by A16, SETFAM_1:def 1;
verum
end;
thus
( ex
Q being
Subset of
T st
(
Q is
open &
Q c= <:F:> " Y &
x in Q ) implies
x in <:F:> " Y )
;
verum
end;
hence
<:F:> " Y is
open
by TOPS_1:25;
verum
end;
[#] (TOP-REAL n) <> {}
;
hence
<:F:> is continuous
by A2, TOPS_2:43; verum