let a, b, c, d, x1 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 st a < b & c < d & f is_continuous_at x & f . a = c & f . b = d & f is one-to-one & f = g & x = x1 holds
g | [.a,b.] 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 st a < b & c < d & f is_continuous_at x & f . a = c & f . b = d & f is one-to-one & f = g & x = x1 holds
g | [.a,b.] is_continuous_in x1
let x be Point of (Closed-Interval-TSpace (a,b)); for g being PartFunc of REAL,REAL st a < b & c < d & f is_continuous_at x & f . a = c & f . b = d & f is one-to-one & f = g & x = x1 holds
g | [.a,b.] is_continuous_in x1
let g be PartFunc of REAL,REAL; ( a < b & c < d & f is_continuous_at x & f . a = c & f . b = d & f is one-to-one & f = g & x = x1 implies g | [.a,b.] is_continuous_in x1 )
assume that
A1:
a < b
and
A2:
c < d
and
A3:
f is_continuous_at x
and
A4:
f . a = c
and
A5:
f . b = d
and
A6:
f is one-to-one
and
A7:
f = g
and
A8:
x = x1
; g | [.a,b.] is_continuous_in x1
A9:
for c being Element of REAL st c in dom g holds
g /. c = g /. c
;
dom g = the carrier of (Closed-Interval-TSpace (a,b))
by A7, FUNCT_2:def 1;
then
dom g = [.a,b.]
by A1, TOPMETR:18;
then
dom g = (dom g) /\ [.a,b.]
;
then A10:
g = g | [.a,b.]
by A9, PARTFUN2:15;
per cases
( x1 = a or x1 = b or ( x1 <> a & x1 <> b ) )
;
suppose A11:
x1 = a
;
g | [.a,b.] is_continuous_in x1
for
N1 being
Neighbourhood of
g . x1 ex
N being
Neighbourhood of
x1 st
g .: N c= N1
proof
reconsider f0 =
f . a as
Point of
(Closed-Interval-TSpace (c,d)) by A2, A4, Lm6;
let N1 be
Neighbourhood of
g . x1;
ex N being Neighbourhood of x1 st g .: N c= N1
reconsider N2 =
N1 as
Subset of
RealSpace by METRIC_1:def 13;
set NN1 =
N1 /\ [.c,d.];
N2 in Family_open_set RealSpace
by Lm3;
then A12:
N2 in the
topology of
(TopSpaceMetr RealSpace)
by TOPMETR:12;
N1 /\ [.c,d.] = N1 /\ the
carrier of
(Closed-Interval-TSpace (c,d))
by A2, TOPMETR:18;
then reconsider NN =
N1 /\ [.c,d.] as
Subset of
(Closed-Interval-TSpace (c,d)) by XBOOLE_1:17;
N1 /\ [.c,d.] = N1 /\ ([#] (Closed-Interval-TSpace (c,d)))
by A2, TOPMETR:18;
then
NN in the
topology of
(Closed-Interval-TSpace (c,d))
by A12, PRE_TOPC:def 4, TOPMETR:def 6;
then A13:
NN is
open
;
f . a in the
carrier of
(Closed-Interval-TSpace (c,d))
by A2, A4, Lm6;
then
(
g . x1 in N1 &
g . x1 in [.c,d.] )
by A2, A7, A11, RCOMP_1:16, TOPMETR:18;
then
g . x1 in N1 /\ [.c,d.]
by XBOOLE_0:def 4;
then reconsider N19 =
NN as
a_neighborhood of
f0 by A7, A11, A13, CONNSP_2:3;
consider H being
a_neighborhood of
x such that A14:
f .: H c= N19
by A3, A8, A11, TMAP_1:def 2;
consider H1 being
Subset of
(Closed-Interval-TSpace (a,b)) such that A15:
H1 is
open
and A16:
H1 c= H
and A17:
x in H1
by CONNSP_2:6;
H1 in the
topology of
(Closed-Interval-TSpace (a,b))
by A15;
then consider Q being
Subset of
R^1 such that A18:
Q in the
topology of
R^1
and A19:
H1 = Q /\ ([#] (Closed-Interval-TSpace (a,b)))
by PRE_TOPC:def 4;
reconsider Q9 =
Q as
Subset of
RealSpace by TOPMETR:12, TOPMETR:def 6;
reconsider Q1 =
Q9 as
Subset of
REAL by METRIC_1:def 13;
Q9 in Family_open_set RealSpace
by A18, TOPMETR:12, TOPMETR:def 6;
then A20:
Q1 is
open
by Lm4;
x1 in Q1
by A8, A17, A19, XBOOLE_0:def 4;
then consider N being
Neighbourhood of
x1 such that A21:
N c= Q1
by A20, RCOMP_1:18;
take
N
;
g .: N c= N1
g .: N c= N1
proof
let aa be
object ;
TARSKI:def 3 ( not aa in g .: N or aa in N1 )
assume A22:
aa in g .: N
;
aa in N1
then reconsider a9 =
aa as
Element of
REAL ;
consider cc being
Element of
REAL such that A23:
cc in dom g
and A24:
cc in N
and A25:
a9 = g . cc
by A22, PARTFUN2:59;
cc in the
carrier of
(Closed-Interval-TSpace (a,b))
by A7, A23, FUNCT_2:def 1;
then
cc in H1
by A19, A21, A24, XBOOLE_0:def 4;
then
g . cc in f .: H
by A7, A16, FUNCT_2:35;
hence
aa in N1
by A14, A25, XBOOLE_0:def 4;
verum
end;
hence
g .: N c= N1
;
verum
end; hence
g | [.a,b.] is_continuous_in x1
by A10, FCONT_1:5;
verum suppose A26:
x1 = b
;
g | [.a,b.] is_continuous_in x1
for
N1 being
Neighbourhood of
g . x1 ex
N being
Neighbourhood of
x1 st
g .: N c= N1
proof
reconsider f0 =
f . b as
Point of
(Closed-Interval-TSpace (c,d)) by A2, A5, Lm6;
let N1 be
Neighbourhood of
g . x1;
ex N being Neighbourhood of x1 st g .: N c= N1
reconsider N2 =
N1 as
Subset of
RealSpace by METRIC_1:def 13;
set NN1 =
N1 /\ ([#] (Closed-Interval-TSpace (c,d)));
reconsider NN =
N1 /\ ([#] (Closed-Interval-TSpace (c,d))) as
Subset of
(Closed-Interval-TSpace (c,d)) ;
N2 in Family_open_set RealSpace
by Lm3;
then
N2 in the
topology of
(TopSpaceMetr RealSpace)
by TOPMETR:12;
then
NN in the
topology of
(Closed-Interval-TSpace (c,d))
by PRE_TOPC:def 4, TOPMETR:def 6;
then A27:
NN is
open
;
(
g . x1 in N1 &
g . x1 in [#] (Closed-Interval-TSpace (c,d)) )
by A2, A5, A7, A26, Lm6, RCOMP_1:16;
then
g . x1 in N1 /\ ([#] (Closed-Interval-TSpace (c,d)))
by XBOOLE_0:def 4;
then reconsider N19 =
NN as
a_neighborhood of
f0 by A7, A26, A27, CONNSP_2:3;
consider H being
a_neighborhood of
x such that A28:
f .: H c= N19
by A3, A8, A26, TMAP_1:def 2;
consider H1 being
Subset of
(Closed-Interval-TSpace (a,b)) such that A29:
H1 is
open
and A30:
H1 c= H
and A31:
x in H1
by CONNSP_2:6;
H1 in the
topology of
(Closed-Interval-TSpace (a,b))
by A29;
then consider Q being
Subset of
R^1 such that A32:
Q in the
topology of
R^1
and A33:
H1 = Q /\ ([#] (Closed-Interval-TSpace (a,b)))
by PRE_TOPC:def 4;
reconsider Q9 =
Q as
Subset of
RealSpace by TOPMETR:12, TOPMETR:def 6;
reconsider Q1 =
Q9 as
Subset of
REAL by METRIC_1:def 13;
Q9 in Family_open_set RealSpace
by A32, TOPMETR:12, TOPMETR:def 6;
then A34:
Q1 is
open
by Lm4;
x1 in Q1
by A8, A31, A33, XBOOLE_0:def 4;
then consider N being
Neighbourhood of
x1 such that A35:
N c= Q1
by A34, RCOMP_1:18;
take
N
;
g .: N c= N1
g .: N c= N1
proof
let aa be
object ;
TARSKI:def 3 ( not aa in g .: N or aa in N1 )
assume A36:
aa in g .: N
;
aa in N1
then reconsider a9 =
aa as
Element of
REAL ;
consider cc being
Element of
REAL such that A37:
cc in dom g
and A38:
cc in N
and A39:
a9 = g . cc
by A36, PARTFUN2:59;
cc in the
carrier of
(Closed-Interval-TSpace (a,b))
by A7, A37, FUNCT_2:def 1;
then
cc in H1
by A33, A35, A38, XBOOLE_0:def 4;
then
g . cc in f .: H
by A7, A30, FUNCT_2:35;
hence
aa in N1
by A28, A39, XBOOLE_0:def 4;
verum
end;
hence
g .: N c= N1
;
verum
end; hence
g | [.a,b.] is_continuous_in x1
by A10, FCONT_1:5;
verum suppose
(
x1 <> a &
x1 <> b )
;
g | [.a,b.] is_continuous_in x1hence
g | [.a,b.] is_continuous_in x1
by A1, A2, A3, A4, A5, A6, A7, A8, A10, Lm7;
verum end;