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