let a, b be real number ; ( a < b implies for t1, t2 being Point of (Closed-Interval-TSpace 0 ,1) holds P[01] a,b,t1,t2 is continuous Function of (Closed-Interval-TSpace a,b),(Closed-Interval-TSpace 0 ,1) )
assume A1:
a < b
; for t1, t2 being Point of (Closed-Interval-TSpace 0 ,1) holds P[01] a,b,t1,t2 is continuous Function of (Closed-Interval-TSpace a,b),(Closed-Interval-TSpace 0 ,1)
reconsider a = a, b = b as Real by XREAL_0:def 1;
A2:
[.a,b.] = the carrier of (Closed-Interval-TSpace a,b)
by A1, TOPMETR:25;
let t1, t2 be Point of (Closed-Interval-TSpace 0 ,1); P[01] a,b,t1,t2 is continuous Function of (Closed-Interval-TSpace a,b),(Closed-Interval-TSpace 0 ,1)
reconsider r1 = t1, r2 = t2 as Real by Lm2;
deffunc H1( Element of REAL ) -> Element of REAL = (((r2 - r1) / (b - a)) * $1) + (((b * r1) - (a * r2)) / (b - a));
consider P being Function of REAL ,REAL such that
A3:
for r being Real holds P . r = H1(r)
from FUNCT_2:sch 4();
reconsider f = P as Function of R^1 ,R^1 by TOPMETR:24;
A4:
for s being Point of (Closed-Interval-TSpace a,b)
for w being Point of R^1 st s = w holds
(P[01] a,b,t1,t2) . s = f . w
proof
let s be
Point of
(Closed-Interval-TSpace a,b);
for w being Point of R^1 st s = w holds
(P[01] a,b,t1,t2) . s = f . wlet w be
Point of
R^1 ;
( s = w implies (P[01] a,b,t1,t2) . s = f . w )
reconsider r =
s as
Real by A1, Lm2;
assume A5:
s = w
;
(P[01] a,b,t1,t2) . s = f . w
thus (P[01] a,b,t1,t2) . s =
(((r2 - r1) / (b - a)) * r) + (((b * r1) - (a * r2)) / (b - a))
by A1, Th14
.=
f . w
by A3, A5
;
verum
end;
A6:
f is continuous
by A3, TOPMETR:28;
for s being Point of (Closed-Interval-TSpace a,b) holds P[01] a,b,t1,t2 is_continuous_at s
proof
let s be
Point of
(Closed-Interval-TSpace a,b);
P[01] a,b,t1,t2 is_continuous_at s
reconsider w =
s as
Point of
R^1 by A2, TARSKI:def 3, TOPMETR:24;
for
G being
Subset of
(Closed-Interval-TSpace 0 ,1) st
G is
open &
(P[01] a,b,t1,t2) . s in G holds
ex
H being
Subset of
(Closed-Interval-TSpace a,b) st
(
H is
open &
s in H &
(P[01] a,b,t1,t2) .: H c= G )
proof
let G be
Subset of
(Closed-Interval-TSpace 0 ,1);
( G is open & (P[01] a,b,t1,t2) . s in G implies ex H being Subset of (Closed-Interval-TSpace a,b) st
( H is open & s in H & (P[01] a,b,t1,t2) .: H c= G ) )
assume
G is
open
;
( not (P[01] a,b,t1,t2) . s in G or ex H being Subset of (Closed-Interval-TSpace a,b) st
( H is open & s in H & (P[01] a,b,t1,t2) .: H c= G ) )
then consider G0 being
Subset of
R^1 such that A7:
G0 is
open
and A8:
G0 /\ ([#] (Closed-Interval-TSpace 0 ,1)) = G
by TOPS_2:32;
A9:
f is_continuous_at w
by A6, TMAP_1:49;
assume
(P[01] a,b,t1,t2) . s in G
;
ex H being Subset of (Closed-Interval-TSpace a,b) st
( H is open & s in H & (P[01] a,b,t1,t2) .: H c= G )
then
f . w in G
by A4;
then
f . w in G0
by A8, XBOOLE_0:def 4;
then consider H0 being
Subset of
R^1 such that A10:
H0 is
open
and A11:
w in H0
and A12:
f .: H0 c= G0
by A7, A9, TMAP_1:48;
now reconsider H =
H0 /\ ([#] (Closed-Interval-TSpace a,b)) as
Subset of
(Closed-Interval-TSpace a,b) ;
take H =
H;
( H is open & s in H & (P[01] a,b,t1,t2) .: H c= G )thus
H is
open
by A10, TOPS_2:32;
( s in H & (P[01] a,b,t1,t2) .: H c= G )thus
s in H
by A11, XBOOLE_0:def 4;
(P[01] a,b,t1,t2) .: H c= Gthus
(P[01] a,b,t1,t2) .: H c= G
verumproof
let t be
set ;
TARSKI:def 3 ( not t in (P[01] a,b,t1,t2) .: H or t in G )
assume
t in (P[01] a,b,t1,t2) .: H
;
t in G
then consider r being
set such that
r in dom (P[01] a,b,t1,t2)
and A13:
r in H
and A14:
t = (P[01] a,b,t1,t2) . r
by FUNCT_1:def 12;
A15:
r in the
carrier of
(Closed-Interval-TSpace a,b)
by A13;
reconsider r =
r as
Point of
(Closed-Interval-TSpace a,b) by A13;
r in dom (P[01] a,b,t1,t2)
by A15, FUNCT_2:def 1;
then A16:
t in (P[01] a,b,t1,t2) .: the
carrier of
(Closed-Interval-TSpace a,b)
by A14, FUNCT_1:def 12;
reconsider p =
r as
Point of
R^1 by A2, TARSKI:def 3, TOPMETR:24;
p in [#] R^1
;
then A17:
p in dom f
by FUNCT_2:def 1;
(
t = f . p &
p in H0 )
by A4, A13, A14, XBOOLE_0:def 4;
then
t in f .: H0
by A17, FUNCT_1:def 12;
hence
t in G
by A8, A12, A16, XBOOLE_0:def 4;
verum
end; end;
hence
ex
H being
Subset of
(Closed-Interval-TSpace a,b) st
(
H is
open &
s in H &
(P[01] a,b,t1,t2) .: H c= G )
;
verum
end;
hence
P[01] a,
b,
t1,
t2 is_continuous_at s
by TMAP_1:48;
verum
end;
hence
P[01] a,b,t1,t2 is continuous Function of (Closed-Interval-TSpace a,b),(Closed-Interval-TSpace 0 ,1)
by TMAP_1:49; verum