:: TREAL_1 semantic presentation
begin
Lm1: for a, b being real number
for x being set st x in [.a,b.] holds
x is Real
;
Lm2: for a, b being real number
for x being Point of (Closed-Interval-TSpace (a,b)) st a <= b holds
x is Real
proof
let a, b be real number ; ::_thesis: for x being Point of (Closed-Interval-TSpace (a,b)) st a <= b holds
x is Real
let x be Point of (Closed-Interval-TSpace (a,b)); ::_thesis: ( a <= b implies x is Real )
assume a <= b ; ::_thesis: x is Real
then the carrier of (Closed-Interval-TSpace (a,b)) = [.a,b.] by TOPMETR:18;
hence x is Real by Lm1; ::_thesis: verum
end;
theorem Th1: :: TREAL_1:1
for a, b being real number
for A being Subset of R^1 st A = [.a,b.] holds
A is closed
proof
let a, b be real number ; ::_thesis: for A being Subset of R^1 st A = [.a,b.] holds
A is closed
let A be Subset of R^1; ::_thesis: ( A = [.a,b.] implies A is closed )
assume A1: A = [.a,b.] ; ::_thesis: A is closed
reconsider B = A ` as Subset of (TopSpaceMetr RealSpace) by TOPMETR:def_6;
reconsider a = a, b = b as Real by XREAL_0:def_1;
reconsider D = B as Subset of RealSpace by TOPMETR:12;
set C = D ` ;
A2: the carrier of RealSpace = the carrier of (TopSpaceMetr RealSpace) by TOPMETR:12;
for c being Point of RealSpace st c in B holds
ex r being real number st
( r > 0 & Ball (c,r) c= B )
proof
let c be Point of RealSpace; ::_thesis: ( c in B implies ex r being real number st
( r > 0 & Ball (c,r) c= B ) )
reconsider n = c as Real by METRIC_1:def_13;
assume c in B ; ::_thesis: ex r being real number st
( r > 0 & Ball (c,r) c= B )
then not n in [.a,b.] by A1, XBOOLE_0:def_5;
then A3: not n in { p where p is Real : ( a <= p & p <= b ) } by RCOMP_1:def_1;
now__::_thesis:_ex_r_being_Element_of_REAL_st_
(_r_>_0_&_Ball_(c,r)_c=_B_)
percases ( not a <= n or not n <= b ) by A3;
supposeA4: not a <= n ; ::_thesis: ex r being Element of REAL st
( r > 0 & Ball (c,r) c= B )
take r = a - n; ::_thesis: ( r > 0 & Ball (c,r) c= B )
now__::_thesis:_for_x_being_set_st_x_in_Ball_(c,r)_holds_
x_in_B
let x be set ; ::_thesis: ( x in Ball (c,r) implies x in B )
assume A5: x in Ball (c,r) ; ::_thesis: x in B
then reconsider t = x as Real by METRIC_1:def_13;
reconsider u = x as Point of RealSpace by A5;
Ball (c,r) = { q where q is Element of RealSpace : dist (c,q) < r } by METRIC_1:17;
then ex v being Element of RealSpace st
( v = u & dist (c,v) < r ) by A5;
then real_dist . (t,n) < r by METRIC_1:def_1, METRIC_1:def_13;
then A6: abs (t - n) < r by METRIC_1:def_12;
t - n <= abs (t - n) by ABSVALUE:4;
then t - n < a - n by A6, XXREAL_0:2;
then for q being Real holds
( not q = t or not a <= q or not q <= b ) by XREAL_1:9;
then not t in { p where p is Real : ( a <= p & p <= b ) } ;
then not u in D ` by A1, A2, RCOMP_1:def_1, TOPMETR:def_6;
hence x in B by SUBSET_1:29; ::_thesis: verum
end;
hence ( r > 0 & Ball (c,r) c= B ) by A4, TARSKI:def_3, XREAL_1:50; ::_thesis: verum
end;
supposeA7: not n <= b ; ::_thesis: ex r being Element of REAL st
( r > 0 & Ball (c,r) c= B )
take r = n - b; ::_thesis: ( r > 0 & Ball (c,r) c= B )
now__::_thesis:_for_x_being_set_st_x_in_Ball_(c,r)_holds_
x_in_B
let x be set ; ::_thesis: ( x in Ball (c,r) implies x in B )
assume A8: x in Ball (c,r) ; ::_thesis: x in B
then reconsider t = x as Real by METRIC_1:def_13;
reconsider u = x as Point of RealSpace by A8;
Ball (c,r) = { q where q is Element of RealSpace : dist (c,q) < r } by METRIC_1:17;
then ex v being Element of RealSpace st
( v = u & dist (c,v) < r ) by A8;
then real_dist . (n,t) < r by METRIC_1:def_1, METRIC_1:def_13;
then A9: abs (n - t) < r by METRIC_1:def_12;
n - t <= abs (n - t) by ABSVALUE:4;
then n - t < n - b by A9, XXREAL_0:2;
then for q being Real holds
( not q = t or not a <= q or not q <= b ) by XREAL_1:10;
then not t in { p where p is Real : ( a <= p & p <= b ) } ;
then not u in D ` by A1, A2, RCOMP_1:def_1, TOPMETR:def_6;
hence x in B by SUBSET_1:29; ::_thesis: verum
end;
hence ( r > 0 & Ball (c,r) c= B ) by A7, TARSKI:def_3, XREAL_1:50; ::_thesis: verum
end;
end;
end;
hence ex r being real number st
( r > 0 & Ball (c,r) c= B ) ; ::_thesis: verum
end;
then A ` is open by TOPMETR:15, TOPMETR:def_6;
hence A is closed by TOPS_1:3; ::_thesis: verum
end;
theorem Th2: :: TREAL_1:2
for a, b being real number st a <= b holds
Closed-Interval-TSpace (a,b) is closed
proof
let a, b be real number ; ::_thesis: ( a <= b implies Closed-Interval-TSpace (a,b) is closed )
assume a <= b ; ::_thesis: Closed-Interval-TSpace (a,b) is closed
then the carrier of (Closed-Interval-TSpace (a,b)) = [.a,b.] by TOPMETR:18;
then for A being Subset of R^1 st A = the carrier of (Closed-Interval-TSpace (a,b)) holds
A is closed by Th1;
hence Closed-Interval-TSpace (a,b) is closed by BORSUK_1:def_11; ::_thesis: verum
end;
theorem :: TREAL_1:3
for a, c, d, b being real number st a <= c & d <= b & c <= d holds
Closed-Interval-TSpace (c,d) is closed SubSpace of Closed-Interval-TSpace (a,b)
proof
let a, c, d, b be real number ; ::_thesis: ( a <= c & d <= b & c <= d implies Closed-Interval-TSpace (c,d) is closed SubSpace of Closed-Interval-TSpace (a,b) )
assume that
A1: a <= c and
A2: d <= b and
A3: c <= d ; ::_thesis: Closed-Interval-TSpace (c,d) is closed SubSpace of Closed-Interval-TSpace (a,b)
[.c,d.] c= [.a,b.] by A1, A2, XXREAL_1:34;
then A4: the carrier of (Closed-Interval-TSpace (c,d)) c= [.a,b.] by A3, TOPMETR:18;
A5: Closed-Interval-TSpace (c,d) is closed SubSpace of R^1 by A3, Th2;
a <= d by A1, A3, XXREAL_0:2;
then the carrier of (Closed-Interval-TSpace (c,d)) c= the carrier of (Closed-Interval-TSpace (a,b)) by A2, A4, TOPMETR:18, XXREAL_0:2;
hence Closed-Interval-TSpace (c,d) is closed SubSpace of Closed-Interval-TSpace (a,b) by A5, TSEP_1:14; ::_thesis: verum
end;
theorem :: TREAL_1:4
for a, c, b, d being real number st a <= c & b <= d & c <= b holds
( Closed-Interval-TSpace (a,d) = (Closed-Interval-TSpace (a,b)) union (Closed-Interval-TSpace (c,d)) & Closed-Interval-TSpace (c,b) = (Closed-Interval-TSpace (a,b)) meet (Closed-Interval-TSpace (c,d)) )
proof
let a, c, b, d be real number ; ::_thesis: ( a <= c & b <= d & c <= b implies ( Closed-Interval-TSpace (a,d) = (Closed-Interval-TSpace (a,b)) union (Closed-Interval-TSpace (c,d)) & Closed-Interval-TSpace (c,b) = (Closed-Interval-TSpace (a,b)) meet (Closed-Interval-TSpace (c,d)) ) )
assume that
A1: a <= c and
A2: b <= d and
A3: c <= b ; ::_thesis: ( Closed-Interval-TSpace (a,d) = (Closed-Interval-TSpace (a,b)) union (Closed-Interval-TSpace (c,d)) & Closed-Interval-TSpace (c,b) = (Closed-Interval-TSpace (a,b)) meet (Closed-Interval-TSpace (c,d)) )
A4: ( the carrier of (Closed-Interval-TSpace (a,b)) = [.a,b.] & the carrier of (Closed-Interval-TSpace (c,d)) = [.c,d.] ) by A1, A2, A3, TOPMETR:18, XXREAL_0:2;
a <= b by A1, A3, XXREAL_0:2;
then A5: the carrier of (Closed-Interval-TSpace (a,d)) = [.a,d.] by A2, TOPMETR:18, XXREAL_0:2;
A6: the carrier of (Closed-Interval-TSpace (c,b)) = [.c,b.] by A3, TOPMETR:18;
[.a,b.] \/ [.c,d.] = [.a,d.] by A1, A2, A3, XXREAL_1:174;
hence Closed-Interval-TSpace (a,d) = (Closed-Interval-TSpace (a,b)) union (Closed-Interval-TSpace (c,d)) by A4, A5, TSEP_1:def_2; ::_thesis: Closed-Interval-TSpace (c,b) = (Closed-Interval-TSpace (a,b)) meet (Closed-Interval-TSpace (c,d))
A7: [.a,b.] /\ [.c,d.] = [.c,b.] by A1, A2, XXREAL_1:143;
then the carrier of (Closed-Interval-TSpace (a,b)) /\ the carrier of (Closed-Interval-TSpace (c,d)) <> {} by A3, A4, XXREAL_1:1;
then the carrier of (Closed-Interval-TSpace (a,b)) meets the carrier of (Closed-Interval-TSpace (c,d)) by XBOOLE_0:def_7;
then Closed-Interval-TSpace (a,b) meets Closed-Interval-TSpace (c,d) by TSEP_1:def_3;
hence Closed-Interval-TSpace (c,b) = (Closed-Interval-TSpace (a,b)) meet (Closed-Interval-TSpace (c,d)) by A4, A6, A7, TSEP_1:def_4; ::_thesis: verum
end;
definition
let a, b be real number ;
assume A1: a <= b ;
func (#) (a,b) -> Point of (Closed-Interval-TSpace (a,b)) equals :Def1: :: TREAL_1:def 1
a;
coherence
a is Point of (Closed-Interval-TSpace (a,b))
proof
a in [.a,b.] by A1, XXREAL_1:1;
hence a is Point of (Closed-Interval-TSpace (a,b)) by A1, TOPMETR:18; ::_thesis: verum
end;
correctness
;
func(a,b) (#) -> Point of (Closed-Interval-TSpace (a,b)) equals :Def2: :: TREAL_1:def 2
b;
coherence
b is Point of (Closed-Interval-TSpace (a,b))
proof
b in [.a,b.] by A1, XXREAL_1:1;
hence b is Point of (Closed-Interval-TSpace (a,b)) by A1, TOPMETR:18; ::_thesis: verum
end;
correctness
;
end;
:: deftheorem Def1 defines (#) TREAL_1:def_1_:_
for a, b being real number st a <= b holds
(#) (a,b) = a;
:: deftheorem Def2 defines (#) TREAL_1:def_2_:_
for a, b being real number st a <= b holds
(a,b) (#) = b;
theorem :: TREAL_1:5
( 0[01] = (#) (0,1) & 1[01] = (0,1) (#) ) by Def1, Def2, BORSUK_1:def_14, BORSUK_1:def_15;
theorem :: TREAL_1:6
for a, b, c being real number st a <= b & b <= c holds
( (#) (a,b) = (#) (a,c) & (b,c) (#) = (a,c) (#) )
proof
let a, b, c be real number ; ::_thesis: ( a <= b & b <= c implies ( (#) (a,b) = (#) (a,c) & (b,c) (#) = (a,c) (#) ) )
assume that
A1: a <= b and
A2: b <= c ; ::_thesis: ( (#) (a,b) = (#) (a,c) & (b,c) (#) = (a,c) (#) )
thus (#) (a,b) = a by A1, Def1
.= (#) (a,c) by A1, A2, Def1, XXREAL_0:2 ; ::_thesis: (b,c) (#) = (a,c) (#)
thus (b,c) (#) = c by A2, Def2
.= (a,c) (#) by A1, A2, Def2, XXREAL_0:2 ; ::_thesis: verum
end;
begin
definition
let a, b be real number ;
assume B1: a <= b ;
let t1, t2 be Point of (Closed-Interval-TSpace (a,b));
func L[01] (t1,t2) -> Function of (Closed-Interval-TSpace (0,1)),(Closed-Interval-TSpace (a,b)) means :Def3: :: TREAL_1:def 3
for s being Point of (Closed-Interval-TSpace (0,1)) holds it . s = ((1 - s) * t1) + (s * t2);
existence
ex b1 being Function of (Closed-Interval-TSpace (0,1)),(Closed-Interval-TSpace (a,b)) st
for s being Point of (Closed-Interval-TSpace (0,1)) holds b1 . s = ((1 - s) * t1) + (s * t2)
proof
reconsider r1 = t1, r2 = t2 as Real by B1, Lm2;
deffunc H1( Element of REAL ) -> Element of REAL = ((1 - $1) * r1) + ($1 * r2);
consider LI being Function of REAL,REAL such that
A1: for r being Real holds LI . r = H1(r) from FUNCT_2:sch_4();
A2: [.a,b.] = the carrier of (Closed-Interval-TSpace (a,b)) by B1, TOPMETR:18;
now__::_thesis:_for_y_being_set_st_y_in_rng_(LI_|_[.0,1.])_holds_
y_in_[.a,b.]
let y be set ; ::_thesis: ( y in rng (LI | [.0,1.]) implies y in [.a,b.] )
assume A3: y in rng (LI | [.0,1.]) ; ::_thesis: y in [.a,b.]
then reconsider d = y as Real ;
y in LI .: [.0,1.] by A3, RELAT_1:115;
then consider x being set such that
x in dom LI and
A4: x in [.0,1.] and
A5: y = LI . x by FUNCT_1:def_6;
reconsider c = x as Real by A4;
A6: d = ((1 - c) * r1) + (c * r2) by A1, A5;
r1 in [.a,b.] by A2;
then r1 in { p where p is Real : ( a <= p & p <= b ) } by RCOMP_1:def_1;
then A7: ex v1 being Real st
( v1 = r1 & a <= v1 & v1 <= b ) ;
c in { p where p is Real : ( 0 <= p & p <= 1 ) } by A4, RCOMP_1:def_1;
then A8: ex u being Real st
( u = c & 0 <= u & u <= 1 ) ;
r2 in [.a,b.] by A2;
then r2 in { p where p is Real : ( a <= p & p <= b ) } by RCOMP_1:def_1;
then A9: ex v2 being Real st
( v2 = r2 & a <= v2 & v2 <= b ) ;
then A10: c * a <= c * r2 by A8, XREAL_1:64;
A11: c * r2 <= c * b by A8, A9, XREAL_1:64;
A12: 0 <= 1 - c by A8, XREAL_1:48;
then (1 - c) * r1 <= (1 - c) * b by A7, XREAL_1:64;
then A13: d <= ((1 - c) * b) + (c * b) by A6, A11, XREAL_1:7;
(1 - c) * a <= (1 - c) * r1 by A7, A12, XREAL_1:64;
then ((1 - c) * a) + (c * a) <= d by A6, A10, XREAL_1:7;
then y in { q where q is Real : ( a <= q & q <= b ) } by A13;
hence y in [.a,b.] by RCOMP_1:def_1; ::_thesis: verum
end;
then A14: rng (LI | [.0,1.]) c= the carrier of (Closed-Interval-TSpace (a,b)) by A2, TARSKI:def_3;
A15: dom (LI | [.0,1.]) = (dom LI) /\ [.0,1.] by RELAT_1:61;
( [.0,1.] = REAL /\ [.0,1.] & dom LI = REAL ) by FUNCT_2:def_1, XBOOLE_1:28;
then dom (LI | [.0,1.]) = the carrier of (Closed-Interval-TSpace (0,1)) by A15, TOPMETR:18;
then reconsider F = LI | [.0,1.] as Function of (Closed-Interval-TSpace (0,1)),(Closed-Interval-TSpace (a,b)) by A14, FUNCT_2:def_1, RELSET_1:4;
take F ; ::_thesis: for s being Point of (Closed-Interval-TSpace (0,1)) holds F . s = ((1 - s) * t1) + (s * t2)
let s be Point of (Closed-Interval-TSpace (0,1)); ::_thesis: F . s = ((1 - s) * t1) + (s * t2)
A16: s is Real by XREAL_0:def_1;
the carrier of (Closed-Interval-TSpace (0,1)) = [.0,1.] by TOPMETR:18;
hence F . s = LI . s by FUNCT_1:49
.= ((1 - s) * t1) + (s * t2) by A1, A16 ;
::_thesis: verum
end;
uniqueness
for b1, b2 being Function of (Closed-Interval-TSpace (0,1)),(Closed-Interval-TSpace (a,b)) st ( for s being Point of (Closed-Interval-TSpace (0,1)) holds b1 . s = ((1 - s) * t1) + (s * t2) ) & ( for s being Point of (Closed-Interval-TSpace (0,1)) holds b2 . s = ((1 - s) * t1) + (s * t2) ) holds
b1 = b2
proof
let F1, F2 be Function of (Closed-Interval-TSpace (0,1)),(Closed-Interval-TSpace (a,b)); ::_thesis: ( ( for s being Point of (Closed-Interval-TSpace (0,1)) holds F1 . s = ((1 - s) * t1) + (s * t2) ) & ( for s being Point of (Closed-Interval-TSpace (0,1)) holds F2 . s = ((1 - s) * t1) + (s * t2) ) implies F1 = F2 )
assume A17: for s being Point of (Closed-Interval-TSpace (0,1)) holds F1 . s = ((1 - s) * t1) + (s * t2) ; ::_thesis: ( ex s being Point of (Closed-Interval-TSpace (0,1)) st not F2 . s = ((1 - s) * t1) + (s * t2) or F1 = F2 )
assume A18: for s being Point of (Closed-Interval-TSpace (0,1)) holds F2 . s = ((1 - s) * t1) + (s * t2) ; ::_thesis: F1 = F2
for s being Point of (Closed-Interval-TSpace (0,1)) holds F1 . s = F2 . s
proof
reconsider r1 = t1, r2 = t2 as Real by B1, Lm2;
let s be Point of (Closed-Interval-TSpace (0,1)); ::_thesis: F1 . s = F2 . s
reconsider r = s as Real by Lm2;
thus F1 . s = ((1 - r) * r1) + (r * r2) by A17
.= F2 . s by A18 ; ::_thesis: verum
end;
hence F1 = F2 by FUNCT_2:63; ::_thesis: verum
end;
end;
:: deftheorem Def3 defines L[01] TREAL_1:def_3_:_
for a, b being real number st a <= b holds
for t1, t2 being Point of (Closed-Interval-TSpace (a,b))
for b5 being Function of (Closed-Interval-TSpace (0,1)),(Closed-Interval-TSpace (a,b)) holds
( b5 = L[01] (t1,t2) iff for s being Point of (Closed-Interval-TSpace (0,1)) holds b5 . s = ((1 - s) * t1) + (s * t2) );
theorem Th7: :: TREAL_1:7
for a, b being real number st a <= b holds
for t1, t2 being Point of (Closed-Interval-TSpace (a,b))
for s being Point of (Closed-Interval-TSpace (0,1)) holds (L[01] (t1,t2)) . s = ((t2 - t1) * s) + t1
proof
let a, b be real number ; ::_thesis: ( a <= b implies for t1, t2 being Point of (Closed-Interval-TSpace (a,b))
for s being Point of (Closed-Interval-TSpace (0,1)) holds (L[01] (t1,t2)) . s = ((t2 - t1) * s) + t1 )
assume A1: a <= b ; ::_thesis: for t1, t2 being Point of (Closed-Interval-TSpace (a,b))
for s being Point of (Closed-Interval-TSpace (0,1)) holds (L[01] (t1,t2)) . s = ((t2 - t1) * s) + t1
let t1, t2 be Point of (Closed-Interval-TSpace (a,b)); ::_thesis: for s being Point of (Closed-Interval-TSpace (0,1)) holds (L[01] (t1,t2)) . s = ((t2 - t1) * s) + t1
let s be Point of (Closed-Interval-TSpace (0,1)); ::_thesis: (L[01] (t1,t2)) . s = ((t2 - t1) * s) + t1
thus (L[01] (t1,t2)) . s = ((1 - s) * t1) + (s * t2) by A1, Def3
.= ((t2 - t1) * s) + t1 ; ::_thesis: verum
end;
theorem Th8: :: TREAL_1:8
for a, b being real number st a <= b holds
for t1, t2 being Point of (Closed-Interval-TSpace (a,b)) holds L[01] (t1,t2) is continuous
proof
let a, b be real number ; ::_thesis: ( a <= b implies for t1, t2 being Point of (Closed-Interval-TSpace (a,b)) holds L[01] (t1,t2) is continuous )
assume A1: a <= b ; ::_thesis: for t1, t2 being Point of (Closed-Interval-TSpace (a,b)) holds L[01] (t1,t2) is continuous
let t1, t2 be Point of (Closed-Interval-TSpace (a,b)); ::_thesis: L[01] (t1,t2) is continuous
reconsider r1 = t1, r2 = t2 as Real by A1, Lm2;
deffunc H1( Element of REAL ) -> Element of REAL = ((r2 - r1) * $1) + r1;
consider L being Function of REAL,REAL such that
A2: for r being Real holds L . r = H1(r) from FUNCT_2:sch_4();
reconsider f = L as Function of R^1,R^1 by TOPMETR:17;
A3: for s being Point of (Closed-Interval-TSpace (0,1))
for w being Point of R^1 st s = w holds
(L[01] (t1,t2)) . s = f . w
proof
let s be Point of (Closed-Interval-TSpace (0,1)); ::_thesis: for w being Point of R^1 st s = w holds
(L[01] (t1,t2)) . s = f . w
let w be Point of R^1; ::_thesis: ( s = w implies (L[01] (t1,t2)) . s = f . w )
reconsider r = s as Real by Lm2;
assume A4: s = w ; ::_thesis: (L[01] (t1,t2)) . s = f . w
thus (L[01] (t1,t2)) . s = ((r2 - r1) * r) + r1 by A1, Th7
.= f . w by A2, A4 ; ::_thesis: verum
end;
A5: [.0,1.] = the carrier of (Closed-Interval-TSpace (0,1)) by TOPMETR:18;
A6: f is continuous by A2, TOPMETR:21;
for s being Point of (Closed-Interval-TSpace (0,1)) holds L[01] (t1,t2) is_continuous_at s
proof
let s be Point of (Closed-Interval-TSpace (0,1)); ::_thesis: L[01] (t1,t2) is_continuous_at s
reconsider w = s as Point of R^1 by A5, TARSKI:def_3, TOPMETR:17;
for G being Subset of (Closed-Interval-TSpace (a,b)) st G is open & (L[01] (t1,t2)) . s in G holds
ex H being Subset of (Closed-Interval-TSpace (0,1)) st
( H is open & s in H & (L[01] (t1,t2)) .: H c= G )
proof
let G be Subset of (Closed-Interval-TSpace (a,b)); ::_thesis: ( G is open & (L[01] (t1,t2)) . s in G implies ex H being Subset of (Closed-Interval-TSpace (0,1)) st
( H is open & s in H & (L[01] (t1,t2)) .: H c= G ) )
assume G is open ; ::_thesis: ( not (L[01] (t1,t2)) . s in G or ex H being Subset of (Closed-Interval-TSpace (0,1)) st
( H is open & s in H & (L[01] (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 (a,b))) = G by TOPS_2:24;
A9: f is_continuous_at w by A6, TMAP_1:44;
assume (L[01] (t1,t2)) . s in G ; ::_thesis: ex H being Subset of (Closed-Interval-TSpace (0,1)) st
( H is open & s in H & (L[01] (t1,t2)) .: H c= G )
then f . w in G by A3;
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:43;
now__::_thesis:_ex_H_being_Subset_of_(Closed-Interval-TSpace_(0,1))_st_
(_H_is_open_&_s_in_H_&_(L[01]_(t1,t2))_.:_H_c=_G_)
reconsider H = H0 /\ ([#] (Closed-Interval-TSpace (0,1))) as Subset of (Closed-Interval-TSpace (0,1)) ;
take H = H; ::_thesis: ( H is open & s in H & (L[01] (t1,t2)) .: H c= G )
thus H is open by A10, TOPS_2:24; ::_thesis: ( s in H & (L[01] (t1,t2)) .: H c= G )
thus s in H by A11, XBOOLE_0:def_4; ::_thesis: (L[01] (t1,t2)) .: H c= G
thus (L[01] (t1,t2)) .: H c= G ::_thesis: verum
proof
let t be set ; :: according to TARSKI:def_3 ::_thesis: ( not t in (L[01] (t1,t2)) .: H or t in G )
assume t in (L[01] (t1,t2)) .: H ; ::_thesis: t in G
then consider r being set such that
r in dom (L[01] (t1,t2)) and
A13: r in H and
A14: t = (L[01] (t1,t2)) . r by FUNCT_1:def_6;
A15: r in the carrier of (Closed-Interval-TSpace (0,1)) by A13;
reconsider r = r as Point of (Closed-Interval-TSpace (0,1)) by A13;
r in dom (L[01] (t1,t2)) by A15, FUNCT_2:def_1;
then A16: t in (L[01] (t1,t2)) .: the carrier of (Closed-Interval-TSpace (0,1)) by A14, FUNCT_1:def_6;
reconsider p = r as Point of R^1 by A5, TARSKI:def_3, TOPMETR:17;
p in [#] R^1 ;
then A17: p in dom f by FUNCT_2:def_1;
( t = f . p & p in H0 ) by A3, A13, A14, XBOOLE_0:def_4;
then t in f .: H0 by A17, FUNCT_1:def_6;
hence t in G by A8, A12, A16, XBOOLE_0:def_4; ::_thesis: verum
end;
end;
hence ex H being Subset of (Closed-Interval-TSpace (0,1)) st
( H is open & s in H & (L[01] (t1,t2)) .: H c= G ) ; ::_thesis: verum
end;
hence L[01] (t1,t2) is_continuous_at s by TMAP_1:43; ::_thesis: verum
end;
hence L[01] (t1,t2) is continuous by TMAP_1:44; ::_thesis: verum
end;
theorem :: TREAL_1:9
for a, b being real number st a <= b holds
for t1, t2 being Point of (Closed-Interval-TSpace (a,b)) holds
( (L[01] (t1,t2)) . ((#) (0,1)) = t1 & (L[01] (t1,t2)) . ((0,1) (#)) = t2 )
proof
let a, b be real number ; ::_thesis: ( a <= b implies for t1, t2 being Point of (Closed-Interval-TSpace (a,b)) holds
( (L[01] (t1,t2)) . ((#) (0,1)) = t1 & (L[01] (t1,t2)) . ((0,1) (#)) = t2 ) )
assume A1: a <= b ; ::_thesis: for t1, t2 being Point of (Closed-Interval-TSpace (a,b)) holds
( (L[01] (t1,t2)) . ((#) (0,1)) = t1 & (L[01] (t1,t2)) . ((0,1) (#)) = t2 )
let t1, t2 be Point of (Closed-Interval-TSpace (a,b)); ::_thesis: ( (L[01] (t1,t2)) . ((#) (0,1)) = t1 & (L[01] (t1,t2)) . ((0,1) (#)) = t2 )
reconsider r1 = t1, r2 = t2 as Real by A1, Lm2;
0 = (#) (0,1) by Def1;
hence (L[01] (t1,t2)) . ((#) (0,1)) = ((1 - 0) * r1) + (0 * r2) by A1, Def3
.= t1 ;
::_thesis: (L[01] (t1,t2)) . ((0,1) (#)) = t2
1 = (0,1) (#) by Def2;
hence (L[01] (t1,t2)) . ((0,1) (#)) = ((1 - 1) * r1) + (1 * r2) by A1, Def3
.= t2 ;
::_thesis: verum
end;
theorem :: TREAL_1:10
L[01] (((#) (0,1)),((0,1) (#))) = id (Closed-Interval-TSpace (0,1))
proof
for x being Point of (Closed-Interval-TSpace (0,1)) holds (L[01] (((#) (0,1)),((0,1) (#)))) . x = x
proof
let x be Point of (Closed-Interval-TSpace (0,1)); ::_thesis: (L[01] (((#) (0,1)),((0,1) (#)))) . x = x
reconsider y = x as Real by Lm2;
( (#) (0,1) = 0 & (0,1) (#) = 1 ) by Def1, Def2;
hence (L[01] (((#) (0,1)),((0,1) (#)))) . x = ((1 - y) * 0) + (y * 1) by Def3
.= x ;
::_thesis: verum
end;
hence L[01] (((#) (0,1)),((0,1) (#))) = id (Closed-Interval-TSpace (0,1)) by FUNCT_2:124; ::_thesis: verum
end;
definition
let a, b be real number ;
assume B1: a < b ;
let t1, t2 be Point of (Closed-Interval-TSpace (0,1));
func P[01] (a,b,t1,t2) -> Function of (Closed-Interval-TSpace (a,b)),(Closed-Interval-TSpace (0,1)) means :Def4: :: TREAL_1:def 4
for s being Point of (Closed-Interval-TSpace (a,b)) holds it . s = (((b - s) * t1) + ((s - a) * t2)) / (b - a);
existence
ex b1 being Function of (Closed-Interval-TSpace (a,b)),(Closed-Interval-TSpace (0,1)) st
for s being Point of (Closed-Interval-TSpace (a,b)) holds b1 . s = (((b - s) * t1) + ((s - a) * t2)) / (b - a)
proof
reconsider a1 = a, b1 = b as Real by XREAL_0:def_1;
reconsider r1 = t1, r2 = t2 as Real by Lm2;
deffunc H1( Element of REAL ) -> Element of REAL = (((b1 - $1) * r1) + (($1 - a1) * r2)) / (b1 - a1);
consider PI being Function of REAL,REAL such that
A1: for r being Real holds PI . r = H1(r) from FUNCT_2:sch_4();
A2: [.0,1.] = the carrier of (Closed-Interval-TSpace (0,1)) by TOPMETR:18;
now__::_thesis:_for_y_being_set_st_y_in_rng_(PI_|_[.a,b.])_holds_
y_in_[.0,1.]
let y be set ; ::_thesis: ( y in rng (PI | [.a,b.]) implies y in [.0,1.] )
assume A3: y in rng (PI | [.a,b.]) ; ::_thesis: y in [.0,1.]
then reconsider d = y as Real ;
y in PI .: [.a,b.] by A3, RELAT_1:115;
then consider x being set such that
x in dom PI and
A4: x in [.a,b.] and
A5: y = PI . x by FUNCT_1:def_6;
reconsider c = x as Real by A4;
A6: d = (((b - c) * r1) + ((c - a) * r2)) / (b - a) by A1, A5;
r1 in [.0,1.] by A2;
then r1 in { p where p is Real : ( 0 <= p & p <= 1 ) } by RCOMP_1:def_1;
then A7: ex v1 being Real st
( v1 = r1 & 0 <= v1 & v1 <= 1 ) ;
c in { p where p is Real : ( a <= p & p <= b ) } by A4, RCOMP_1:def_1;
then A8: ex u being Real st
( u = c & a <= u & u <= b ) ;
then A9: 0 <= c - a by XREAL_1:48;
r2 in [.0,1.] by A2;
then r2 in { p where p is Real : ( 0 <= p & p <= 1 ) } by RCOMP_1:def_1;
then A10: ex v2 being Real st
( v2 = r2 & 0 <= v2 & v2 <= 1 ) ;
then A11: (c - a) * r2 <= c - a by A9, XREAL_1:153;
A12: 0 < b - a by B1, XREAL_1:50;
A13: 0 <= b - c by A8, XREAL_1:48;
then (b - c) * r1 <= b - c by A7, XREAL_1:153;
then ((b - c) * r1) + ((c - a) * r2) <= (b + (- c)) + (c - a) by A11, XREAL_1:7;
then d <= (b - a) / (b - a) by A12, A6, XREAL_1:72;
then d <= 1 by A12, XCMPLX_1:60;
then y in { q where q is Real : ( 0 <= q & q <= 1 ) } by A7, A10, A12, A6, A13, A9;
hence y in [.0,1.] by RCOMP_1:def_1; ::_thesis: verum
end;
then A14: rng (PI | [.a,b.]) c= the carrier of (Closed-Interval-TSpace (0,1)) by A2, TARSKI:def_3;
A15: dom (PI | [.a,b.]) = (dom PI) /\ [.a,b.] by RELAT_1:61;
( [.a,b.] = REAL /\ [.a,b.] & dom PI = REAL ) by FUNCT_2:def_1, XBOOLE_1:28;
then dom (PI | [.a,b.]) = the carrier of (Closed-Interval-TSpace (a,b)) by B1, A15, TOPMETR:18;
then reconsider F = PI | [.a,b.] as Function of (Closed-Interval-TSpace (a,b)),(Closed-Interval-TSpace (0,1)) by A14, FUNCT_2:def_1, RELSET_1:4;
take F ; ::_thesis: for s being Point of (Closed-Interval-TSpace (a,b)) holds F . s = (((b - s) * t1) + ((s - a) * t2)) / (b - a)
let s be Point of (Closed-Interval-TSpace (a,b)); ::_thesis: F . s = (((b - s) * t1) + ((s - a) * t2)) / (b - a)
A16: s is Real by XREAL_0:def_1;
the carrier of (Closed-Interval-TSpace (a,b)) = [.a,b.] by B1, TOPMETR:18;
hence F . s = PI . s by FUNCT_1:49
.= (((b - s) * t1) + ((s - a) * t2)) / (b - a) by A1, A16 ;
::_thesis: verum
end;
uniqueness
for b1, b2 being Function of (Closed-Interval-TSpace (a,b)),(Closed-Interval-TSpace (0,1)) st ( for s being Point of (Closed-Interval-TSpace (a,b)) holds b1 . s = (((b - s) * t1) + ((s - a) * t2)) / (b - a) ) & ( for s being Point of (Closed-Interval-TSpace (a,b)) holds b2 . s = (((b - s) * t1) + ((s - a) * t2)) / (b - a) ) holds
b1 = b2
proof
let F1, F2 be Function of (Closed-Interval-TSpace (a,b)),(Closed-Interval-TSpace (0,1)); ::_thesis: ( ( for s being Point of (Closed-Interval-TSpace (a,b)) holds F1 . s = (((b - s) * t1) + ((s - a) * t2)) / (b - a) ) & ( for s being Point of (Closed-Interval-TSpace (a,b)) holds F2 . s = (((b - s) * t1) + ((s - a) * t2)) / (b - a) ) implies F1 = F2 )
assume A17: for s being Point of (Closed-Interval-TSpace (a,b)) holds F1 . s = (((b - s) * t1) + ((s - a) * t2)) / (b - a) ; ::_thesis: ( ex s being Point of (Closed-Interval-TSpace (a,b)) st not F2 . s = (((b - s) * t1) + ((s - a) * t2)) / (b - a) or F1 = F2 )
assume A18: for s being Point of (Closed-Interval-TSpace (a,b)) holds F2 . s = (((b - s) * t1) + ((s - a) * t2)) / (b - a) ; ::_thesis: F1 = F2
let s be Point of (Closed-Interval-TSpace (a,b)); :: according to FUNCT_2:def_8 ::_thesis: F1 . s = F2 . s
reconsider r = s as Real by B1, Lm2;
reconsider r1 = t1, r2 = t2 as Real by Lm2;
thus F1 . s = (((b - r) * r1) + ((r - a) * r2)) / (b - a) by A17
.= F2 . s by A18 ; ::_thesis: verum
end;
end;
:: deftheorem Def4 defines P[01] TREAL_1:def_4_:_
for a, b being real number st a < b holds
for t1, t2 being Point of (Closed-Interval-TSpace (0,1))
for b5 being Function of (Closed-Interval-TSpace (a,b)),(Closed-Interval-TSpace (0,1)) holds
( b5 = P[01] (a,b,t1,t2) iff for s being Point of (Closed-Interval-TSpace (a,b)) holds b5 . s = (((b - s) * t1) + ((s - a) * t2)) / (b - a) );
theorem Th11: :: TREAL_1:11
for a, b being real number st a < b holds
for t1, t2 being Point of (Closed-Interval-TSpace (0,1))
for s being Point of (Closed-Interval-TSpace (a,b)) holds (P[01] (a,b,t1,t2)) . s = (((t2 - t1) / (b - a)) * s) + (((b * t1) - (a * t2)) / (b - a))
proof
let a, b be real number ; ::_thesis: ( a < b implies for t1, t2 being Point of (Closed-Interval-TSpace (0,1))
for s being Point of (Closed-Interval-TSpace (a,b)) holds (P[01] (a,b,t1,t2)) . s = (((t2 - t1) / (b - a)) * s) + (((b * t1) - (a * t2)) / (b - a)) )
assume A1: a < b ; ::_thesis: for t1, t2 being Point of (Closed-Interval-TSpace (0,1))
for s being Point of (Closed-Interval-TSpace (a,b)) holds (P[01] (a,b,t1,t2)) . s = (((t2 - t1) / (b - a)) * s) + (((b * t1) - (a * t2)) / (b - a))
let t1, t2 be Point of (Closed-Interval-TSpace (0,1)); ::_thesis: for s being Point of (Closed-Interval-TSpace (a,b)) holds (P[01] (a,b,t1,t2)) . s = (((t2 - t1) / (b - a)) * s) + (((b * t1) - (a * t2)) / (b - a))
let s be Point of (Closed-Interval-TSpace (a,b)); ::_thesis: (P[01] (a,b,t1,t2)) . s = (((t2 - t1) / (b - a)) * s) + (((b * t1) - (a * t2)) / (b - a))
thus (P[01] (a,b,t1,t2)) . s = (((b - s) * t1) + ((s - a) * t2)) / (b - a) by A1, Def4
.= ((s * (t2 - t1)) + ((b * t1) - (a * t2))) / (b - a)
.= ((s * (t2 - t1)) / (b - a)) + (((b * t1) - (a * t2)) / (b - a)) by XCMPLX_1:62
.= ((s * (t2 - t1)) * (1 / (b - a))) + (((b * t1) - (a * t2)) / (b - a)) by XCMPLX_1:99
.= (((t2 - t1) * (1 / (b - a))) * s) + (((b * t1) - (a * t2)) / (b - a))
.= (((t2 - t1) / (b - a)) * s) + (((b * t1) - (a * t2)) / (b - a)) by XCMPLX_1:99 ; ::_thesis: verum
end;
theorem Th12: :: TREAL_1:12
for a, b being real number st a < b holds
for t1, t2 being Point of (Closed-Interval-TSpace (0,1)) holds P[01] (a,b,t1,t2) is continuous
proof
let a, b be real number ; ::_thesis: ( a < b implies for t1, t2 being Point of (Closed-Interval-TSpace (0,1)) holds P[01] (a,b,t1,t2) is continuous )
assume A1: a < b ; ::_thesis: for t1, t2 being Point of (Closed-Interval-TSpace (0,1)) holds P[01] (a,b,t1,t2) is continuous
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:18;
let t1, t2 be Point of (Closed-Interval-TSpace (0,1)); ::_thesis: P[01] (a,b,t1,t2) is continuous
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:17;
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)); ::_thesis: for w being Point of R^1 st s = w holds
(P[01] (a,b,t1,t2)) . s = f . w
let w be Point of R^1; ::_thesis: ( s = w implies (P[01] (a,b,t1,t2)) . s = f . w )
reconsider r = s as Real by A1, Lm2;
assume A5: s = w ; ::_thesis: (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, Th11
.= f . w by A3, A5 ; ::_thesis: verum
end;
A6: f is continuous by A3, TOPMETR:21;
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)); ::_thesis: P[01] (a,b,t1,t2) is_continuous_at s
reconsider w = s as Point of R^1 by A2, TARSKI:def_3, TOPMETR:17;
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)); ::_thesis: ( 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 ; ::_thesis: ( 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:24;
A9: f is_continuous_at w by A6, TMAP_1:44;
assume (P[01] (a,b,t1,t2)) . s in G ; ::_thesis: 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:43;
now__::_thesis:_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_)
reconsider H = H0 /\ ([#] (Closed-Interval-TSpace (a,b))) as Subset of (Closed-Interval-TSpace (a,b)) ;
take H = H; ::_thesis: ( H is open & s in H & (P[01] (a,b,t1,t2)) .: H c= G )
thus H is open by A10, TOPS_2:24; ::_thesis: ( s in H & (P[01] (a,b,t1,t2)) .: H c= G )
thus s in H by A11, XBOOLE_0:def_4; ::_thesis: (P[01] (a,b,t1,t2)) .: H c= G
thus (P[01] (a,b,t1,t2)) .: H c= G ::_thesis: verum
proof
let t be set ; :: according to TARSKI:def_3 ::_thesis: ( not t in (P[01] (a,b,t1,t2)) .: H or t in G )
assume t in (P[01] (a,b,t1,t2)) .: H ; ::_thesis: 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_6;
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_6;
reconsider p = r as Point of R^1 by A2, TARSKI:def_3, TOPMETR:17;
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_6;
hence t in G by A8, A12, A16, XBOOLE_0:def_4; ::_thesis: 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 ) ; ::_thesis: verum
end;
hence P[01] (a,b,t1,t2) is_continuous_at s by TMAP_1:43; ::_thesis: verum
end;
hence P[01] (a,b,t1,t2) is continuous by TMAP_1:44; ::_thesis: verum
end;
theorem :: TREAL_1:13
for a, b being real number st a < b holds
for t1, t2 being Point of (Closed-Interval-TSpace (0,1)) holds
( (P[01] (a,b,t1,t2)) . ((#) (a,b)) = t1 & (P[01] (a,b,t1,t2)) . ((a,b) (#)) = t2 )
proof
let a, b be real number ; ::_thesis: ( a < b implies for t1, t2 being Point of (Closed-Interval-TSpace (0,1)) holds
( (P[01] (a,b,t1,t2)) . ((#) (a,b)) = t1 & (P[01] (a,b,t1,t2)) . ((a,b) (#)) = t2 ) )
assume A1: a < b ; ::_thesis: for t1, t2 being Point of (Closed-Interval-TSpace (0,1)) holds
( (P[01] (a,b,t1,t2)) . ((#) (a,b)) = t1 & (P[01] (a,b,t1,t2)) . ((a,b) (#)) = t2 )
then A2: b - a <> 0 ;
let t1, t2 be Point of (Closed-Interval-TSpace (0,1)); ::_thesis: ( (P[01] (a,b,t1,t2)) . ((#) (a,b)) = t1 & (P[01] (a,b,t1,t2)) . ((a,b) (#)) = t2 )
reconsider r1 = t1, r2 = t2 as Real by Lm2;
a = (#) (a,b) by A1, Def1;
hence (P[01] (a,b,t1,t2)) . ((#) (a,b)) = (((b - a) * r1) + ((a - a) * r2)) / (b - a) by A1, Def4
.= t1 by A2, XCMPLX_1:89 ;
::_thesis: (P[01] (a,b,t1,t2)) . ((a,b) (#)) = t2
b = (a,b) (#) by A1, Def2;
hence (P[01] (a,b,t1,t2)) . ((a,b) (#)) = (((b - b) * r1) + ((b - a) * r2)) / (b - a) by A1, Def4
.= t2 by A2, XCMPLX_1:89 ;
::_thesis: verum
end;
theorem :: TREAL_1:14
P[01] (0,1,((#) (0,1)),((0,1) (#))) = id (Closed-Interval-TSpace (0,1))
proof
for x being Point of (Closed-Interval-TSpace (0,1)) holds (P[01] (0,1,((#) (0,1)),((0,1) (#)))) . x = x
proof
let x be Point of (Closed-Interval-TSpace (0,1)); ::_thesis: (P[01] (0,1,((#) (0,1)),((0,1) (#)))) . x = x
reconsider y = x as Real by Lm2;
( (#) (0,1) = 0 & (0,1) (#) = 1 ) by Def1, Def2;
hence (P[01] (0,1,((#) (0,1)),((0,1) (#)))) . x = (((1 - y) * 0) + ((y - 0) * 1)) / (1 - 0) by Def4
.= x ;
::_thesis: verum
end;
hence P[01] (0,1,((#) (0,1)),((0,1) (#))) = id (Closed-Interval-TSpace (0,1)) by FUNCT_2:124; ::_thesis: verum
end;
theorem Th15: :: TREAL_1:15
for a, b being real number st a < b holds
( id (Closed-Interval-TSpace (a,b)) = (L[01] (((#) (a,b)),((a,b) (#)))) * (P[01] (a,b,((#) (0,1)),((0,1) (#)))) & id (Closed-Interval-TSpace (0,1)) = (P[01] (a,b,((#) (0,1)),((0,1) (#)))) * (L[01] (((#) (a,b)),((a,b) (#)))) )
proof
let a, b be real number ; ::_thesis: ( a < b implies ( id (Closed-Interval-TSpace (a,b)) = (L[01] (((#) (a,b)),((a,b) (#)))) * (P[01] (a,b,((#) (0,1)),((0,1) (#)))) & id (Closed-Interval-TSpace (0,1)) = (P[01] (a,b,((#) (0,1)),((0,1) (#)))) * (L[01] (((#) (a,b)),((a,b) (#)))) ) )
A1: ( 0 = (#) (0,1) & 1 = (0,1) (#) ) by Def1, Def2;
set L = L[01] (((#) (a,b)),((a,b) (#)));
set P = P[01] (a,b,((#) (0,1)),((0,1) (#)));
assume A2: a < b ; ::_thesis: ( id (Closed-Interval-TSpace (a,b)) = (L[01] (((#) (a,b)),((a,b) (#)))) * (P[01] (a,b,((#) (0,1)),((0,1) (#)))) & id (Closed-Interval-TSpace (0,1)) = (P[01] (a,b,((#) (0,1)),((0,1) (#)))) * (L[01] (((#) (a,b)),((a,b) (#)))) )
then A3: b - a <> 0 ;
A4: ( a = (#) (a,b) & b = (a,b) (#) ) by A2, Def1, Def2;
for c being Point of (Closed-Interval-TSpace (a,b)) holds ((L[01] (((#) (a,b)),((a,b) (#)))) * (P[01] (a,b,((#) (0,1)),((0,1) (#))))) . c = c
proof
let c be Point of (Closed-Interval-TSpace (a,b)); ::_thesis: ((L[01] (((#) (a,b)),((a,b) (#)))) * (P[01] (a,b,((#) (0,1)),((0,1) (#))))) . c = c
reconsider r = c as Real by A2, Lm2;
A5: (P[01] (a,b,((#) (0,1)),((0,1) (#)))) . c = (((b - r) * 0) + ((r - a) * 1)) / (b - a) by A2, A1, Def4
.= (r - a) / (b - a) ;
thus ((L[01] (((#) (a,b)),((a,b) (#)))) * (P[01] (a,b,((#) (0,1)),((0,1) (#))))) . c = (L[01] (((#) (a,b)),((a,b) (#)))) . ((P[01] (a,b,((#) (0,1)),((0,1) (#)))) . c) by FUNCT_2:15
.= ((1 - ((r - a) / (b - a))) * a) + (((r - a) / (b - a)) * b) by A2, A4, A5, Def3
.= ((((1 * (b - a)) - (r - a)) / (b - a)) * a) + (((r - a) / (b - a)) * b) by A3, XCMPLX_1:127
.= (((b - r) / (b - a)) * (a / 1)) + (((r - a) / (b - a)) * b)
.= (((b - r) * a) / (1 * (b - a))) + (((r - a) / (b - a)) * b) by XCMPLX_1:76
.= (((b - r) * a) / (b - a)) + (((r - a) / (b - a)) * (b / 1))
.= (((b - r) * a) / (b - a)) + (((r - a) * b) / (1 * (b - a))) by XCMPLX_1:76
.= (((a * b) - (a * r)) + ((r - a) * b)) / (b - a) by XCMPLX_1:62
.= ((b - a) * r) / (b - a)
.= c by A3, XCMPLX_1:89 ; ::_thesis: verum
end;
hence id (Closed-Interval-TSpace (a,b)) = (L[01] (((#) (a,b)),((a,b) (#)))) * (P[01] (a,b,((#) (0,1)),((0,1) (#)))) by FUNCT_2:124; ::_thesis: id (Closed-Interval-TSpace (0,1)) = (P[01] (a,b,((#) (0,1)),((0,1) (#)))) * (L[01] (((#) (a,b)),((a,b) (#))))
for c being Point of (Closed-Interval-TSpace (0,1)) holds ((P[01] (a,b,((#) (0,1)),((0,1) (#)))) * (L[01] (((#) (a,b)),((a,b) (#))))) . c = c
proof
let c be Point of (Closed-Interval-TSpace (0,1)); ::_thesis: ((P[01] (a,b,((#) (0,1)),((0,1) (#)))) * (L[01] (((#) (a,b)),((a,b) (#))))) . c = c
reconsider r = c as Real by Lm2;
A6: (L[01] (((#) (a,b)),((a,b) (#)))) . c = ((1 - r) * a) + (r * b) by A2, A4, Def3
.= (r * (b - a)) + a ;
thus ((P[01] (a,b,((#) (0,1)),((0,1) (#)))) * (L[01] (((#) (a,b)),((a,b) (#))))) . c = (P[01] (a,b,((#) (0,1)),((0,1) (#)))) . ((L[01] (((#) (a,b)),((a,b) (#)))) . c) by FUNCT_2:15
.= (((b - ((r * (b - a)) + a)) * 0) + ((((r * (b - a)) + a) - a) * 1)) / (b - a) by A2, A1, A6, Def4
.= c by A3, XCMPLX_1:89 ; ::_thesis: verum
end;
hence id (Closed-Interval-TSpace (0,1)) = (P[01] (a,b,((#) (0,1)),((0,1) (#)))) * (L[01] (((#) (a,b)),((a,b) (#)))) by FUNCT_2:124; ::_thesis: verum
end;
theorem Th16: :: TREAL_1:16
for a, b being real number st a < b holds
( id (Closed-Interval-TSpace (a,b)) = (L[01] (((a,b) (#)),((#) (a,b)))) * (P[01] (a,b,((0,1) (#)),((#) (0,1)))) & id (Closed-Interval-TSpace (0,1)) = (P[01] (a,b,((0,1) (#)),((#) (0,1)))) * (L[01] (((a,b) (#)),((#) (a,b)))) )
proof
let a, b be real number ; ::_thesis: ( a < b implies ( id (Closed-Interval-TSpace (a,b)) = (L[01] (((a,b) (#)),((#) (a,b)))) * (P[01] (a,b,((0,1) (#)),((#) (0,1)))) & id (Closed-Interval-TSpace (0,1)) = (P[01] (a,b,((0,1) (#)),((#) (0,1)))) * (L[01] (((a,b) (#)),((#) (a,b)))) ) )
A1: ( 0 = (#) (0,1) & 1 = (0,1) (#) ) by Def1, Def2;
set L = L[01] (((a,b) (#)),((#) (a,b)));
set P = P[01] (a,b,((0,1) (#)),((#) (0,1)));
assume A2: a < b ; ::_thesis: ( id (Closed-Interval-TSpace (a,b)) = (L[01] (((a,b) (#)),((#) (a,b)))) * (P[01] (a,b,((0,1) (#)),((#) (0,1)))) & id (Closed-Interval-TSpace (0,1)) = (P[01] (a,b,((0,1) (#)),((#) (0,1)))) * (L[01] (((a,b) (#)),((#) (a,b)))) )
then A3: b - a <> 0 ;
A4: ( a = (#) (a,b) & b = (a,b) (#) ) by A2, Def1, Def2;
for c being Point of (Closed-Interval-TSpace (a,b)) holds ((L[01] (((a,b) (#)),((#) (a,b)))) * (P[01] (a,b,((0,1) (#)),((#) (0,1))))) . c = c
proof
let c be Point of (Closed-Interval-TSpace (a,b)); ::_thesis: ((L[01] (((a,b) (#)),((#) (a,b)))) * (P[01] (a,b,((0,1) (#)),((#) (0,1))))) . c = c
reconsider r = c as Real by A2, Lm2;
A5: (P[01] (a,b,((0,1) (#)),((#) (0,1)))) . c = (((b - r) * 1) + ((r - a) * 0)) / (b - a) by A2, A1, Def4
.= (b - r) / (b - a) ;
thus ((L[01] (((a,b) (#)),((#) (a,b)))) * (P[01] (a,b,((0,1) (#)),((#) (0,1))))) . c = (L[01] (((a,b) (#)),((#) (a,b)))) . ((P[01] (a,b,((0,1) (#)),((#) (0,1)))) . c) by FUNCT_2:15
.= ((1 - ((b - r) / (b - a))) * b) + (((b - r) / (b - a)) * a) by A2, A4, A5, Def3
.= ((((1 * (b - a)) - (b - r)) / (b - a)) * b) + (((b - r) / (b - a)) * a) by A3, XCMPLX_1:127
.= (((r - a) / (b - a)) * (b / 1)) + (((b - r) / (b - a)) * a)
.= (((r - a) * b) / (1 * (b - a))) + (((b - r) / (b - a)) * a) by XCMPLX_1:76
.= (((r - a) * b) / (b - a)) + (((b - r) / (b - a)) * (a / 1))
.= (((r - a) * b) / (b - a)) + (((b - r) * a) / (1 * (b - a))) by XCMPLX_1:76
.= (((b * r) - (b * a)) + ((b - r) * a)) / (b - a) by XCMPLX_1:62
.= ((b - a) * r) / (b - a)
.= c by A3, XCMPLX_1:89 ; ::_thesis: verum
end;
hence id (Closed-Interval-TSpace (a,b)) = (L[01] (((a,b) (#)),((#) (a,b)))) * (P[01] (a,b,((0,1) (#)),((#) (0,1)))) by FUNCT_2:124; ::_thesis: id (Closed-Interval-TSpace (0,1)) = (P[01] (a,b,((0,1) (#)),((#) (0,1)))) * (L[01] (((a,b) (#)),((#) (a,b))))
for c being Point of (Closed-Interval-TSpace (0,1)) holds ((P[01] (a,b,((0,1) (#)),((#) (0,1)))) * (L[01] (((a,b) (#)),((#) (a,b))))) . c = c
proof
let c be Point of (Closed-Interval-TSpace (0,1)); ::_thesis: ((P[01] (a,b,((0,1) (#)),((#) (0,1)))) * (L[01] (((a,b) (#)),((#) (a,b))))) . c = c
reconsider r = c as Real by Lm2;
A6: (L[01] (((a,b) (#)),((#) (a,b)))) . c = ((1 - r) * b) + (r * a) by A2, A4, Def3
.= (r * (a - b)) + b ;
thus ((P[01] (a,b,((0,1) (#)),((#) (0,1)))) * (L[01] (((a,b) (#)),((#) (a,b))))) . c = (P[01] (a,b,((0,1) (#)),((#) (0,1)))) . ((L[01] (((a,b) (#)),((#) (a,b)))) . c) by FUNCT_2:15
.= (((b - ((r * (a - b)) + b)) * 1) + ((((r * (a - b)) + b) - a) * 0)) / (b - a) by A2, A1, A6, Def4
.= (r * (- (a - b))) / (b - a)
.= c by A3, XCMPLX_1:89 ; ::_thesis: verum
end;
hence id (Closed-Interval-TSpace (0,1)) = (P[01] (a,b,((0,1) (#)),((#) (0,1)))) * (L[01] (((a,b) (#)),((#) (a,b)))) by FUNCT_2:124; ::_thesis: verum
end;
theorem Th17: :: TREAL_1:17
for a, b being real number st a < b holds
( L[01] (((#) (a,b)),((a,b) (#))) is being_homeomorphism & (L[01] (((#) (a,b)),((a,b) (#)))) " = P[01] (a,b,((#) (0,1)),((0,1) (#))) & P[01] (a,b,((#) (0,1)),((0,1) (#))) is being_homeomorphism & (P[01] (a,b,((#) (0,1)),((0,1) (#)))) " = L[01] (((#) (a,b)),((a,b) (#))) )
proof
let a, b be real number ; ::_thesis: ( a < b implies ( L[01] (((#) (a,b)),((a,b) (#))) is being_homeomorphism & (L[01] (((#) (a,b)),((a,b) (#)))) " = P[01] (a,b,((#) (0,1)),((0,1) (#))) & P[01] (a,b,((#) (0,1)),((0,1) (#))) is being_homeomorphism & (P[01] (a,b,((#) (0,1)),((0,1) (#)))) " = L[01] (((#) (a,b)),((a,b) (#))) ) )
set L = L[01] (((#) (a,b)),((a,b) (#)));
set P = P[01] (a,b,((#) (0,1)),((0,1) (#)));
assume A1: a < b ; ::_thesis: ( L[01] (((#) (a,b)),((a,b) (#))) is being_homeomorphism & (L[01] (((#) (a,b)),((a,b) (#)))) " = P[01] (a,b,((#) (0,1)),((0,1) (#))) & P[01] (a,b,((#) (0,1)),((0,1) (#))) is being_homeomorphism & (P[01] (a,b,((#) (0,1)),((0,1) (#)))) " = L[01] (((#) (a,b)),((a,b) (#))) )
then A2: id the carrier of (Closed-Interval-TSpace (0,1)) = (P[01] (a,b,((#) (0,1)),((0,1) (#)))) * (L[01] (((#) (a,b)),((a,b) (#)))) by Th15;
then A3: L[01] (((#) (a,b)),((a,b) (#))) is one-to-one by FUNCT_2:23;
A4: ( L[01] (((#) (a,b)),((a,b) (#))) is continuous & P[01] (a,b,((#) (0,1)),((0,1) (#))) is continuous Function of (Closed-Interval-TSpace (a,b)),(Closed-Interval-TSpace (0,1)) ) by A1, Th8, Th12;
A5: id the carrier of (Closed-Interval-TSpace (a,b)) = id (Closed-Interval-TSpace (a,b))
.= (L[01] (((#) (a,b)),((a,b) (#)))) * (P[01] (a,b,((#) (0,1)),((0,1) (#)))) by A1, Th15 ;
then A6: L[01] (((#) (a,b)),((a,b) (#))) is onto by FUNCT_2:23;
then A7: rng (L[01] (((#) (a,b)),((a,b) (#)))) = [#] (Closed-Interval-TSpace (a,b)) by FUNCT_2:def_3;
A8: (L[01] (((#) (a,b)),((a,b) (#)))) " = (L[01] (((#) (a,b)),((a,b) (#)))) " by A3, A6, TOPS_2:def_4;
( dom (L[01] (((#) (a,b)),((a,b) (#)))) = [#] (Closed-Interval-TSpace (0,1)) & P[01] (a,b,((#) (0,1)),((0,1) (#))) = (L[01] (((#) (a,b)),((a,b) (#)))) " ) by A2, A3, A7, FUNCT_2:30, FUNCT_2:def_1;
hence L[01] (((#) (a,b)),((a,b) (#))) is being_homeomorphism by A3, A7, A8, A4, TOPS_2:def_5; ::_thesis: ( (L[01] (((#) (a,b)),((a,b) (#)))) " = P[01] (a,b,((#) (0,1)),((0,1) (#))) & P[01] (a,b,((#) (0,1)),((0,1) (#))) is being_homeomorphism & (P[01] (a,b,((#) (0,1)),((0,1) (#)))) " = L[01] (((#) (a,b)),((a,b) (#))) )
thus (L[01] (((#) (a,b)),((a,b) (#)))) " = P[01] (a,b,((#) (0,1)),((0,1) (#))) by A2, A3, A7, A8, FUNCT_2:30; ::_thesis: ( P[01] (a,b,((#) (0,1)),((0,1) (#))) is being_homeomorphism & (P[01] (a,b,((#) (0,1)),((0,1) (#)))) " = L[01] (((#) (a,b)),((a,b) (#))) )
A9: P[01] (a,b,((#) (0,1)),((0,1) (#))) is onto by A2, FUNCT_2:23;
then A10: rng (P[01] (a,b,((#) (0,1)),((0,1) (#)))) = [#] (Closed-Interval-TSpace (0,1)) by FUNCT_2:def_3;
A11: ( L[01] (((#) (a,b)),((a,b) (#))) is continuous Function of (Closed-Interval-TSpace (0,1)),(Closed-Interval-TSpace (a,b)) & P[01] (a,b,((#) (0,1)),((0,1) (#))) is continuous ) by A1, Th8, Th12;
A12: P[01] (a,b,((#) (0,1)),((0,1) (#))) is one-to-one by A5, FUNCT_2:23;
A13: (P[01] (a,b,((#) (0,1)),((0,1) (#)))) " = (P[01] (a,b,((#) (0,1)),((0,1) (#)))) " by A12, A9, TOPS_2:def_4;
( dom (P[01] (a,b,((#) (0,1)),((0,1) (#)))) = [#] (Closed-Interval-TSpace (a,b)) & L[01] (((#) (a,b)),((a,b) (#))) = (P[01] (a,b,((#) (0,1)),((0,1) (#)))) " ) by A10, A5, A12, FUNCT_2:30, FUNCT_2:def_1;
hence P[01] (a,b,((#) (0,1)),((0,1) (#))) is being_homeomorphism by A10, A12, A13, A11, TOPS_2:def_5; ::_thesis: (P[01] (a,b,((#) (0,1)),((0,1) (#)))) " = L[01] (((#) (a,b)),((a,b) (#)))
thus (P[01] (a,b,((#) (0,1)),((0,1) (#)))) " = L[01] (((#) (a,b)),((a,b) (#))) by A10, A5, A12, A13, FUNCT_2:30; ::_thesis: verum
end;
theorem :: TREAL_1:18
for a, b being real number st a < b holds
( L[01] (((a,b) (#)),((#) (a,b))) is being_homeomorphism & (L[01] (((a,b) (#)),((#) (a,b)))) " = P[01] (a,b,((0,1) (#)),((#) (0,1))) & P[01] (a,b,((0,1) (#)),((#) (0,1))) is being_homeomorphism & (P[01] (a,b,((0,1) (#)),((#) (0,1)))) " = L[01] (((a,b) (#)),((#) (a,b))) )
proof
let a, b be real number ; ::_thesis: ( a < b implies ( L[01] (((a,b) (#)),((#) (a,b))) is being_homeomorphism & (L[01] (((a,b) (#)),((#) (a,b)))) " = P[01] (a,b,((0,1) (#)),((#) (0,1))) & P[01] (a,b,((0,1) (#)),((#) (0,1))) is being_homeomorphism & (P[01] (a,b,((0,1) (#)),((#) (0,1)))) " = L[01] (((a,b) (#)),((#) (a,b))) ) )
set L = L[01] (((a,b) (#)),((#) (a,b)));
set P = P[01] (a,b,((0,1) (#)),((#) (0,1)));
assume A1: a < b ; ::_thesis: ( L[01] (((a,b) (#)),((#) (a,b))) is being_homeomorphism & (L[01] (((a,b) (#)),((#) (a,b)))) " = P[01] (a,b,((0,1) (#)),((#) (0,1))) & P[01] (a,b,((0,1) (#)),((#) (0,1))) is being_homeomorphism & (P[01] (a,b,((0,1) (#)),((#) (0,1)))) " = L[01] (((a,b) (#)),((#) (a,b))) )
then A2: id the carrier of (Closed-Interval-TSpace (0,1)) = (P[01] (a,b,((0,1) (#)),((#) (0,1)))) * (L[01] (((a,b) (#)),((#) (a,b)))) by Th16;
then A3: L[01] (((a,b) (#)),((#) (a,b))) is one-to-one by FUNCT_2:23;
A4: ( L[01] (((a,b) (#)),((#) (a,b))) is continuous & P[01] (a,b,((0,1) (#)),((#) (0,1))) is continuous Function of (Closed-Interval-TSpace (a,b)),(Closed-Interval-TSpace (0,1)) ) by A1, Th8, Th12;
A5: id the carrier of (Closed-Interval-TSpace (a,b)) = id (Closed-Interval-TSpace (a,b))
.= (L[01] (((a,b) (#)),((#) (a,b)))) * (P[01] (a,b,((0,1) (#)),((#) (0,1)))) by A1, Th16 ;
then A6: L[01] (((a,b) (#)),((#) (a,b))) is onto by FUNCT_2:23;
then A7: rng (L[01] (((a,b) (#)),((#) (a,b)))) = [#] (Closed-Interval-TSpace (a,b)) by FUNCT_2:def_3;
A8: (L[01] (((a,b) (#)),((#) (a,b)))) " = (L[01] (((a,b) (#)),((#) (a,b)))) " by A3, A6, TOPS_2:def_4;
( dom (L[01] (((a,b) (#)),((#) (a,b)))) = [#] (Closed-Interval-TSpace (0,1)) & P[01] (a,b,((0,1) (#)),((#) (0,1))) = (L[01] (((a,b) (#)),((#) (a,b)))) " ) by A2, A3, A7, FUNCT_2:30, FUNCT_2:def_1;
hence L[01] (((a,b) (#)),((#) (a,b))) is being_homeomorphism by A3, A7, A8, A4, TOPS_2:def_5; ::_thesis: ( (L[01] (((a,b) (#)),((#) (a,b)))) " = P[01] (a,b,((0,1) (#)),((#) (0,1))) & P[01] (a,b,((0,1) (#)),((#) (0,1))) is being_homeomorphism & (P[01] (a,b,((0,1) (#)),((#) (0,1)))) " = L[01] (((a,b) (#)),((#) (a,b))) )
thus (L[01] (((a,b) (#)),((#) (a,b)))) " = P[01] (a,b,((0,1) (#)),((#) (0,1))) by A2, A3, A7, A8, FUNCT_2:30; ::_thesis: ( P[01] (a,b,((0,1) (#)),((#) (0,1))) is being_homeomorphism & (P[01] (a,b,((0,1) (#)),((#) (0,1)))) " = L[01] (((a,b) (#)),((#) (a,b))) )
A9: P[01] (a,b,((0,1) (#)),((#) (0,1))) is onto by A2, FUNCT_2:23;
then A10: rng (P[01] (a,b,((0,1) (#)),((#) (0,1)))) = [#] (Closed-Interval-TSpace (0,1)) by FUNCT_2:def_3;
A11: ( L[01] (((a,b) (#)),((#) (a,b))) is continuous Function of (Closed-Interval-TSpace (0,1)),(Closed-Interval-TSpace (a,b)) & P[01] (a,b,((0,1) (#)),((#) (0,1))) is continuous ) by A1, Th8, Th12;
A12: P[01] (a,b,((0,1) (#)),((#) (0,1))) is one-to-one by A5, FUNCT_2:23;
A13: (P[01] (a,b,((0,1) (#)),((#) (0,1)))) " = (P[01] (a,b,((0,1) (#)),((#) (0,1)))) " by A12, A9, TOPS_2:def_4;
( dom (P[01] (a,b,((0,1) (#)),((#) (0,1)))) = [#] (Closed-Interval-TSpace (a,b)) & L[01] (((a,b) (#)),((#) (a,b))) = (P[01] (a,b,((0,1) (#)),((#) (0,1)))) " ) by A10, A5, A12, FUNCT_2:30, FUNCT_2:def_1;
hence P[01] (a,b,((0,1) (#)),((#) (0,1))) is being_homeomorphism by A10, A12, A13, A11, TOPS_2:def_5; ::_thesis: (P[01] (a,b,((0,1) (#)),((#) (0,1)))) " = L[01] (((a,b) (#)),((#) (a,b)))
thus (P[01] (a,b,((0,1) (#)),((#) (0,1)))) " = L[01] (((a,b) (#)),((#) (a,b))) by A10, A5, A12, A13, FUNCT_2:30; ::_thesis: verum
end;
begin
theorem Th19: :: TREAL_1:19
I[01] is connected
proof
for A, B being Subset of I[01] st [#] I[01] = A \/ B & A <> {} I[01] & B <> {} I[01] & A is closed & B is closed holds
A meets B
proof
let A, B be Subset of I[01]; ::_thesis: ( [#] I[01] = A \/ B & A <> {} I[01] & B <> {} I[01] & A is closed & B is closed implies A meets B )
assume that
A1: [#] I[01] = A \/ B and
A2: A <> {} I[01] and
A3: B <> {} I[01] and
A4: A is closed and
A5: B is closed ; ::_thesis: A meets B
reconsider P = A, Q = B as Subset of REAL by BORSUK_1:40, XBOOLE_1:1;
assume A6: A misses B ; ::_thesis: contradiction
set x = the Element of P;
reconsider x = the Element of P as Real by A2, TARSKI:def_3;
A7: now__::_thesis:_ex_x_being_Real_st_x_in_P
take x = x; ::_thesis: x in P
thus x in P by A2; ::_thesis: verum
end;
set x = the Element of Q;
reconsider x = the Element of Q as Real by A3, TARSKI:def_3;
A8: now__::_thesis:_ex_x_being_Real_st_x_in_Q
take x = x; ::_thesis: x in Q
thus x in Q by A3; ::_thesis: verum
end;
A9: the carrier of RealSpace = the carrier of (TopSpaceMetr RealSpace) by TOPMETR:12;
0 is LowerBound of P
proof
let r be ext-real number ; :: according to XXREAL_2:def_2 ::_thesis: ( not r in P or 0 <= r )
assume r in P ; ::_thesis: 0 <= r
then r in [.0,1.] by BORSUK_1:40;
then r in { w where w is Real : ( 0 <= w & w <= 1 ) } by RCOMP_1:def_1;
then ex u being Real st
( u = r & 0 <= u & u <= 1 ) ;
hence 0 <= r ; ::_thesis: verum
end;
then A10: P is bounded_below by XXREAL_2:def_9;
0 is LowerBound of Q
proof
let r be ext-real number ; :: according to XXREAL_2:def_2 ::_thesis: ( not r in Q or 0 <= r )
assume r in Q ; ::_thesis: 0 <= r
then r in [.0,1.] by BORSUK_1:40;
then r in { w where w is Real : ( 0 <= w & w <= 1 ) } by RCOMP_1:def_1;
then ex u being Real st
( u = r & 0 <= u & u <= 1 ) ;
hence 0 <= r ; ::_thesis: verum
end;
then A11: Q is bounded_below by XXREAL_2:def_9;
reconsider A0 = P, B0 = Q as Subset of R^1 by METRIC_1:def_13, TOPMETR:12, TOPMETR:def_6;
A12: I[01] is closed SubSpace of R^1 by Th2, TOPMETR:20;
then A13: A0 is closed by A4, TSEP_1:12;
A14: B0 is closed by A5, A12, TSEP_1:12;
0 in { w where w is Real : ( 0 <= w & w <= 1 ) } ;
then A15: 0 in [.0,1.] by RCOMP_1:def_1;
now__::_thesis:_contradiction
percases ( 0 in P or 0 in Q ) by A1, A15, BORSUK_1:40, XBOOLE_0:def_3;
supposeA16: 0 in P ; ::_thesis: contradiction
reconsider B00 = B0 ` as Subset of R^1 ;
set l = lower_bound Q;
reconsider m = lower_bound Q as Point of RealSpace by METRIC_1:def_13;
reconsider t = m as Point of R^1 by TOPMETR:12, TOPMETR:def_6;
set W = { w where w is Real : ( 0 <= w & w < lower_bound Q ) } ;
A17: lower_bound Q in Q
proof
assume not lower_bound Q in Q ; ::_thesis: contradiction
then A18: t in B00 by SUBSET_1:29;
B00 is open by A14, TOPS_1:3;
then consider s being real number such that
A19: s > 0 and
A20: Ball (m,s) c= B0 ` by A18, TOPMETR:15, TOPMETR:def_6;
consider r being real number such that
A21: r in Q and
A22: r < (lower_bound Q) + s by A8, A11, A19, SEQ_4:def_2;
reconsider r = r as Real by XREAL_0:def_1;
lower_bound Q <= r by A11, A21, SEQ_4:def_2;
then (lower_bound Q) - r <= 0 by XREAL_1:47;
then A23: - s < - ((lower_bound Q) - r) by A19, XREAL_1:24;
reconsider rm = r as Point of RealSpace by METRIC_1:def_13;
r - (lower_bound Q) < s by A22, XREAL_1:19;
then abs (r - (lower_bound Q)) < s by A23, SEQ_2:1;
then the distance of RealSpace . (rm,m) < s by METRIC_1:def_12, METRIC_1:def_13;
then dist (m,rm) < s by METRIC_1:def_1;
then rm in { q where q is Element of RealSpace : dist (m,q) < s } ;
then rm in Ball (m,s) by METRIC_1:17;
hence contradiction by A20, A21, XBOOLE_0:def_5; ::_thesis: verum
end;
then lower_bound Q in [.0,1.] by BORSUK_1:40;
then lower_bound Q in { u where u is Real : ( 0 <= u & u <= 1 ) } by RCOMP_1:def_1;
then A24: ex u0 being Real st
( u0 = lower_bound Q & 0 <= u0 & u0 <= 1 ) ;
now__::_thesis:_for_x_being_set_st_x_in__{__w_where_w_is_Real_:_(_0_<=_w_&_w_<_lower_bound_Q_)__}__holds_
x_in_P
let x be set ; ::_thesis: ( x in { w where w is Real : ( 0 <= w & w < lower_bound Q ) } implies x in P )
assume x in { w where w is Real : ( 0 <= w & w < lower_bound Q ) } ; ::_thesis: x in P
then consider w0 being Real such that
A25: w0 = x and
A26: 0 <= w0 and
A27: w0 < lower_bound Q ;
w0 <= 1 by A24, A27, XXREAL_0:2;
then w0 in { u where u is Real : ( 0 <= u & u <= 1 ) } by A26;
then w0 in P \/ Q by A1, BORSUK_1:40, RCOMP_1:def_1;
then ( w0 in P or w0 in Q ) by XBOOLE_0:def_3;
hence x in P by A11, A25, A27, SEQ_4:def_2; ::_thesis: verum
end;
then A28: { w where w is Real : ( 0 <= w & w < lower_bound Q ) } c= P by TARSKI:def_3;
then reconsider D = { w where w is Real : ( 0 <= w & w < lower_bound Q ) } as Subset of R^1 by A9, METRIC_1:def_13, TOPMETR:def_6, XBOOLE_1:1;
A29: not 0 in Q by A6, A16, XBOOLE_0:3;
now__::_thesis:_for_G_being_Subset_of_R^1_st_G_is_open_&_t_in_G_holds_
D_meets_G
let G be Subset of R^1; ::_thesis: ( G is open & t in G implies D meets G )
assume A30: G is open ; ::_thesis: ( t in G implies D meets G )
assume t in G ; ::_thesis: D meets G
then consider e being real number such that
A31: e > 0 and
A32: Ball (m,e) c= G by A30, TOPMETR:15, TOPMETR:def_6;
reconsider e = e as Element of REAL by XREAL_0:def_1;
set e0 = max (0,((lower_bound Q) - (e / 2)));
reconsider e1 = max (0,((lower_bound Q) - (e / 2))) as Point of RealSpace by METRIC_1:def_13;
A33: e * (1 / 2) < e * 1 by A31, XREAL_1:68;
now__::_thesis:_abs_((lower_bound_Q)_-_(max_(0,((lower_bound_Q)_-_(e_/_2)))))_<_e
percases ( max (0,((lower_bound Q) - (e / 2))) = 0 or max (0,((lower_bound Q) - (e / 2))) = (lower_bound Q) - (e / 2) ) by XXREAL_0:16;
supposeA34: max (0,((lower_bound Q) - (e / 2))) = 0 ; ::_thesis: abs ((lower_bound Q) - (max (0,((lower_bound Q) - (e / 2))))) < e
then lower_bound Q <= e / 2 by XREAL_1:50, XXREAL_0:25;
then lower_bound Q < e by A33, XXREAL_0:2;
hence abs ((lower_bound Q) - (max (0,((lower_bound Q) - (e / 2))))) < e by A24, A34, ABSVALUE:def_1; ::_thesis: verum
end;
suppose max (0,((lower_bound Q) - (e / 2))) = (lower_bound Q) - (e / 2) ; ::_thesis: abs ((lower_bound Q) - (max (0,((lower_bound Q) - (e / 2))))) < e
hence abs ((lower_bound Q) - (max (0,((lower_bound Q) - (e / 2))))) < e by A31, A33, ABSVALUE:def_1; ::_thesis: verum
end;
end;
end;
then the distance of RealSpace . (m,e1) < e by METRIC_1:def_12, METRIC_1:def_13;
then dist (m,e1) < e by METRIC_1:def_1;
then e1 in { z where z is Element of RealSpace : dist (m,z) < e } ;
then A35: e1 in Ball (m,e) by METRIC_1:17;
( max (0,((lower_bound Q) - (e / 2))) = 0 or max (0,((lower_bound Q) - (e / 2))) = (lower_bound Q) - (e / 2) ) by XXREAL_0:16;
then ( 0 <= max (0,((lower_bound Q) - (e / 2))) & max (0,((lower_bound Q) - (e / 2))) < lower_bound Q ) by A29, A17, A24, A31, XREAL_1:44, XREAL_1:139, XXREAL_0:25;
then max (0,((lower_bound Q) - (e / 2))) in { w where w is Real : ( 0 <= w & w < lower_bound Q ) } ;
hence D meets G by A32, A35, XBOOLE_0:3; ::_thesis: verum
end;
then A36: t in Cl D by PRE_TOPC:24;
A37: Cl A0 = A0 by A13, PRE_TOPC:22;
Cl D c= Cl A0 by A28, PRE_TOPC:19;
hence contradiction by A6, A17, A36, A37, XBOOLE_0:3; ::_thesis: verum
end;
supposeA38: 0 in Q ; ::_thesis: contradiction
reconsider A00 = A0 ` as Subset of R^1 ;
set l = lower_bound P;
reconsider m = lower_bound P as Point of RealSpace by METRIC_1:def_13;
reconsider t = m as Point of R^1 by TOPMETR:12, TOPMETR:def_6;
set W = { w where w is Real : ( 0 <= w & w < lower_bound P ) } ;
A39: lower_bound P in P
proof
assume not lower_bound P in P ; ::_thesis: contradiction
then A40: t in A00 by SUBSET_1:29;
A00 is open by A13, TOPS_1:3;
then consider s being real number such that
A41: s > 0 and
A42: Ball (m,s) c= A0 ` by A40, TOPMETR:15, TOPMETR:def_6;
consider r being real number such that
A43: r in P and
A44: r < (lower_bound P) + s by A7, A10, A41, SEQ_4:def_2;
reconsider r = r as Real by XREAL_0:def_1;
lower_bound P <= r by A10, A43, SEQ_4:def_2;
then (lower_bound P) - r <= 0 by XREAL_1:47;
then A45: - s < - ((lower_bound P) - r) by A41, XREAL_1:24;
reconsider rm = r as Point of RealSpace by METRIC_1:def_13;
r - (lower_bound P) < s by A44, XREAL_1:19;
then abs (r - (lower_bound P)) < s by A45, SEQ_2:1;
then real_dist . (r,(lower_bound P)) < s by METRIC_1:def_12;
then dist (rm,m) < s by METRIC_1:def_1, METRIC_1:def_13;
then rm in { q where q is Element of RealSpace : dist (m,q) < s } ;
then rm in Ball (m,s) by METRIC_1:17;
hence contradiction by A42, A43, XBOOLE_0:def_5; ::_thesis: verum
end;
then lower_bound P in [.0,1.] by BORSUK_1:40;
then lower_bound P in { u where u is Real : ( 0 <= u & u <= 1 ) } by RCOMP_1:def_1;
then A46: ex u0 being Real st
( u0 = lower_bound P & 0 <= u0 & u0 <= 1 ) ;
now__::_thesis:_for_x_being_set_st_x_in__{__w_where_w_is_Real_:_(_0_<=_w_&_w_<_lower_bound_P_)__}__holds_
x_in_Q
let x be set ; ::_thesis: ( x in { w where w is Real : ( 0 <= w & w < lower_bound P ) } implies x in Q )
assume x in { w where w is Real : ( 0 <= w & w < lower_bound P ) } ; ::_thesis: x in Q
then consider w0 being Real such that
A47: w0 = x and
A48: 0 <= w0 and
A49: w0 < lower_bound P ;
w0 <= 1 by A46, A49, XXREAL_0:2;
then w0 in { u where u is Real : ( 0 <= u & u <= 1 ) } by A48;
then w0 in P \/ Q by A1, BORSUK_1:40, RCOMP_1:def_1;
then ( w0 in P or w0 in Q ) by XBOOLE_0:def_3;
hence x in Q by A10, A47, A49, SEQ_4:def_2; ::_thesis: verum
end;
then A50: { w where w is Real : ( 0 <= w & w < lower_bound P ) } c= Q by TARSKI:def_3;
then reconsider D = { w where w is Real : ( 0 <= w & w < lower_bound P ) } as Subset of R^1 by A9, METRIC_1:def_13, TOPMETR:def_6, XBOOLE_1:1;
A51: not 0 in P by A6, A38, XBOOLE_0:3;
now__::_thesis:_for_G_being_Subset_of_R^1_st_G_is_open_&_t_in_G_holds_
D_meets_G
let G be Subset of R^1; ::_thesis: ( G is open & t in G implies D meets G )
assume A52: G is open ; ::_thesis: ( t in G implies D meets G )
assume t in G ; ::_thesis: D meets G
then consider e being real number such that
A53: e > 0 and
A54: Ball (m,e) c= G by A52, TOPMETR:15, TOPMETR:def_6;
reconsider e = e as Real by XREAL_0:def_1;
set e0 = max (0,((lower_bound P) - (e / 2)));
reconsider e1 = max (0,((lower_bound P) - (e / 2))) as Point of RealSpace by METRIC_1:def_13;
A55: e * (1 / 2) < e * 1 by A53, XREAL_1:68;
now__::_thesis:_abs_((lower_bound_P)_-_(max_(0,((lower_bound_P)_-_(e_/_2)))))_<_e
percases ( max (0,((lower_bound P) - (e / 2))) = 0 or max (0,((lower_bound P) - (e / 2))) = (lower_bound P) - (e / 2) ) by XXREAL_0:16;
supposeA56: max (0,((lower_bound P) - (e / 2))) = 0 ; ::_thesis: abs ((lower_bound P) - (max (0,((lower_bound P) - (e / 2))))) < e
then lower_bound P <= e / 2 by XREAL_1:50, XXREAL_0:25;
then lower_bound P < e by A55, XXREAL_0:2;
hence abs ((lower_bound P) - (max (0,((lower_bound P) - (e / 2))))) < e by A46, A56, ABSVALUE:def_1; ::_thesis: verum
end;
suppose max (0,((lower_bound P) - (e / 2))) = (lower_bound P) - (e / 2) ; ::_thesis: abs ((lower_bound P) - (max (0,((lower_bound P) - (e / 2))))) < e
hence abs ((lower_bound P) - (max (0,((lower_bound P) - (e / 2))))) < e by A53, A55, ABSVALUE:def_1; ::_thesis: verum
end;
end;
end;
then real_dist . ((lower_bound P),(max (0,((lower_bound P) - (e / 2))))) < e by METRIC_1:def_12;
then dist (m,e1) < e by METRIC_1:def_1, METRIC_1:def_13;
then e1 in { z where z is Element of RealSpace : dist (m,z) < e } ;
then A57: e1 in Ball (m,e) by METRIC_1:17;
( max (0,((lower_bound P) - (e / 2))) = 0 or max (0,((lower_bound P) - (e / 2))) = (lower_bound P) - (e / 2) ) by XXREAL_0:16;
then ( 0 <= max (0,((lower_bound P) - (e / 2))) & max (0,((lower_bound P) - (e / 2))) < lower_bound P ) by A51, A39, A46, A53, XREAL_1:44, XREAL_1:139, XXREAL_0:25;
then max (0,((lower_bound P) - (e / 2))) in { w where w is Real : ( 0 <= w & w < lower_bound P ) } ;
hence D meets G by A54, A57, XBOOLE_0:3; ::_thesis: verum
end;
then A58: t in Cl D by PRE_TOPC:24;
A59: Cl B0 = B0 by A14, PRE_TOPC:22;
Cl D c= Cl B0 by A50, PRE_TOPC:19;
hence contradiction by A6, A39, A58, A59, XBOOLE_0:3; ::_thesis: verum
end;
end;
end;
hence contradiction ; ::_thesis: verum
end;
hence I[01] is connected by CONNSP_1:10; ::_thesis: verum
end;
theorem :: TREAL_1:20
for a, b being real number st a <= b holds
Closed-Interval-TSpace (a,b) is connected
proof
let a, b be real number ; ::_thesis: ( a <= b implies Closed-Interval-TSpace (a,b) is connected )
assume A1: a <= b ; ::_thesis: Closed-Interval-TSpace (a,b) is connected
now__::_thesis:_Closed-Interval-TSpace_(a,b)_is_connected
percases ( a < b or a = b ) by A1, XXREAL_0:1;
suppose a < b ; ::_thesis: Closed-Interval-TSpace (a,b) is connected
then L[01] (((#) (a,b)),((a,b) (#))) is being_homeomorphism by Th17;
then A2: ( rng (L[01] (((#) (a,b)),((a,b) (#)))) = [#] (Closed-Interval-TSpace (a,b)) & L[01] (((#) (a,b)),((a,b) (#))) is continuous ) by TOPS_2:def_5;
set A = the carrier of (Closed-Interval-TSpace (0,1));
( the carrier of (Closed-Interval-TSpace (0,1)) = [#] (Closed-Interval-TSpace (0,1)) & (L[01] (((#) (a,b)),((a,b) (#)))) .: the carrier of (Closed-Interval-TSpace (0,1)) = rng (L[01] (((#) (a,b)),((a,b) (#)))) ) by RELSET_1:22;
hence Closed-Interval-TSpace (a,b) is connected by A2, Th19, CONNSP_1:14, TOPMETR:20; ::_thesis: verum
end;
supposeA3: a = b ; ::_thesis: Closed-Interval-TSpace (a,b) is connected
then ( [.a,b.] = {a} & a = (#) (a,b) ) by Def1, XXREAL_1:17;
then [#] (Closed-Interval-TSpace (a,b)) = {((#) (a,b))} by A3, TOPMETR:18;
hence Closed-Interval-TSpace (a,b) is connected by CONNSP_1:27; ::_thesis: verum
end;
end;
end;
hence Closed-Interval-TSpace (a,b) is connected ; ::_thesis: verum
end;
theorem Th21: :: TREAL_1:21
for f being continuous Function of I[01],I[01] ex x being Point of I[01] st f . x = x
proof
let f be continuous Function of I[01],I[01]; ::_thesis: ex x being Point of I[01] st f . x = x
reconsider F = f as Function of [.0,1.],[.0,1.] by BORSUK_1:40;
set A = { a where a is Real : ( a in [.0,1.] & F . a in [.0,a.] ) } ;
set B = { b where b is Real : ( b in [.0,1.] & F . b in [.b,1.] ) } ;
{ a where a is Real : ( a in [.0,1.] & F . a in [.0,a.] ) } c= REAL
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { a where a is Real : ( a in [.0,1.] & F . a in [.0,a.] ) } or x in REAL )
assume x in { a where a is Real : ( a in [.0,1.] & F . a in [.0,a.] ) } ; ::_thesis: x in REAL
then ex a being Real st
( a = x & a in [.0,1.] & F . a in [.0,a.] ) ;
hence x in REAL ; ::_thesis: verum
end;
then reconsider A = { a where a is Real : ( a in [.0,1.] & F . a in [.0,a.] ) } as Subset of REAL ;
A1: Closed-Interval-TSpace (0,1) = TopSpaceMetr (Closed-Interval-MSpace (0,1)) by TOPMETR:def_7;
A2: A c= [.0,1.]
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in A or x in [.0,1.] )
assume A3: x in A ; ::_thesis: x in [.0,1.]
then reconsider x = x as Real ;
ex a0 being Real st
( a0 = x & a0 in [.0,1.] & F . a0 in [.0,a0.] ) by A3;
hence x in [.0,1.] ; ::_thesis: verum
end;
{ b where b is Real : ( b in [.0,1.] & F . b in [.b,1.] ) } c= REAL
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { b where b is Real : ( b in [.0,1.] & F . b in [.b,1.] ) } or x in REAL )
assume x in { b where b is Real : ( b in [.0,1.] & F . b in [.b,1.] ) } ; ::_thesis: x in REAL
then ex b being Real st
( b = x & b in [.0,1.] & F . b in [.b,1.] ) ;
hence x in REAL ; ::_thesis: verum
end;
then reconsider B = { b where b is Real : ( b in [.0,1.] & F . b in [.b,1.] ) } as Subset of REAL ;
A4: the carrier of (Closed-Interval-MSpace (0,1)) = [.0,1.] by TOPMETR:10;
0 in { w where w is Real : ( 0 <= w & w <= 1 ) } ;
then A5: 0 in [.0,1.] by RCOMP_1:def_1;
A6: [.0,1.] <> {} by XXREAL_1:1;
then [.0,1.] = dom F by FUNCT_2:def_1;
then F . 0 in rng F by A5, FUNCT_1:def_3;
then A7: 0 in B by A5;
A8: [.0,1.] = { q where q is Real : ( 0 <= q & q <= 1 ) } by RCOMP_1:def_1;
A9: [.0,1.] c= A \/ B
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in [.0,1.] or x in A \/ B )
assume A10: x in [.0,1.] ; ::_thesis: x in A \/ B
then reconsider y = x as Real ;
ex p being Real st
( p = y & 0 <= p & p <= 1 ) by A8, A10;
then A11: [.0,1.] = [.0,y.] \/ [.y,1.] by XXREAL_1:174;
[.0,1.] = dom F by A6, FUNCT_2:def_1;
then A12: F . y in rng F by A10, FUNCT_1:def_3;
now__::_thesis:_y_in_A_\/_B
percases ( F . y in [.0,y.] or F . y in [.y,1.] ) by A11, A12, XBOOLE_0:def_3;
supposeA13: F . y in [.0,y.] ; ::_thesis: y in A \/ B
A14: A c= A \/ B by XBOOLE_1:7;
y in A by A10, A13;
hence y in A \/ B by A14; ::_thesis: verum
end;
supposeA15: F . y in [.y,1.] ; ::_thesis: y in A \/ B
A16: B c= A \/ B by XBOOLE_1:7;
y in B by A10, A15;
hence y in A \/ B by A16; ::_thesis: verum
end;
end;
end;
hence x in A \/ B ; ::_thesis: verum
end;
1 in { w where w is Real : ( 0 <= w & w <= 1 ) } ;
then A17: 1 in [.0,1.] by RCOMP_1:def_1;
A18: B c= [.0,1.]
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in B or x in [.0,1.] )
assume A19: x in B ; ::_thesis: x in [.0,1.]
then reconsider x = x as Real ;
ex b0 being Real st
( b0 = x & b0 in [.0,1.] & F . b0 in [.b0,1.] ) by A19;
hence x in [.0,1.] ; ::_thesis: verum
end;
assume A20: for x being Point of I[01] holds f . x <> x ; ::_thesis: contradiction
A21: A /\ B = {}
proof
set x = the Element of A /\ B;
assume A22: A /\ B <> {} ; ::_thesis: contradiction
then A23: the Element of A /\ B in A by XBOOLE_0:def_4;
then A24: ex z being Real st
( z = the Element of A /\ B & z in [.0,1.] & F . z in [.0,z.] ) ;
reconsider x = the Element of A /\ B as Real by A23;
x in B by A22, XBOOLE_0:def_4;
then ex b0 being Real st
( b0 = x & b0 in [.0,1.] & F . b0 in [.b0,1.] ) ;
then A25: F . x in [.0,x.] /\ [.x,1.] by A24, XBOOLE_0:def_4;
x in { q where q is Real : ( 0 <= q & q <= 1 ) } by A24, RCOMP_1:def_1;
then ex u being Real st
( u = x & 0 <= u & u <= 1 ) ;
then F . x in {x} by A25, XXREAL_1:418;
then F . x = x by TARSKI:def_1;
hence contradiction by A20, A24, BORSUK_1:40; ::_thesis: verum
end;
then A26: A misses B by XBOOLE_0:def_7;
[.0,1.] = dom F by A6, FUNCT_2:def_1;
then F . 1 in rng F by A17, FUNCT_1:def_3;
then A27: 1 in A by A17;
ex P, Q being Subset of I[01] st
( [#] I[01] = P \/ Q & P <> {} I[01] & Q <> {} I[01] & P is closed & Q is closed & P misses Q )
proof
reconsider P = A, Q = B as Subset of I[01] by A2, A18, BORSUK_1:40;
take P ; ::_thesis: ex Q being Subset of I[01] st
( [#] I[01] = P \/ Q & P <> {} I[01] & Q <> {} I[01] & P is closed & Q is closed & P misses Q )
take Q ; ::_thesis: ( [#] I[01] = P \/ Q & P <> {} I[01] & Q <> {} I[01] & P is closed & Q is closed & P misses Q )
thus A28: [#] I[01] = P \/ Q by A9, BORSUK_1:40, XBOOLE_0:def_10; ::_thesis: ( P <> {} I[01] & Q <> {} I[01] & P is closed & Q is closed & P misses Q )
thus ( P <> {} I[01] & Q <> {} I[01] ) by A27, A7; ::_thesis: ( P is closed & Q is closed & P misses Q )
thus P is closed ::_thesis: ( Q is closed & P misses Q )
proof
set z = the Element of (Cl P) /\ Q;
assume not P is closed ; ::_thesis: contradiction
then A29: Cl P <> P by PRE_TOPC:22;
A30: (Cl P) /\ Q <> {}
proof
assume (Cl P) /\ Q = {} ; ::_thesis: contradiction
then Cl P misses Q by XBOOLE_0:def_7;
then A31: Cl P c= Q ` by SUBSET_1:23;
( P c= Cl P & P = Q ` ) by A26, A28, PRE_TOPC:5, PRE_TOPC:18;
hence contradiction by A29, A31, XBOOLE_0:def_10; ::_thesis: verum
end;
then A32: the Element of (Cl P) /\ Q in Cl P by XBOOLE_0:def_4;
A33: the Element of (Cl P) /\ Q in Q by A30, XBOOLE_0:def_4;
reconsider z = the Element of (Cl P) /\ Q as Point of I[01] by A32;
reconsider t0 = z as Real by A33;
A34: ex c being Real st
( c = t0 & c in [.0,1.] & F . c in [.c,1.] ) by A33;
then reconsider s0 = F . t0 as Real ;
t0 <= s0 by A34, XXREAL_1:1;
then A35: 0 <= s0 - t0 by XREAL_1:48;
set r = (s0 - t0) * (2 ");
reconsider m = z, n = f . z as Point of (Closed-Interval-MSpace (0,1)) by BORSUK_1:40, TOPMETR:10;
reconsider W = Ball (n,((s0 - t0) * (2 "))) as Subset of I[01] by BORSUK_1:40, TOPMETR:10;
A36: ( W is open & f is_continuous_at z ) by A1, TMAP_1:50, TOPMETR:14, TOPMETR:20;
A37: s0 - t0 <> 0 by A20;
then A38: 0 / 2 < (s0 - t0) / 2 by A35, XREAL_1:74;
then f . z in W by TBSP_1:11;
then consider V being Subset of I[01] such that
A39: ( V is open & z in V ) and
A40: f .: V c= W by A36, TMAP_1:43;
consider s being real number such that
A41: s > 0 and
A42: Ball (m,s) c= V by A1, A39, TOPMETR:15, TOPMETR:20;
reconsider s = s as Real by XREAL_0:def_1;
set r0 = min (s,((s0 - t0) * (2 ")));
reconsider W0 = Ball (m,(min (s,((s0 - t0) * (2 "))))) as Subset of I[01] by BORSUK_1:40, TOPMETR:10;
min (s,((s0 - t0) * (2 "))) > 0 by A38, A41, XXREAL_0:15;
then A43: z in W0 by TBSP_1:11;
set w = the Element of P /\ W0;
W0 is open by A1, TOPMETR:14, TOPMETR:20;
then P meets W0 by A32, A43, PRE_TOPC:24;
then A44: P /\ W0 <> {} I[01] by XBOOLE_0:def_7;
then A45: the Element of P /\ W0 in P by XBOOLE_0:def_4;
A46: the Element of P /\ W0 in W0 by A44, XBOOLE_0:def_4;
then reconsider w = the Element of P /\ W0 as Point of (Closed-Interval-MSpace (0,1)) ;
reconsider w1 = w as Point of I[01] by A45;
reconsider d = w1 as Real by A45;
A47: d in A by A44, XBOOLE_0:def_4;
Ball (m,(min (s,((s0 - t0) * (2 "))))) = { q where q is Element of (Closed-Interval-MSpace (0,1)) : dist (m,q) < min (s,((s0 - t0) * (2 "))) } by METRIC_1:17;
then ( min (s,((s0 - t0) * (2 "))) <= (s0 - t0) * (2 ") & ex p being Element of (Closed-Interval-MSpace (0,1)) st
( p = w & dist (m,p) < min (s,((s0 - t0) * (2 "))) ) ) by A46, XXREAL_0:17;
then dist (w,m) < (s0 - t0) * (2 ") by XXREAL_0:2;
then A48: abs (d - t0) < (s0 - t0) * (2 ") by HEINE:1;
d - t0 <= abs (d - t0) by ABSVALUE:4;
then ( t0 + ((s0 - t0) * (2 ")) = s0 - ((s0 - t0) * (2 ")) & d - t0 < (s0 - t0) * (2 ") ) by A48, XXREAL_0:2;
then A49: d < s0 - ((s0 - t0) * (2 ")) by XREAL_1:19;
A50: (s0 - t0) * (2 ") < (s0 - t0) * 1 by A35, A37, XREAL_1:68;
A51: Ball (n,((s0 - t0) * (2 "))) c= [.t0,1.]
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Ball (n,((s0 - t0) * (2 "))) or x in [.t0,1.] )
assume A52: x in Ball (n,((s0 - t0) * (2 "))) ; ::_thesis: x in [.t0,1.]
then reconsider u = x as Point of (Closed-Interval-MSpace (0,1)) ;
x in [.0,1.] by A4, A52;
then reconsider t = x as Real ;
Ball (n,((s0 - t0) * (2 "))) = { q where q is Element of (Closed-Interval-MSpace (0,1)) : dist (n,q) < (s0 - t0) * (2 ") } by METRIC_1:17;
then ex p being Element of (Closed-Interval-MSpace (0,1)) st
( p = u & dist (n,p) < (s0 - t0) * (2 ") ) by A52;
then abs (s0 - t) < (s0 - t0) * (2 ") by HEINE:1;
then A53: abs (s0 - t) < s0 - t0 by A50, XXREAL_0:2;
s0 - t <= abs (s0 - t) by ABSVALUE:4;
then s0 - t < s0 - t0 by A53, XXREAL_0:2;
then A54: t0 <= t by XREAL_1:10;
t <= 1 by A4, A52, XXREAL_1:1;
then t in { q where q is Real : ( t0 <= q & q <= 1 ) } by A54;
hence x in [.t0,1.] by RCOMP_1:def_1; ::_thesis: verum
end;
A55: Ball (n,((s0 - t0) * (2 "))) c= [.d,1.]
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Ball (n,((s0 - t0) * (2 "))) or x in [.d,1.] )
assume A56: x in Ball (n,((s0 - t0) * (2 "))) ; ::_thesis: x in [.d,1.]
then reconsider v = x as Point of (Closed-Interval-MSpace (0,1)) ;
x in [.0,1.] by A4, A56;
then reconsider t = x as Real ;
Ball (n,((s0 - t0) * (2 "))) = { q where q is Element of (Closed-Interval-MSpace (0,1)) : dist (n,q) < (s0 - t0) * (2 ") } by METRIC_1:17;
then ex p being Element of (Closed-Interval-MSpace (0,1)) st
( p = v & dist (n,p) < (s0 - t0) * (2 ") ) by A56;
then A57: abs (s0 - t) < (s0 - t0) * (2 ") by HEINE:1;
A58: now__::_thesis:_d_<_t
percases ( t <= s0 or s0 < t ) ;
suppose t <= s0 ; ::_thesis: d < t
then 0 <= s0 - t by XREAL_1:48;
then s0 - t < (s0 - t0) * (2 ") by A57, ABSVALUE:def_1;
then s0 < ((s0 - t0) * (2 ")) + t by XREAL_1:19;
then s0 - ((s0 - t0) * (2 ")) < t by XREAL_1:19;
hence d < t by A49, XXREAL_0:2; ::_thesis: verum
end;
supposeA59: s0 < t ; ::_thesis: d < t
s0 - ((s0 - t0) * (2 ")) < s0 by A38, XREAL_1:44;
then d < s0 by A49, XXREAL_0:2;
hence d < t by A59, XXREAL_0:2; ::_thesis: verum
end;
end;
end;
t <= 1 by A51, A56, XXREAL_1:1;
then t in { w0 where w0 is Real : ( d <= w0 & w0 <= 1 ) } by A58;
hence x in [.d,1.] by RCOMP_1:def_1; ::_thesis: verum
end;
Ball (m,(min (s,((s0 - t0) * (2 "))))) c= Ball (m,s) by PCOMPS_1:1, XXREAL_0:17;
then W0 c= V by A42, XBOOLE_1:1;
then f . w1 in f .: V by A46, FUNCT_2:35;
then f . w1 in W by A40;
then d in B by A55, BORSUK_1:40;
hence contradiction by A26, A47, XBOOLE_0:3; ::_thesis: verum
end;
thus Q is closed ::_thesis: P misses Q
proof
set z = the Element of (Cl Q) /\ P;
assume not Q is closed ; ::_thesis: contradiction
then A60: Cl Q <> Q by PRE_TOPC:22;
A61: (Cl Q) /\ P <> {}
proof
assume (Cl Q) /\ P = {} ; ::_thesis: contradiction
then Cl Q misses P by XBOOLE_0:def_7;
then A62: Cl Q c= P ` by SUBSET_1:23;
( Q c= Cl Q & Q = P ` ) by A26, A28, PRE_TOPC:5, PRE_TOPC:18;
hence contradiction by A60, A62, XBOOLE_0:def_10; ::_thesis: verum
end;
then A63: the Element of (Cl Q) /\ P in Cl Q by XBOOLE_0:def_4;
A64: the Element of (Cl Q) /\ P in P by A61, XBOOLE_0:def_4;
reconsider z = the Element of (Cl Q) /\ P as Point of I[01] by A63;
reconsider t0 = z as Real by A64;
A65: ex c being Real st
( c = t0 & c in [.0,1.] & F . c in [.0,c.] ) by A64;
then reconsider s0 = F . t0 as Real ;
s0 <= t0 by A65, XXREAL_1:1;
then A66: 0 <= t0 - s0 by XREAL_1:48;
set r = (t0 - s0) * (2 ");
reconsider m = z, n = f . z as Point of (Closed-Interval-MSpace (0,1)) by BORSUK_1:40, TOPMETR:10;
reconsider W = Ball (n,((t0 - s0) * (2 "))) as Subset of I[01] by BORSUK_1:40, TOPMETR:10;
A67: ( W is open & f is_continuous_at z ) by A1, TMAP_1:50, TOPMETR:14, TOPMETR:20;
A68: t0 - s0 <> 0 by A20;
then A69: 0 / 2 < (t0 - s0) / 2 by A66, XREAL_1:74;
then f . z in W by TBSP_1:11;
then consider V being Subset of I[01] such that
A70: ( V is open & z in V ) and
A71: f .: V c= W by A67, TMAP_1:43;
consider s being real number such that
A72: s > 0 and
A73: Ball (m,s) c= V by A1, A70, TOPMETR:15, TOPMETR:20;
reconsider s = s as Real by XREAL_0:def_1;
set r0 = min (s,((t0 - s0) * (2 ")));
reconsider W0 = Ball (m,(min (s,((t0 - s0) * (2 "))))) as Subset of I[01] by BORSUK_1:40, TOPMETR:10;
min (s,((t0 - s0) * (2 "))) > 0 by A69, A72, XXREAL_0:15;
then A74: z in W0 by TBSP_1:11;
set w = the Element of Q /\ W0;
W0 is open by A1, TOPMETR:14, TOPMETR:20;
then Q meets W0 by A63, A74, PRE_TOPC:24;
then A75: Q /\ W0 <> {} I[01] by XBOOLE_0:def_7;
then A76: the Element of Q /\ W0 in Q by XBOOLE_0:def_4;
A77: the Element of Q /\ W0 in W0 by A75, XBOOLE_0:def_4;
then reconsider w = the Element of Q /\ W0 as Point of (Closed-Interval-MSpace (0,1)) ;
reconsider w1 = w as Point of I[01] by A76;
reconsider d = w1 as Real by A76;
A78: d in B by A75, XBOOLE_0:def_4;
Ball (m,(min (s,((t0 - s0) * (2 "))))) = { q where q is Element of (Closed-Interval-MSpace (0,1)) : dist (m,q) < min (s,((t0 - s0) * (2 "))) } by METRIC_1:17;
then ( min (s,((t0 - s0) * (2 "))) <= (t0 - s0) * (2 ") & ex p being Element of (Closed-Interval-MSpace (0,1)) st
( p = w & dist (m,p) < min (s,((t0 - s0) * (2 "))) ) ) by A77, XXREAL_0:17;
then dist (m,w) < (t0 - s0) * (2 ") by XXREAL_0:2;
then A79: abs (t0 - d) < (t0 - s0) * (2 ") by HEINE:1;
t0 - d <= abs (t0 - d) by ABSVALUE:4;
then t0 + (- d) < (t0 - s0) * (2 ") by A79, XXREAL_0:2;
then t0 < ((t0 - s0) * (2 ")) - (- d) by XREAL_1:20;
then ( s0 + ((t0 - s0) * (2 ")) = t0 - ((t0 - s0) * (2 ")) & t0 < ((t0 - s0) * (2 ")) + (- (- d)) ) ;
then A80: s0 + ((t0 - s0) * (2 ")) < d by XREAL_1:19;
A81: (t0 - s0) * (2 ") < (t0 - s0) * 1 by A66, A68, XREAL_1:68;
A82: Ball (n,((t0 - s0) * (2 "))) c= [.0,t0.]
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Ball (n,((t0 - s0) * (2 "))) or x in [.0,t0.] )
assume A83: x in Ball (n,((t0 - s0) * (2 "))) ; ::_thesis: x in [.0,t0.]
then reconsider u = x as Point of (Closed-Interval-MSpace (0,1)) ;
x in [.0,1.] by A4, A83;
then reconsider t = x as Real ;
Ball (n,((t0 - s0) * (2 "))) = { q where q is Element of (Closed-Interval-MSpace (0,1)) : dist (n,q) < (t0 - s0) * (2 ") } by METRIC_1:17;
then ex p being Element of (Closed-Interval-MSpace (0,1)) st
( p = u & dist (n,p) < (t0 - s0) * (2 ") ) by A83;
then abs (t - s0) < (t0 - s0) * (2 ") by HEINE:1;
then A84: abs (t - s0) < t0 - s0 by A81, XXREAL_0:2;
t - s0 <= abs (t - s0) by ABSVALUE:4;
then t - s0 < t0 - s0 by A84, XXREAL_0:2;
then A85: t <= t0 by XREAL_1:9;
0 <= t by A4, A83, XXREAL_1:1;
then t in { q where q is Real : ( 0 <= q & q <= t0 ) } by A85;
hence x in [.0,t0.] by RCOMP_1:def_1; ::_thesis: verum
end;
A86: Ball (n,((t0 - s0) * (2 "))) c= [.0,d.]
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Ball (n,((t0 - s0) * (2 "))) or x in [.0,d.] )
assume A87: x in Ball (n,((t0 - s0) * (2 "))) ; ::_thesis: x in [.0,d.]
then reconsider v = x as Point of (Closed-Interval-MSpace (0,1)) ;
x in [.0,1.] by A4, A87;
then reconsider t = x as Real ;
Ball (n,((t0 - s0) * (2 "))) = { q where q is Element of (Closed-Interval-MSpace (0,1)) : dist (n,q) < (t0 - s0) * (2 ") } by METRIC_1:17;
then ex p being Element of (Closed-Interval-MSpace (0,1)) st
( p = v & dist (n,p) < (t0 - s0) * (2 ") ) by A87;
then A88: abs (t - s0) < (t0 - s0) * (2 ") by HEINE:1;
A89: now__::_thesis:_t_<_d
percases ( s0 <= t or t < s0 ) ;
suppose s0 <= t ; ::_thesis: t < d
then 0 <= t - s0 by XREAL_1:48;
then t - s0 < (t0 - s0) * (2 ") by A88, ABSVALUE:def_1;
then t < s0 + ((t0 - s0) * (2 ")) by XREAL_1:19;
hence t < d by A80, XXREAL_0:2; ::_thesis: verum
end;
supposeA90: t < s0 ; ::_thesis: t < d
s0 < s0 + ((t0 - s0) * (2 ")) by A69, XREAL_1:29;
then s0 < d by A80, XXREAL_0:2;
hence t < d by A90, XXREAL_0:2; ::_thesis: verum
end;
end;
end;
0 <= t by A82, A87, XXREAL_1:1;
then t in { w0 where w0 is Real : ( 0 <= w0 & w0 <= d ) } by A89;
hence x in [.0,d.] by RCOMP_1:def_1; ::_thesis: verum
end;
Ball (m,(min (s,((t0 - s0) * (2 "))))) c= Ball (m,s) by PCOMPS_1:1, XXREAL_0:17;
then W0 c= V by A73, XBOOLE_1:1;
then f . w1 in f .: V by A77, FUNCT_2:35;
then f . w1 in W by A71;
then d in A by A86, BORSUK_1:40;
hence contradiction by A26, A78, XBOOLE_0:3; ::_thesis: verum
end;
thus P misses Q by A21, XBOOLE_0:def_7; ::_thesis: verum
end;
hence contradiction by Th19, CONNSP_1:10; ::_thesis: verum
end;
theorem Th22: :: TREAL_1:22
for a, b being real number st a <= b holds
for f being continuous Function of (Closed-Interval-TSpace (a,b)),(Closed-Interval-TSpace (a,b)) ex x being Point of (Closed-Interval-TSpace (a,b)) st f . x = x
proof
let a, b be real number ; ::_thesis: ( a <= b implies for f being continuous Function of (Closed-Interval-TSpace (a,b)),(Closed-Interval-TSpace (a,b)) ex x being Point of (Closed-Interval-TSpace (a,b)) st f . x = x )
assume A1: a <= b ; ::_thesis: for f being continuous Function of (Closed-Interval-TSpace (a,b)),(Closed-Interval-TSpace (a,b)) ex x being Point of (Closed-Interval-TSpace (a,b)) st f . x = x
let f be continuous Function of (Closed-Interval-TSpace (a,b)),(Closed-Interval-TSpace (a,b)); ::_thesis: ex x being Point of (Closed-Interval-TSpace (a,b)) st f . x = x
now__::_thesis:_ex_x_being_Point_of_(Closed-Interval-TSpace_(a,b))_st_f_._x_=_x
percases ( a < b or a = b ) by A1, XXREAL_0:1;
supposeA2: a < b ; ::_thesis: ex x being Point of (Closed-Interval-TSpace (a,b)) st f . x = x
set L = L[01] (((#) (a,b)),((a,b) (#)));
set P = P[01] (a,b,((#) (0,1)),((0,1) (#)));
A3: P[01] (a,b,((#) (0,1)),((0,1) (#))) is continuous Function of (Closed-Interval-TSpace (a,b)),(Closed-Interval-TSpace (0,1)) by A2, Th12;
set g = ((P[01] (a,b,((#) (0,1)),((0,1) (#)))) * f) * (L[01] (((#) (a,b)),((a,b) (#))));
A4: id (Closed-Interval-TSpace (a,b)) = (L[01] (((#) (a,b)),((a,b) (#)))) * (P[01] (a,b,((#) (0,1)),((0,1) (#)))) by A2, Th15;
then A5: f = ((L[01] (((#) (a,b)),((a,b) (#)))) * (P[01] (a,b,((#) (0,1)),((0,1) (#))))) * f by FUNCT_2:17
.= (L[01] (((#) (a,b)),((a,b) (#)))) * ((P[01] (a,b,((#) (0,1)),((0,1) (#)))) * f) by RELAT_1:36
.= (L[01] (((#) (a,b)),((a,b) (#)))) * (((P[01] (a,b,((#) (0,1)),((0,1) (#)))) * f) * ((L[01] (((#) (a,b)),((a,b) (#)))) * (P[01] (a,b,((#) (0,1)),((0,1) (#)))))) by A4, FUNCT_2:17
.= (L[01] (((#) (a,b)),((a,b) (#)))) * ((((P[01] (a,b,((#) (0,1)),((0,1) (#)))) * f) * (L[01] (((#) (a,b)),((a,b) (#))))) * (P[01] (a,b,((#) (0,1)),((0,1) (#))))) by RELAT_1:36
.= ((L[01] (((#) (a,b)),((a,b) (#)))) * (((P[01] (a,b,((#) (0,1)),((0,1) (#)))) * f) * (L[01] (((#) (a,b)),((a,b) (#)))))) * (P[01] (a,b,((#) (0,1)),((0,1) (#)))) by RELAT_1:36 ;
L[01] (((#) (a,b)),((a,b) (#))) is continuous Function of (Closed-Interval-TSpace (0,1)),(Closed-Interval-TSpace (a,b)) by A1, Th8;
then consider y being Point of (Closed-Interval-TSpace (0,1)) such that
A6: (((P[01] (a,b,((#) (0,1)),((0,1) (#)))) * f) * (L[01] (((#) (a,b)),((a,b) (#))))) . y = y by A3, Th21, TOPMETR:20;
A7: id (Closed-Interval-TSpace (0,1)) = (P[01] (a,b,((#) (0,1)),((0,1) (#)))) * (L[01] (((#) (a,b)),((a,b) (#)))) by A2, Th15;
now__::_thesis:_ex_x_being_Element_of_the_carrier_of_(Closed-Interval-TSpace_(a,b))_st_f_._x_=_x
take x = (L[01] (((#) (a,b)),((a,b) (#)))) . y; ::_thesis: f . x = x
thus f . x = ((((L[01] (((#) (a,b)),((a,b) (#)))) * (((P[01] (a,b,((#) (0,1)),((0,1) (#)))) * f) * (L[01] (((#) (a,b)),((a,b) (#)))))) * (P[01] (a,b,((#) (0,1)),((0,1) (#))))) * (L[01] (((#) (a,b)),((a,b) (#))))) . y by A5, FUNCT_2:15
.= (((L[01] (((#) (a,b)),((a,b) (#)))) * (((P[01] (a,b,((#) (0,1)),((0,1) (#)))) * f) * (L[01] (((#) (a,b)),((a,b) (#)))))) * (id (Closed-Interval-TSpace (0,1)))) . y by A7, RELAT_1:36
.= ((L[01] (((#) (a,b)),((a,b) (#)))) * (((P[01] (a,b,((#) (0,1)),((0,1) (#)))) * f) * (L[01] (((#) (a,b)),((a,b) (#)))))) . y by FUNCT_2:17
.= x by A6, FUNCT_2:15 ; ::_thesis: verum
end;
hence ex x being Point of (Closed-Interval-TSpace (a,b)) st f . x = x ; ::_thesis: verum
end;
supposeA8: a = b ; ::_thesis: ex x being Point of (Closed-Interval-TSpace (a,b)) st f . x = x
then ( [.a,b.] = {a} & a = (#) (a,b) ) by Def1, XXREAL_1:17;
then A9: the carrier of (Closed-Interval-TSpace (a,b)) = {((#) (a,b))} by A8, TOPMETR:18;
now__::_thesis:_ex_x_being_Point_of_(Closed-Interval-TSpace_(a,b))_st_f_._x_=_x
take x = (#) (a,b); ::_thesis: f . x = x
thus f . x = x by A9, TARSKI:def_1; ::_thesis: verum
end;
hence ex x being Point of (Closed-Interval-TSpace (a,b)) st f . x = x ; ::_thesis: verum
end;
end;
end;
hence ex x being Point of (Closed-Interval-TSpace (a,b)) st f . x = x ; ::_thesis: verum
end;
theorem Th23: :: TREAL_1:23
for X, Y being non empty SubSpace of R^1
for f being continuous Function of X,Y st ex a, b being Real st
( a <= b & [.a,b.] c= the carrier of X & [.a,b.] c= the carrier of Y & f .: [.a,b.] c= [.a,b.] ) holds
ex x being Point of X st f . x = x
proof
let X, Y be non empty SubSpace of R^1 ; ::_thesis: for f being continuous Function of X,Y st ex a, b being Real st
( a <= b & [.a,b.] c= the carrier of X & [.a,b.] c= the carrier of Y & f .: [.a,b.] c= [.a,b.] ) holds
ex x being Point of X st f . x = x
let f be continuous Function of X,Y; ::_thesis: ( ex a, b being Real st
( a <= b & [.a,b.] c= the carrier of X & [.a,b.] c= the carrier of Y & f .: [.a,b.] c= [.a,b.] ) implies ex x being Point of X st f . x = x )
given a, b being Real such that A1: a <= b and
A2: [.a,b.] c= the carrier of X and
A3: [.a,b.] c= the carrier of Y and
A4: f .: [.a,b.] c= [.a,b.] ; ::_thesis: ex x being Point of X st f . x = x
reconsider A = [.a,b.] as non empty Subset of X by A1, A2, XXREAL_1:1;
A5: dom (f | A) = (dom f) /\ A by RELAT_1:61;
( A = the carrier of X /\ A & dom f = the carrier of X ) by FUNCT_2:def_1, XBOOLE_1:28;
then A6: dom (f | A) = the carrier of (Closed-Interval-TSpace (a,b)) by A1, A5, TOPMETR:18;
A7: A = the carrier of (Closed-Interval-TSpace (a,b)) by A1, TOPMETR:18;
then reconsider Z = Closed-Interval-TSpace (a,b) as SubSpace of X by TSEP_1:4;
rng (f | A) c= the carrier of (Closed-Interval-TSpace (a,b)) by A4, A7, RELAT_1:115;
then reconsider g = f | A as Function of (Closed-Interval-TSpace (a,b)),(Closed-Interval-TSpace (a,b)) by A6, FUNCT_2:def_1, RELSET_1:4;
A8: Z is SubSpace of Y by A3, A7, TSEP_1:4;
for s being Point of (Closed-Interval-TSpace (a,b)) holds g is_continuous_at s
proof
let s be Point of (Closed-Interval-TSpace (a,b)); ::_thesis: g is_continuous_at s
reconsider w = s as Point of X by A7, TARSKI:def_3;
for G being Subset of (Closed-Interval-TSpace (a,b)) st G is open & g . s in G holds
ex H being Subset of Z st
( H is open & s in H & g .: H c= G )
proof
let G be Subset of (Closed-Interval-TSpace (a,b)); ::_thesis: ( G is open & g . s in G implies ex H being Subset of Z st
( H is open & s in H & g .: H c= G ) )
A9: f is_continuous_at w by TMAP_1:44;
assume G is open ; ::_thesis: ( not g . s in G or ex H being Subset of Z st
( H is open & s in H & g .: H c= G ) )
then consider G0 being Subset of Y such that
A10: G0 is open and
A11: G0 /\ ([#] (Closed-Interval-TSpace (a,b))) = G by A8, TOPS_2:24;
assume g . s in G ; ::_thesis: ex H being Subset of Z st
( H is open & s in H & g .: H c= G )
then f . w in G by A7, FUNCT_1:49;
then f . w in G0 by A11, XBOOLE_0:def_4;
then consider H0 being Subset of X such that
A12: H0 is open and
A13: w in H0 and
A14: f .: H0 c= G0 by A10, A9, TMAP_1:43;
now__::_thesis:_ex_H_being_Subset_of_Z_st_
(_H_is_open_&_s_in_H_&_g_.:_H_c=_G_)
reconsider H = H0 /\ ([#] (Closed-Interval-TSpace (a,b))) as Subset of Z ;
take H = H; ::_thesis: ( H is open & s in H & g .: H c= G )
thus H is open by A12, TOPS_2:24; ::_thesis: ( s in H & g .: H c= G )
thus s in H by A13, XBOOLE_0:def_4; ::_thesis: g .: H c= G
thus g .: H c= G ::_thesis: verum
proof
let t be set ; :: according to TARSKI:def_3 ::_thesis: ( not t in g .: H or t in G )
assume t in g .: H ; ::_thesis: t in G
then consider r being set such that
r in dom g and
A15: r in H and
A16: t = g . r by FUNCT_1:def_6;
A17: r in the carrier of Z by A15;
reconsider r = r as Point of (Closed-Interval-TSpace (a,b)) by A15;
r in dom g by A17, FUNCT_2:def_1;
then A18: t in g .: the carrier of Z by A16, FUNCT_1:def_6;
reconsider p = r as Point of X by A7, TARSKI:def_3;
p in [#] X ;
then A19: p in dom f by FUNCT_2:def_1;
( t = f . p & p in H0 ) by A7, A15, A16, FUNCT_1:49, XBOOLE_0:def_4;
then t in f .: H0 by A19, FUNCT_1:def_6;
hence t in G by A11, A14, A18, XBOOLE_0:def_4; ::_thesis: verum
end;
end;
hence ex H being Subset of Z st
( H is open & s in H & g .: H c= G ) ; ::_thesis: verum
end;
hence g is_continuous_at s by TMAP_1:43; ::_thesis: verum
end;
then reconsider h = g as continuous Function of (Closed-Interval-TSpace (a,b)),(Closed-Interval-TSpace (a,b)) by TMAP_1:44;
now__::_thesis:_ex_x_being_Point_of_X_st_f_._x_=_x
consider y being Point of (Closed-Interval-TSpace (a,b)) such that
A20: h . y = y by A1, Th22;
reconsider x = y as Point of X by A7, TARSKI:def_3;
take x = x; ::_thesis: f . x = x
thus f . x = x by A7, A20, FUNCT_1:49; ::_thesis: verum
end;
hence ex x being Point of X st f . x = x ; ::_thesis: verum
end;
theorem :: TREAL_1:24
for X, Y being non empty SubSpace of R^1
for f being continuous Function of X,Y st ex a, b being Real st
( a <= b & [.a,b.] c= the carrier of X & f .: [.a,b.] c= [.a,b.] ) holds
ex x being Point of X st f . x = x
proof
let X, Y be non empty SubSpace of R^1 ; ::_thesis: for f being continuous Function of X,Y st ex a, b being Real st
( a <= b & [.a,b.] c= the carrier of X & f .: [.a,b.] c= [.a,b.] ) holds
ex x being Point of X st f . x = x
let f be continuous Function of X,Y; ::_thesis: ( ex a, b being Real st
( a <= b & [.a,b.] c= the carrier of X & f .: [.a,b.] c= [.a,b.] ) implies ex x being Point of X st f . x = x )
given a, b being Real such that A1: a <= b and
A2: [.a,b.] c= the carrier of X and
A3: f .: [.a,b.] c= [.a,b.] ; ::_thesis: ex x being Point of X st f . x = x
set g = (Y incl R^1) * f;
the carrier of Y c= the carrier of R^1 by BORSUK_1:1;
then reconsider B = f .: [.a,b.] as Subset of R^1 by XBOOLE_1:1;
((Y incl R^1) * f) .: [.a,b.] = (Y incl R^1) .: (f .: [.a,b.]) by RELAT_1:126;
then ((Y incl R^1) * f) .: [.a,b.] = ((id R^1) | Y) .: B by TMAP_1:def_6;
then ((Y incl R^1) * f) .: [.a,b.] = (id R^1) .: B by TMAP_1:55;
then A4: ((Y incl R^1) * f) .: [.a,b.] c= [.a,b.] by A3, FUNCT_1:92;
A5: ( Y incl R^1 is continuous Function of Y,R^1 & R^1 is SubSpace of R^1 ) by TMAP_1:87, TSEP_1:2;
the carrier of X c= the carrier of R^1 by BORSUK_1:1;
then A6: [.a,b.] c= the carrier of R^1 by A2, XBOOLE_1:1;
now__::_thesis:_ex_x_being_Point_of_X_st_f_._x_=_x
consider x being Point of X such that
A7: ((Y incl R^1) * f) . x = x by A1, A2, A5, A6, A4, Th23;
the carrier of Y c= the carrier of R^1 by BORSUK_1:1;
then reconsider y = f . x as Point of R^1 by TARSKI:def_3;
take x = x; ::_thesis: f . x = x
thus f . x = (Y incl R^1) . y by TMAP_1:84
.= x by A7, FUNCT_2:15 ; ::_thesis: verum
end;
hence ex x being Point of X st f . x = x ; ::_thesis: verum
end;