let f be Function of R^1 ,R^1 ; :: thesis: for x being Point of R^1
for g being PartFunc of REAL ,REAL
for x1 being Real st f is_continuous_at x & f = g & x = x1 holds
g is_continuous_in x1
let x be Point of R^1 ; :: thesis: for g being PartFunc of REAL ,REAL
for x1 being Real st f is_continuous_at x & f = g & x = x1 holds
g is_continuous_in x1
let g be PartFunc of REAL ,REAL ; :: thesis: for x1 being Real st f is_continuous_at x & f = g & x = x1 holds
g is_continuous_in x1
let x1 be Real; :: thesis: ( f is_continuous_at x & f = g & x = x1 implies g is_continuous_in x1 )
assume A1:
( f is_continuous_at x & f = g & x = x1 )
; :: thesis: g is_continuous_in x1
for N1 being Neighbourhood of g . x1 ex N being Neighbourhood of x1 st g .: N c= N1
proof
let N1 be
Neighbourhood of
g . x1;
:: thesis: ex N being Neighbourhood of x1 st g .: N c= N1
reconsider fx =
f . x as
Point of
R^1 ;
reconsider N1' =
N1 as
Subset of
R^1 by TOPMETR:24;
reconsider N2 =
N1 as
Subset of
RealSpace by TOPMETR:16, TOPMETR:24, TOPMETR:def 7;
N2 in Family_open_set RealSpace
by Lm3;
then
N2 in the
topology of
(TopSpaceMetr RealSpace )
by TOPMETR:16;
then
(
fx in N1' &
N1' is
open )
by A1, PRE_TOPC:def 5, RCOMP_1:37, TOPMETR:def 7;
then reconsider G =
N1' as
a_neighborhood of
fx by CONNSP_2:5;
consider H being
a_neighborhood of
x such that A3:
f .: H c= G
by A1, TMAP_1:def 2;
consider V being
Subset of
R^1 such that A4:
(
V is
open &
V c= H &
x in V )
by CONNSP_2:8;
V in the
topology of
R^1
by A4, PRE_TOPC:def 5;
then A5:
V in Family_open_set RealSpace
by TOPMETR:16, TOPMETR:def 7;
reconsider V1 =
V as
Subset of
REAL by TOPMETR:24;
V1 is
open
by A5, Lm4;
then consider N being
Neighbourhood of
x1 such that A6:
N c= V1
by A1, A4, RCOMP_1:39;
N c= H
by A4, A6, XBOOLE_1:1;
then
g .: N c= g .: H
by RELAT_1:156;
hence
ex
N being
Neighbourhood of
x1 st
g .: N c= N1
by A1, A3, XBOOLE_1:1;
:: thesis: verum
end;
hence
g is_continuous_in x1
by FCONT_1:5; :: thesis: verum