let X be non empty strict SubSpace of R^1 ; for f being RealMap of X
for g being PartFunc of REAL,REAL
for x being Point of X
for x0 being Real st g = f & x = x0 holds
( ( for V being Subset of REAL st f . x in V & V is open holds
ex W being Subset of X st
( x in W & W is open & f .: W c= V ) ) iff g is_continuous_in x0 )
let f be RealMap of X; for g being PartFunc of REAL,REAL
for x being Point of X
for x0 being Real st g = f & x = x0 holds
( ( for V being Subset of REAL st f . x in V & V is open holds
ex W being Subset of X st
( x in W & W is open & f .: W c= V ) ) iff g is_continuous_in x0 )
let g be PartFunc of REAL,REAL; for x being Point of X
for x0 being Real st g = f & x = x0 holds
( ( for V being Subset of REAL st f . x in V & V is open holds
ex W being Subset of X st
( x in W & W is open & f .: W c= V ) ) iff g is_continuous_in x0 )
let x be Point of X; for x0 being Real st g = f & x = x0 holds
( ( for V being Subset of REAL st f . x in V & V is open holds
ex W being Subset of X st
( x in W & W is open & f .: W c= V ) ) iff g is_continuous_in x0 )
let x0 be Real; ( g = f & x = x0 implies ( ( for V being Subset of REAL st f . x in V & V is open holds
ex W being Subset of X st
( x in W & W is open & f .: W c= V ) ) iff g is_continuous_in x0 ) )
assume AS:
( g = f & x = x0 )
; ( ( for V being Subset of REAL st f . x in V & V is open holds
ex W being Subset of X st
( x in W & W is open & f .: W c= V ) ) iff g is_continuous_in x0 )
A1:
dom g = the carrier of X
by FUNCT_2:def 1, AS;
hereby ( g is_continuous_in x0 implies for V being Subset of REAL st f . x in V & V is open holds
ex W being Subset of X st
( x in W & W is open & f .: W c= V ) )
assume A2:
for
V being
Subset of
REAL st
f . x in V &
V is
open holds
ex
W being
Subset of
X st
(
x in W &
W is
open &
f .: W c= V )
;
g is_continuous_in x0
for
N1 being
Neighbourhood of
g . x0 ex
N being
Neighbourhood of
x0 st
g .: N c= N1
proof
let N1 be
Neighbourhood of
g . x0;
ex N being Neighbourhood of x0 st g .: N c= N1
consider s being
Real such that A3:
(
0 < s &
N1 = ].((g . x0) - s),((g . x0) + s).[ )
by RCOMP_1:def 6;
A4:
].((g . x0) - s),((g . x0) + s).[ is
open
by RCOMP_1:7;
B5:
|.((g . x0) - (g . x0)).| = 0
;
consider W being
Subset of
X such that A6:
(
x in W &
W is
open &
f .: W c= ].((g . x0) - s),((g . x0) + s).[ )
by A2, A4, B5, A3, RCOMP_1:1, AS;
W in the
topology of
X
by A6, PRE_TOPC:def 2;
then consider W0 being
Subset of
R^1 such that A7:
(
W0 in the
topology of
R^1 &
W = W0 /\ ([#] X) )
by PRE_TOPC:def 4;
reconsider W1 =
W0 as
Subset of
REAL ;
W0 is
open
by A7, PRE_TOPC:def 2;
then A8:
W1 is
open
by BORSUK_5:39;
x0 in W1
by A6, A7, AS, XBOOLE_0:def 4;
then consider N being
Neighbourhood of
x0 such that A9:
N c= W1
by A8, RCOMP_1:18;
take
N
;
g .: N c= N1
A10:
g .: N c= g .: W1
by A9, RELAT_1:123;
g .: W1 = f .: W
by A1, A7, AS, RELAT_1:112;
hence
g .: N c= N1
by A3, A6, A10;
verum
end; hence
g is_continuous_in x0
by FCONT_1:5;
verum
end;
assume B11:
g is_continuous_in x0
; for V being Subset of REAL st f . x in V & V is open holds
ex W being Subset of X st
( x in W & W is open & f .: W c= V )
thus
for V being Subset of REAL st f . x in V & V is open holds
ex W being Subset of X st
( x in W & W is open & f .: W c= V )
verumproof
let V be
Subset of
REAL;
( f . x in V & V is open implies ex W being Subset of X st
( x in W & W is open & f .: W c= V ) )
assume
(
f . x in V &
V is
open )
;
ex W being Subset of X st
( x in W & W is open & f .: W c= V )
then consider N1 being
Neighbourhood of
f . x such that A13:
N1 c= V
by RCOMP_1:18;
consider N being
Neighbourhood of
x0 such that A14:
g .: N c= N1
by B11, FCONT_1:5, AS;
consider s being
Real such that A15:
(
0 < s &
N = ].(x0 - s),(x0 + s).[ )
by RCOMP_1:def 6;
A16:
].(x0 - s),(x0 + s).[ is
open
by RCOMP_1:7;
B17:
|.(x0 - x0).| = 0
;
reconsider W0 =
].(x0 - s),(x0 + s).[ as
Subset of
R^1 ;
W0 is
open
by A16, BORSUK_5:39;
then
W0 in the
topology of
R^1
by PRE_TOPC:def 2;
then
W0 /\ ([#] X) in the
topology of
X
by PRE_TOPC:def 4;
then reconsider W =
W0 /\ ([#] X) as
open Subset of
X by PRE_TOPC:def 2;
take
W
;
( x in W & W is open & f .: W c= V )
(
x in W0 &
x in [#] X )
by B17, A15, RCOMP_1:1, AS;
hence
x in W
by XBOOLE_0:def 4;
( W is open & f .: W c= V )
thus
W is
open
;
f .: W c= V
f .: W = g .: W0
by RELAT_1:112, A1, AS;
hence
f .: W c= V
by A13, A14, A15;
verum
end;