let a, b, c, d be Real; 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)); 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)); 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; 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; ( 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 that
A1:
a < b
and
A2:
c < d
and
A3:
f is_continuous_at x
and
A4:
x <> a
and
A5:
x <> b
and
A6:
f . a = c
and
A7:
f . b = d
and
A8:
f is one-to-one
and
A9:
f = g
and
A10:
x = x1
; g is_continuous_in x1
A11:
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
reconsider fx =
f . x as
Point of
(Closed-Interval-TSpace (c,d)) ;
set Rm =
min (
((g . x1) - c),
(d - (g . x1)));
let N1 be
Neighbourhood of
g . x1;
ex N being Neighbourhood of x1 st g .: N c= N1
Closed-Interval-TSpace (
c,
d)
= TopSpaceMetr (Closed-Interval-MSpace (c,d))
by TOPMETR:def 7;
then A12:
the
topology of
(Closed-Interval-TSpace (c,d)) = Family_open_set (Closed-Interval-MSpace (c,d))
by TOPMETR:12;
min (
((g . x1) - c),
(d - (g . x1)))
> 0
proof
A13:
b in dom f
by A1, A11, Lm6;
A14:
a in dom f
by A1, A11, 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 A15:
min (
((g . x1) - c),
(d - (g . x1)))
= (g . x1) - c
;
min (((g . x1) - c),(d - (g . x1))) > 0
g . x1 in the
carrier of
(Closed-Interval-TSpace (c,d))
by A9, A10, FUNCT_2:5;
then A16:
g . x1 >= c
by A2, Lm6;
min (
((g . x1) - c),
(d - (g . x1)))
<> 0
by A4, A6, A8, A9, A10, A11, A14, A15, FUNCT_1:def 4;
hence
min (
((g . x1) - c),
(d - (g . x1)))
> 0
by A15, A16, XREAL_1:48;
verum end; suppose A17:
min (
((g . x1) - c),
(d - (g . x1)))
= d - (g . x1)
;
min (((g . x1) - c),(d - (g . x1))) > 0
g . x1 in the
carrier of
(Closed-Interval-TSpace (c,d))
by A9, A10, FUNCT_2:5;
then A18:
g . x1 <= d
by A2, Lm6;
d - (g . x1) <> d - d
by A5, A7, A8, A9, A10, A11, A13, FUNCT_1:def 4;
hence
min (
((g . x1) - c),
(d - (g . x1)))
> 0
by A17, A18, XREAL_1:48;
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 6;
consider Ham being
Neighbourhood of
g . x1 such that A19:
Ham c= N1
and A20:
Ham c= Wuj
by RCOMP_1:17;
A21:
Wuj c= ].c,d.[
proof
let aa be
object ;
TARSKI:def 3 ( not aa in Wuj or aa in ].c,d.[ )
assume
aa in Wuj
;
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 A22:
A = aa
and A23:
(g . x1) - (min (((g . x1) - c),(d - (g . x1)))) < A
and A24:
A < (g . x1) + (min (((g . x1) - c),(d - (g . x1))))
;
min (
((g . x1) - c),
(d - (g . x1)))
<= d - (g . x1)
by XXREAL_0:17;
then
(g . x1) + (min (((g . x1) - c),(d - (g . x1)))) <= (g . x1) + (d - (g . x1))
by XREAL_1:6;
then A25:
A < d
by A24, XXREAL_0:2;
min (
((g . x1) - c),
(d - (g . x1)))
<= (g . x1) - c
by XXREAL_0:17;
then
c + (min (((g . x1) - c),(d - (g . x1)))) <= g . x1
by XREAL_1:19;
then
c <= (g . x1) - (min (((g . x1) - c),(d - (g . x1))))
by XREAL_1:19;
then
c < A
by A23, XXREAL_0:2;
then
A in { l where l is Real : ( c < l & l < d ) }
by A25;
hence
aa in ].c,d.[
by A22, RCOMP_1:def 2;
verum
end;
].c,d.[ c= [.c,d.]
by XXREAL_1:25;
then A26:
Wuj c= [.c,d.]
by A21;
then
Wuj c= the
carrier of
(Closed-Interval-MSpace (c,d))
by A2, TOPMETR:10;
then reconsider N21 =
Ham as
Subset of
(Closed-Interval-MSpace (c,d)) by A20, XBOOLE_1:1;
the
carrier of
(Closed-Interval-MSpace (c,d)) =
the
carrier of
(TopSpaceMetr (Closed-Interval-MSpace (c,d)))
by TOPMETR:12
.=
the
carrier of
(Closed-Interval-TSpace (c,d))
by TOPMETR:def 7
;
then reconsider N19 =
N21 as
Subset of
(Closed-Interval-TSpace (c,d)) ;
N21 in Family_open_set (Closed-Interval-MSpace (c,d))
by Th12;
then
N19 is
open
by A12;
then reconsider G =
N19 as
a_neighborhood of
fx by A9, A10, CONNSP_2:3, RCOMP_1:16;
consider H being
a_neighborhood of
x such that A27:
f .: H c= G
by A3, TMAP_1:def 2;
consider V being
Subset of
(Closed-Interval-TSpace (a,b)) such that A28:
V is
open
and A29:
V c= H
and A30:
x in V
by CONNSP_2:6;
A31: the
carrier of
(Closed-Interval-MSpace (a,b)) =
the
carrier of
(TopSpaceMetr (Closed-Interval-MSpace (a,b)))
by TOPMETR:12
.=
the
carrier of
(Closed-Interval-TSpace (a,b))
by TOPMETR:def 7
;
then reconsider V2 =
V as
Subset of
(Closed-Interval-MSpace (a,b)) ;
V c= the
carrier of
(Closed-Interval-MSpace (a,b))
by A31;
then
V c= [.a,b.]
by A1, TOPMETR:10;
then reconsider V1 =
V as
Subset of
REAL by XBOOLE_1:1;
A32:
Ham c= [.c,d.]
by A20, A26;
A33:
( not
a in V1 & not
b in V1 )
proof
assume A34:
(
a in V1 or
b in V1 )
;
contradiction
end;
Closed-Interval-TSpace (
a,
b)
= TopSpaceMetr (Closed-Interval-MSpace (a,b))
by TOPMETR:def 7;
then
the
topology of
(Closed-Interval-TSpace (a,b)) = Family_open_set (Closed-Interval-MSpace (a,b))
by TOPMETR:12;
then
V2 in Family_open_set (Closed-Interval-MSpace (a,b))
by A28;
then
V1 is
open
by A1, A33, Th10;
then consider N being
Neighbourhood of
x1 such that A35:
N c= V1
by A10, A30, RCOMP_1:18;
N c= H
by A29, A35;
then A36:
g .: N c= g .: H
by RELAT_1:123;
f .: H c= N1
by A19, A27;
hence
ex
N being
Neighbourhood of
x1 st
g .: N c= N1
by A9, A36, XBOOLE_1:1;
verum
end;
hence
g is_continuous_in x1
by FCONT_1:5; verum