let K0, B0 be Subset of (TOP-REAL 2); :: thesis: for f being Function of ((TOP-REAL 2) | K0),((TOP-REAL 2) | B0)
for f1, f2 being Function of ((TOP-REAL 2) | K0),R^1 st f1 is continuous & f2 is continuous & K0 <> {} & B0 <> {} & ( for x, y, r, s being real number st |[x,y]| in K0 & r = f1 . |[x,y]| & s = f2 . |[x,y]| holds
f . |[x,y]| = |[r,s]| ) holds
f is continuous
let f be Function of ((TOP-REAL 2) | K0),((TOP-REAL 2) | B0); :: thesis: for f1, f2 being Function of ((TOP-REAL 2) | K0),R^1 st f1 is continuous & f2 is continuous & K0 <> {} & B0 <> {} & ( for x, y, r, s being real number st |[x,y]| in K0 & r = f1 . |[x,y]| & s = f2 . |[x,y]| holds
f . |[x,y]| = |[r,s]| ) holds
f is continuous
let f1, f2 be Function of ((TOP-REAL 2) | K0),R^1 ; :: thesis: ( f1 is continuous & f2 is continuous & K0 <> {} & B0 <> {} & ( for x, y, r, s being real number st |[x,y]| in K0 & r = f1 . |[x,y]| & s = f2 . |[x,y]| holds
f . |[x,y]| = |[r,s]| ) implies f is continuous )
assume A1:
( f1 is continuous & f2 is continuous & K0 <> {} & B0 <> {} & ( for x, y, r, s being real number st |[x,y]| in K0 & r = f1 . |[x,y]| & s = f2 . |[x,y]| holds
f . |[x,y]| = |[r,s]| ) )
; :: thesis: f is continuous
then reconsider K1 = K0 as non empty Subset of (TOP-REAL 2) ;
reconsider B1 = B0 as non empty Subset of (TOP-REAL 2) by A1;
reconsider X = (TOP-REAL 2) | K1, Y = (TOP-REAL 2) | B1 as non empty TopSpace ;
reconsider f0 = f as Function of X,Y ;
for r being Point of X
for V being Subset of Y st f0 . r in V & V is open holds
ex W being Subset of X st
( r in W & W is open & f0 .: W c= V )
proof
let r be
Point of
X;
:: thesis: for V being Subset of Y st f0 . r in V & V is open holds
ex W being Subset of X st
( r in W & W is open & f0 .: W c= V )let V be
Subset of
Y;
:: thesis: ( f0 . r in V & V is open implies ex W being Subset of X st
( r in W & W is open & f0 .: W c= V ) )
assume A2:
(
f0 . r in V &
V is
open )
;
:: thesis: ex W being Subset of X st
( r in W & W is open & f0 .: W c= V )
then consider V2 being
Subset of
(TOP-REAL 2) such that A3:
(
V2 is
open &
V = V2 /\ ([#] Y) )
by TOPS_2:32;
A4:
V2 /\ ([#] Y) c= V2
by XBOOLE_1:17;
then
f0 . r in V2
by A2, A3;
then reconsider p =
f0 . r as
Point of
(TOP-REAL 2) ;
consider r2 being
real number such that A5:
(
r2 > 0 &
{ q where q is Point of (TOP-REAL 2) : ( (p `1 ) - r2 < q `1 & q `1 < (p `1 ) + r2 & (p `2 ) - r2 < q `2 & q `2 < (p `2 ) + r2 ) } c= V2 )
by A2, A3, A4, Th21;
A6:
r in the
carrier of
X
;
then A7:
r in dom f1
by FUNCT_2:def 1;
A8:
r in dom f2
by A6, FUNCT_2:def 1;
A9:
f1 . r in rng f1
by A7, FUNCT_1:12;
f2 . r in rng f2
by A8, FUNCT_1:12;
then reconsider r3 =
f1 . r,
r4 =
f2 . r as
Real by A9, TOPMETR:24;
A10: the
carrier of
X =
[#] X
.=
K0
by PRE_TOPC:def 10
;
then
r in K0
;
then reconsider pr =
r as
Point of
(TOP-REAL 2) ;
A11:
r = |[(pr `1 ),(pr `2 )]|
by EUCLID:57;
then A12:
f0 . |[(pr `1 ),(pr `2 )]| = |[r3,r4]|
by A1, A10;
p `1 < (p `1 ) + r2
by A5, XREAL_1:31;
then
(
(p `1 ) - r2 < p `1 &
p `1 < (p `1 ) + r2 )
by XREAL_1:21;
then A13:
p `1 in ].((p `1 ) - r2),((p `1 ) + r2).[
by XXREAL_1:4;
then A14:
f1 . r in ].((p `1 ) - r2),((p `1 ) + r2).[
by A11, A12, EUCLID:56;
p `2 < (p `2 ) + r2
by A5, XREAL_1:31;
then
(
(p `2 ) - r2 < p `2 &
p `2 < (p `2 ) + r2 )
by XREAL_1:21;
then A15:
p `2 in ].((p `2 ) - r2),((p `2 ) + r2).[
by XXREAL_1:4;
reconsider G1 =
].((p `1 ) - r2),((p `1 ) + r2).[,
G2 =
].((p `2 ) - r2),((p `2 ) + r2).[ as
Subset of
R^1 by TOPMETR:24;
A16:
(
G1 is
open &
G2 is
open )
by JORDAN6:46;
A17:
(
f1 . r in G1 &
f2 . r in G2 )
by A11, A12, A13, A15, EUCLID:56;
consider W1 being
Subset of
X such that A18:
(
r in W1 &
W1 is
open &
f1 .: W1 c= G1 )
by A1, A14, A16, Th20;
consider W2 being
Subset of
X such that A19:
(
r in W2 &
W2 is
open &
f2 .: W2 c= G2 )
by A1, A16, A17, Th20;
reconsider W5 =
W1 /\ W2 as
Subset of
X ;
A20:
r in W5
by A18, A19, XBOOLE_0:def 4;
f1 .: W5 c= f1 .: W1
by RELAT_1:156, XBOOLE_1:17;
then A21:
f1 .: W5 c= G1
by A18, XBOOLE_1:1;
f2 .: W5 c= f2 .: W2
by RELAT_1:156, XBOOLE_1:17;
then A22:
f2 .: W5 c= G2
by A19, XBOOLE_1:1;
f0 .: W5 c= V
proof
let v be
set ;
:: according to TARSKI:def 3 :: thesis: ( not v in f0 .: W5 or v in V )
assume A23:
v in f0 .: W5
;
:: thesis: v in V
then reconsider q2 =
v as
Point of
Y ;
consider k being
set such that A24:
(
k in dom f0 &
k in W5 &
q2 = f0 . k )
by A23, FUNCT_1:def 12;
A25:
q2 in [#] Y
;
the
carrier of
X =
[#] X
.=
K0
by PRE_TOPC:def 10
;
then
k in K0
by A24;
then reconsider r8 =
k as
Point of
(TOP-REAL 2) ;
A26:
dom f0 =
the
carrier of
((TOP-REAL 2) | K1)
by FUNCT_2:def 1
.=
[#] ((TOP-REAL 2) | K1)
.=
K0
by PRE_TOPC:def 10
;
A27:
k = |[(r8 `1 ),(r8 `2 )]|
by EUCLID:57;
A28:
|[(r8 `1 ),(r8 `2 )]| in K0
by A24, A26, EUCLID:57;
A29:
dom f1 =
the
carrier of
((TOP-REAL 2) | K0)
by FUNCT_2:def 1
.=
[#] ((TOP-REAL 2) | K0)
.=
K0
by PRE_TOPC:def 10
;
A30:
dom f2 =
the
carrier of
((TOP-REAL 2) | K0)
by FUNCT_2:def 1
.=
[#] ((TOP-REAL 2) | K0)
.=
K0
by PRE_TOPC:def 10
;
A31:
f1 . |[(r8 `1 ),(r8 `2 )]| in rng f1
by A28, A29, FUNCT_1:def 5;
f2 . |[(r8 `1 ),(r8 `2 )]| in rng f2
by A28, A30, FUNCT_1:def 5;
then reconsider r7 =
f1 . |[(r8 `1 ),(r8 `2 )]|,
s7 =
f2 . |[(r8 `1 ),(r8 `2 )]| as
Real by A31, TOPMETR:24;
A32:
v = |[r7,s7]|
by A1, A24, A26, A27;
A33:
|[r7,s7]| `1 = r7
by EUCLID:56;
A34:
|[r7,s7]| `2 = s7
by EUCLID:56;
A35:
|[(r8 `1 ),(r8 `2 )]| in W5
by A24, EUCLID:57;
then A36:
f1 . |[(r8 `1 ),(r8 `2 )]| in f1 .: W5
by A28, A29, FUNCT_1:def 12;
f2 . |[(r8 `1 ),(r8 `2 )]| in f2 .: W5
by A28, A30, A35, FUNCT_1:def 12;
then
(
(p `1 ) - r2 < r7 &
r7 < (p `1 ) + r2 &
(p `2 ) - r2 < s7 &
s7 < (p `2 ) + r2 )
by A21, A22, A36, XXREAL_1:4;
then
v in { q3 where q3 is Point of (TOP-REAL 2) : ( (p `1 ) - r2 < q3 `1 & q3 `1 < (p `1 ) + r2 & (p `2 ) - r2 < q3 `2 & q3 `2 < (p `2 ) + r2 ) }
by A32, A33, A34;
hence
v in V
by A3, A5, A25, XBOOLE_0:def 4;
:: thesis: verum
end;
hence
ex
W being
Subset of
X st
(
r in W &
W is
open &
f0 .: W c= V )
by A18, A19, A20, TOPS_1:38;
:: thesis: verum
end;
hence
f is continuous
by Th20; :: thesis: verum