:: by Toshihiko Watanabe

::

:: Received August 17, 1992

:: Copyright (c) 1992-2021 Association of Mizar Users

Lm1: for a, b being Real

for x being set st x in [.a,b.] holds

x is Element of REAL

;

Lm2: for a, b being Real

for x being Point of (Closed-Interval-TSpace (a,b)) st a <= b holds

x is Element of REAL

proof end;

theorem :: TREAL_1:3

for a, b, c, d being Real st a <= c & d <= b & c <= d holds

Closed-Interval-TSpace (c,d) is closed SubSpace of Closed-Interval-TSpace (a,b)

Closed-Interval-TSpace (c,d) is closed SubSpace of Closed-Interval-TSpace (a,b)

proof end;

theorem :: TREAL_1:4

for a, b, c, d being Real 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)) )

( 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 end;

definition

let a, b be Real;

assume A1: a <= b ;

coherence

a is Point of (Closed-Interval-TSpace (a,b))

;

coherence

b is Point of (Closed-Interval-TSpace (a,b))

;

end;
assume A1: a <= b ;

coherence

a is Point of (Closed-Interval-TSpace (a,b))

proof end;

correctness ;

coherence

b is Point of (Closed-Interval-TSpace (a,b))

proof end;

correctness ;

theorem :: TREAL_1:5

:: 2. Continuous Mappings Between Topological Intervals.

definition

let a, b be Real;

assume A1: a <= b ;

let t1, t2 be Point of (Closed-Interval-TSpace (a,b));

ex b_{1} 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 b_{1} . s = ((1 - s) * t1) + (s * t2)

for b_{1}, b_{2} 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 b_{1} . s = ((1 - s) * t1) + (s * t2) ) & ( for s being Point of (Closed-Interval-TSpace (0,1)) holds b_{2} . s = ((1 - s) * t1) + (s * t2) ) holds

b_{1} = b_{2}

end;
assume A1: 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 for s being Point of (Closed-Interval-TSpace (0,1)) holds it . s = ((1 - s) * t1) + (s * t2);

ex b

for s being Point of (Closed-Interval-TSpace (0,1)) holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def3 defines L[01] TREAL_1:def 3 :

for a, b being Real st a <= b holds

for t1, t2 being Point of (Closed-Interval-TSpace (a,b))

for b_{5} being Function of (Closed-Interval-TSpace (0,1)),(Closed-Interval-TSpace (a,b)) holds

( b_{5} = L[01] (t1,t2) iff for s being Point of (Closed-Interval-TSpace (0,1)) holds b_{5} . s = ((1 - s) * t1) + (s * t2) );

for a, b being Real st a <= b holds

for t1, t2 being Point of (Closed-Interval-TSpace (a,b))

for b

( b

theorem Th7: :: TREAL_1:7

for a, b being Real 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

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 end;

theorem Th8: :: TREAL_1:8

for a, b being Real st a <= b holds

for t1, t2 being Point of (Closed-Interval-TSpace (a,b)) holds L[01] (t1,t2) is continuous

for t1, t2 being Point of (Closed-Interval-TSpace (a,b)) holds L[01] (t1,t2) is continuous

proof end;

theorem :: TREAL_1:9

for a, b being Real 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 )

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 end;

definition

let a, b be Real;

assume A1: a < b ;

let t1, t2 be Point of (Closed-Interval-TSpace (0,1));

ex b_{1} 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 b_{1} . s = (((b - s) * t1) + ((s - a) * t2)) / (b - a)

for b_{1}, b_{2} 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 b_{1} . s = (((b - s) * t1) + ((s - a) * t2)) / (b - a) ) & ( for s being Point of (Closed-Interval-TSpace (a,b)) holds b_{2} . s = (((b - s) * t1) + ((s - a) * t2)) / (b - a) ) holds

b_{1} = b_{2}

end;
assume A1: 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 for s being Point of (Closed-Interval-TSpace (a,b)) holds it . s = (((b - s) * t1) + ((s - a) * t2)) / (b - a);

ex b

for s being Point of (Closed-Interval-TSpace (a,b)) holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def4 defines P[01] TREAL_1:def 4 :

for a, b being Real st a < b holds

for t1, t2 being Point of (Closed-Interval-TSpace (0,1))

for b_{5} being Function of (Closed-Interval-TSpace (a,b)),(Closed-Interval-TSpace (0,1)) holds

( b_{5} = P[01] (a,b,t1,t2) iff for s being Point of (Closed-Interval-TSpace (a,b)) holds b_{5} . s = (((b - s) * t1) + ((s - a) * t2)) / (b - a) );

for a, b being Real st a < b holds

for t1, t2 being Point of (Closed-Interval-TSpace (0,1))

for b

( b

theorem Th11: :: TREAL_1:11

for a, b being Real 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))

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 end;

theorem Th12: :: TREAL_1:12

for a, b being Real st a < b holds

for t1, t2 being Point of (Closed-Interval-TSpace (0,1)) holds P[01] (a,b,t1,t2) is continuous

for t1, t2 being Point of (Closed-Interval-TSpace (0,1)) holds P[01] (a,b,t1,t2) is continuous

proof end;

theorem :: TREAL_1:13

for a, b being Real 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 )

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 end;

theorem Th15: :: TREAL_1:15

for a, b being Real 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) (#)))) )

( 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 end;

theorem Th16: :: TREAL_1:16

for a, b being Real 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)))) )

( 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 end;

theorem Th17: :: TREAL_1:17

for a, b being Real 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) (#))) )

( 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 end;

theorem :: TREAL_1:18

for a, b being Real 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))) )

( 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 end;

:: 3. Connectedness of Intervals and Brouwer Fixed Point Theorem for Intervals.

theorem Th22: :: TREAL_1:22

for a, b being Real 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

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 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

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 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

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 end;