let a, b, c, d be Real; :: thesis: for f being Function of (Closed-Interval-TSpace a,b),(Closed-Interval-TSpace c,d)
for x being Point of (Closed-Interval-TSpace a,b)
for g being PartFunc of REAL ,REAL
for x1 being Real st a < b & c < d & f is_continuous_at x & x <> a & x <> b & f . a = c & f . b = d & f is one-to-one & f = g & x = x1 holds
g is_continuous_in x1
let f be Function of (Closed-Interval-TSpace a,b),(Closed-Interval-TSpace c,d); :: thesis: for x being Point of (Closed-Interval-TSpace a,b)
for g being PartFunc of REAL ,REAL
for x1 being Real st a < b & c < d & f is_continuous_at x & x <> a & x <> b & f . a = c & f . b = d & f is one-to-one & f = g & x = x1 holds
g is_continuous_in x1
let x be Point of (Closed-Interval-TSpace a,b); :: thesis: for g being PartFunc of REAL ,REAL
for x1 being Real st a < b & c < d & f is_continuous_at x & x <> a & x <> b & f . a = c & f . b = d & f is one-to-one & f = g & x = x1 holds
g is_continuous_in x1
let g be PartFunc of REAL ,REAL ; :: thesis: for x1 being Real st a < b & c < d & f is_continuous_at x & x <> a & x <> b & f . a = c & f . b = d & f is one-to-one & f = g & x = x1 holds
g is_continuous_in x1
let x1 be Real; :: thesis: ( a < b & c < d & f is_continuous_at x & x <> a & x <> b & f . a = c & f . b = d & f is one-to-one & f = g & x = x1 implies g is_continuous_in x1 )
assume A1:
( a < b & c < d & f is_continuous_at x & x <> a & x <> b & f . a = c & f . b = d & f is one-to-one & f = g & x = x1 )
; :: thesis: g is_continuous_in x1
A2:
dom f = the carrier of (Closed-Interval-TSpace a,b)
by FUNCT_2:def 1;
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
set Rm =
min ((g . x1) - c),
(d - (g . x1));
min ((g . x1) - c),
(d - (g . x1)) > 0
proof
A3:
(
a in dom f &
b in dom f )
by A1, A2, Lm6;
per cases
( min ((g . x1) - c),(d - (g . x1)) = (g . x1) - c or min ((g . x1) - c),(d - (g . x1)) = d - (g . x1) )
by XXREAL_0:15;
suppose A4:
min ((g . x1) - c),
(d - (g . x1)) = (g . x1) - c
;
:: thesis: min ((g . x1) - c),(d - (g . x1)) > 0 then A5:
min ((g . x1) - c),
(d - (g . x1)) <> 0
by A1, A2, A3, FUNCT_1:def 8;
g . x1 in the
carrier of
(Closed-Interval-TSpace c,d)
by A1, FUNCT_2:7;
then
g . x1 >= c
by A1, Lm6;
hence
min ((g . x1) - c),
(d - (g . x1)) > 0
by A4, A5, XREAL_1:50;
:: thesis: verum end;
end;
then reconsider Wuj =
].((g . x1) - (min ((g . x1) - c),(d - (g . x1)))),((g . x1) + (min ((g . x1) - c),(d - (g . x1)))).[ as
Neighbourhood of
g . x1 by RCOMP_1:def 7;
consider Ham being
Neighbourhood of
g . x1 such that A8:
(
Ham c= N1 &
Ham c= Wuj )
by RCOMP_1:38;
reconsider fx =
f . x as
Point of
(Closed-Interval-TSpace c,d) ;
A9:
].c,d.[ c= [.c,d.]
by XXREAL_1:25;
Wuj c= ].c,d.[
proof
A10:
(
min ((g . x1) - c),
(d - (g . x1)) <= (g . x1) - c &
min ((g . x1) - c),
(d - (g . x1)) <= d - (g . x1) )
by XXREAL_0:17;
let aa be
set ;
:: according to TARSKI:def 3 :: thesis: ( not aa in Wuj or aa in ].c,d.[ )
assume
aa in Wuj
;
:: thesis: aa in ].c,d.[
then
aa in { l where l is Real : ( (g . x1) - (min ((g . x1) - c),(d - (g . x1))) < l & l < (g . x1) + (min ((g . x1) - c),(d - (g . x1))) ) }
by RCOMP_1:def 2;
then consider A being
Real such that A11:
(
A = aa &
(g . x1) - (min ((g . x1) - c),(d - (g . x1))) < A &
A < (g . x1) + (min ((g . x1) - c),(d - (g . x1))) )
;
c + (min ((g . x1) - c),(d - (g . x1))) <= g . x1
by A10, XREAL_1:21;
then
c <= (g . x1) - (min ((g . x1) - c),(d - (g . x1)))
by XREAL_1:21;
then A12:
c < A
by A11, XXREAL_0:2;
(g . x1) + (min ((g . x1) - c),(d - (g . x1))) <= (g . x1) + (d - (g . x1))
by A10, XREAL_1:8;
then
A < d
by A11, XXREAL_0:2;
then
A in { l where l is Real : ( c < l & l < d ) }
by A12;
hence
aa in ].c,d.[
by A11, RCOMP_1:def 2;
:: thesis: verum
end;
then A13:
Wuj c= [.c,d.]
by A9, XBOOLE_1:1;
then A14:
Wuj c= the
carrier of
(Closed-Interval-MSpace c,d)
by A1, TOPMETR:14;
A15:
Ham c= [.c,d.]
by A8, A13, XBOOLE_1:1;
A16: the
carrier of
(Closed-Interval-MSpace c,d) =
the
carrier of
(TopSpaceMetr (Closed-Interval-MSpace c,d))
by TOPMETR:16
.=
the
carrier of
(Closed-Interval-TSpace c,d)
by TOPMETR:def 8
;
A17: the
carrier of
(Closed-Interval-MSpace a,b) =
the
carrier of
(TopSpaceMetr (Closed-Interval-MSpace a,b))
by TOPMETR:16
.=
the
carrier of
(Closed-Interval-TSpace a,b)
by TOPMETR:def 8
;
reconsider N21 =
Ham as
Subset of
(Closed-Interval-MSpace c,d) by A8, A14, XBOOLE_1:1;
reconsider N1' =
N21 as
Subset of
(Closed-Interval-TSpace c,d) by A16;
Closed-Interval-TSpace c,
d = TopSpaceMetr (Closed-Interval-MSpace c,d)
by TOPMETR:def 8;
then A18:
the
topology of
(Closed-Interval-TSpace c,d) = Family_open_set (Closed-Interval-MSpace c,d)
by TOPMETR:16;
Closed-Interval-TSpace a,
b = TopSpaceMetr (Closed-Interval-MSpace a,b)
by TOPMETR:def 8;
then A19:
the
topology of
(Closed-Interval-TSpace a,b) = Family_open_set (Closed-Interval-MSpace a,b)
by TOPMETR:16;
N21 in Family_open_set (Closed-Interval-MSpace c,d)
by A1, Th13;
then
(
fx in N1' &
N1' is
open )
by A1, A18, PRE_TOPC:def 5, RCOMP_1:37;
then reconsider G =
N1' as
a_neighborhood of
fx by CONNSP_2:5;
consider H being
a_neighborhood of
x such that A20:
f .: H c= G
by A1, TMAP_1:def 2;
A21:
f .: H c= N1
by A8, A20, XBOOLE_1:1;
consider V being
Subset of
(Closed-Interval-TSpace a,b) such that A22:
(
V is
open &
V c= H &
x in V )
by CONNSP_2:8;
reconsider V2 =
V as
Subset of
(Closed-Interval-MSpace a,b) by A17;
V c= the
carrier of
(Closed-Interval-MSpace a,b)
by A17;
then A23:
V c= [.a,b.]
by A1, TOPMETR:14;
A24:
V2 in Family_open_set (Closed-Interval-MSpace a,b)
by A19, A22, PRE_TOPC:def 5;
reconsider V1 =
V as
Subset of
REAL by A23, XBOOLE_1:1;
( not
a in V1 & not
b in V1 )
then
V1 is
open
by A1, A24, Th11;
then consider N being
Neighbourhood of
x1 such that A26:
N c= V1
by A1, A22, RCOMP_1:39;
N c= H
by A22, A26, 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, A21, XBOOLE_1:1;
:: thesis: verum
end;
hence
g is_continuous_in x1
by FCONT_1:5; :: thesis: verum