:: TREAL_1 semantic presentation

theorem Th1: :: TREAL_1:1

for b₁, b₂, b₃, b₄ being real number st b₁ <= b₂ & b₃ <= b₄ holds
[.b₂,b₃.] c= [.b₁,b₄.]

proof end;

theorem Th2: :: TREAL_1:2

for b₁, b₂, b₃, b₄ being real number st b₁ <= b₂ & b₃ <= b₄ & b₂ <= b₃ holds
[.b₁,b₃.] \/ [.b₂,b₄.] = [.b₁,b₄.]

proof end;

theorem Th3: :: TREAL_1:3

for b₁, b₂, b₃, b₄ being real number st b₁ <= b₂ & b₃ <= b₄ & b₂ <= b₃ holds
[.b₁,b₃.] /\ [.b₂,b₄.] = [.b₂,b₃.]

proof end;

Lemma4: for b₁, b₂ being real number
for b₃ being set st b₃ in [.b₁,b₂.] holds
b₃ is Real
;

Lemma5: for b₁, b₂, b₃ being real number
for b₄ being set st b₄ in [.b₁,b₂.] & b₁ <= b₂ & b₃ = b₄ holds
( b₁ <= b₃ & b₃ <= b₂ )

proof end;

Lemma6: for b₁, b₂ being real number
for b₃ being Point of (Closed-Interval-TSpace b₁,b₂) st b₁ <= b₂ holds
b₃ is Real

proof end;

theorem Th4: :: TREAL_1:4

for b₁, b₂ being real number
for b₃ being Subset of R^1 st b₃ = [.b₁,b₂.] holds
b₃ is closed

proof end;

theorem Th5: :: TREAL_1:5

for b₁, b₂ being real number st b₁ <= b₂ holds
Closed-Interval-TSpace b₁,b₂ is closed SubSpace of R^1

proof end;

theorem Th6: :: TREAL_1:6

for b₁, b₂, b₃, b₄ being real number st b₁ <= b₂ & b₃ <= b₄ & b₂ <= b₃ holds
Closed-Interval-TSpace b₂,b₃ is closed SubSpace of Closed-Interval-TSpace b₁,b₄

proof end;

theorem Th7: :: TREAL_1:7

for b₁, b₂, b₃, b₄ being real number st b₁ <= b₂ & b₃ <= b₄ & b₂ <= b₃ holds
( Closed-Interval-TSpace b₁,b₄ = (Closed-Interval-TSpace b₁,b₃) union (Closed-Interval-TSpace b₂,b₄) & Closed-Interval-TSpace b₂,b₃ = (Closed-Interval-TSpace b₁,b₃) meet (Closed-Interval-TSpace b₂,b₄) )

proof end;

definition

let c₁, c₂ be real number ;
assume E9: c₁ <= c₂ ;
func (#) c₁,c₂ -> Point of (Closed-Interval-TSpace a₁,a₂) equals :Def1: :: TREAL_1:def 1
a₁;
coherence

proof end;

correctness ;
func c₁,c₂ (#) -> Point of (Closed-Interval-TSpace a₁,a₂) equals :Def2: :: TREAL_1:def 2
a₂;
coherence

proof end;

correctness ;

end;

:: deftheorem Def1 defines (#) TREAL_1:def 1 :

:: deftheorem Def2 defines (#) TREAL_1:def 2 :

theorem Th8: :: TREAL_1:8

( 0[01] = (#) 0,1 & 1[01] = 0,1 (#) ) by Def1, Def2, BORSUK_1:def 17, BORSUK_1:def 18;

theorem Th9: :: TREAL_1:9

for b₁, b₂, b₃ being real number st b₁ <= b₂ & b₂ <= b₃ holds
( (#) b₁,b₂ = (#) b₁,b₃ & b₂,b₃ (#) = b₁,b₃ (#) )

proof end;

definition

let c₁, c₂ be real number ;
assume E11: c₁ <= c₂ ;
let c₃, c₄ be Point of (Closed-Interval-TSpace c₁,c₂);
func L[01] c₃,c₄ -> Function of (Closed-Interval-TSpace 0,1),(Closed-Interval-TSpace a₁,a₂) means :Def3: :: TREAL_1:def 3
for b₁ being Point of (Closed-Interval-TSpace 0,1)
for b₂, b₃, b₄ being real number st b₁ = b₂ & b₃ = a₃ & b₄ = a₄ holds
a₅ . b₁ = ((1 - b₂) * b₃) + (b₂ * b₄);
existence

proof end;

uniqueness

proof end;

end;

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

theorem Th10: :: TREAL_1:10

for b₁, b₂ being real number st b₁ <= b₂ holds
for b₃, b₄ being Point of (Closed-Interval-TSpace b₁,b₂)
for b₅ being Point of (Closed-Interval-TSpace 0,1)
for b₆, b₇, b₈ being real number st b₅ = b₆ & b₇ = b₃ & b₈ = b₄ holds
(L[01] b₃,b₄) . b₅ = ((b₈ - b₇) * b₆) + b₇

proof end;

theorem Th11: :: TREAL_1:11

for b₁, b₂ being real number st b₁ <= b₂ holds
for b₃, b₄ being Point of (Closed-Interval-TSpace b₁,b₂) holds L[01] b₃,b₄ is continuous Function of (Closed-Interval-TSpace 0,1),(Closed-Interval-TSpace b₁,b₂)

proof end;

theorem Th12: :: TREAL_1:12

for b₁, b₂ being real number st b₁ <= b₂ holds
for b₃, b₄ being Point of (Closed-Interval-TSpace b₁,b₂) holds
( (L[01] b₃,b₄) . ((#) 0,1) = b₃ & (L[01] b₃,b₄) . (0,1 (#) ) = b₄ )

proof end;

theorem Th13: :: TREAL_1:13

L[01] ((#) 0,1),(0,1 (#) ) = id (Closed-Interval-TSpace 0,1)

proof end;

definition

let c₁, c₂ be real number ;
assume E14: c₁ < c₂ ;
let c₃, c₄ be Point of (Closed-Interval-TSpace 0,1);
func P[01] c₁,c₂,c₃,c₄ -> Function of (Closed-Interval-TSpace a₁,a₂),(Closed-Interval-TSpace 0,1) means :Def4: :: TREAL_1:def 4
for b₁ being Point of (Closed-Interval-TSpace a₁,a₂)
for b₂, b₃, b₄ being real number st b₁ = b₂ & b₃ = a₃ & b₄ = a₄ holds
a₅ . b₁ = (((a₂ - b₂) * b₃) + ((b₂ - a₁) * b₄)) / (a₂ - a₁);
existence

proof end;

uniqueness

proof end;

end;

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

theorem Th14: :: TREAL_1:14

for b₁, b₂ being real number st b₁ < b₂ holds
for b₃, b₄ being Point of (Closed-Interval-TSpace 0,1)
for b₅ being Point of (Closed-Interval-TSpace b₁,b₂)
for b₆, b₇, b₈ being Real st b₅ = b₆ & b₇ = b₃ & b₈ = b₄ holds
(P[01] b₁,b₂,b₃,b₄) . b₅ = (((b₈ - b₇) / (b₂ - b₁)) * b₆) + (((b₂ * b₇) - (b₁ * b₈)) / (b₂ - b₁))

proof end;

theorem Th15: :: TREAL_1:15

for b₁, b₂ being real number st b₁ < b₂ holds
for b₃, b₄ being Point of (Closed-Interval-TSpace 0,1) holds P[01] b₁,b₂,b₃,b₄ is continuous Function of (Closed-Interval-TSpace b₁,b₂),(Closed-Interval-TSpace 0,1)

proof end;

theorem Th16: :: TREAL_1:16

for b₁, b₂ being real number st b₁ < b₂ holds
for b₃, b₄ being Point of (Closed-Interval-TSpace 0,1) holds
( (P[01] b₁,b₂,b₃,b₄) . ((#) b₁,b₂) = b₃ & (P[01] b₁,b₂,b₃,b₄) . (b₁,b₂ (#) ) = b₄ )

proof end;

theorem Th17: :: TREAL_1:17

P[01] 0,1,((#) 0,1),(0,1 (#) ) = id (Closed-Interval-TSpace 0,1)

proof end;

theorem Th18: :: TREAL_1:18

for b₁, b₂ being real number st b₁ < b₂ holds
( id (Closed-Interval-TSpace b₁,b₂) = (L[01] ((#) b₁,b₂),(b₁,b₂ (#) )) * (P[01] b₁,b₂,((#) 0,1),(0,1 (#) )) & id (Closed-Interval-TSpace 0,1) = (P[01] b₁,b₂,((#) 0,1),(0,1 (#) )) * (L[01] ((#) b₁,b₂),(b₁,b₂ (#) )) )

proof end;

theorem Th19: :: TREAL_1:19

for b₁, b₂ being real number st b₁ < b₂ holds
( id (Closed-Interval-TSpace b₁,b₂) = (L[01] (b₁,b₂ (#) ),((#) b₁,b₂)) * (P[01] b₁,b₂,(0,1 (#) ),((#) 0,1)) & id (Closed-Interval-TSpace 0,1) = (P[01] b₁,b₂,(0,1 (#) ),((#) 0,1)) * (L[01] (b₁,b₂ (#) ),((#) b₁,b₂)) )

proof end;

theorem Th20: :: TREAL_1:20

for b₁, b₂ being real number st b₁ < b₂ holds
( L[01] ((#) b₁,b₂),(b₁,b₂ (#) ) is_homeomorphism & (L[01] ((#) b₁,b₂),(b₁,b₂ (#) )) " = P[01] b₁,b₂,((#) 0,1),(0,1 (#) ) & P[01] b₁,b₂,((#) 0,1),(0,1 (#) ) is_homeomorphism & (P[01] b₁,b₂,((#) 0,1),(0,1 (#) )) " = L[01] ((#) b₁,b₂),(b₁,b₂ (#) ) )

proof end;

theorem Th21: :: TREAL_1:21

for b₁, b₂ being real number st b₁ < b₂ holds
( L[01] (b₁,b₂ (#) ),((#) b₁,b₂) is_homeomorphism & (L[01] (b₁,b₂ (#) ),((#) b₁,b₂)) " = P[01] b₁,b₂,(0,1 (#) ),((#) 0,1) & P[01] b₁,b₂,(0,1 (#) ),((#) 0,1) is_homeomorphism & (P[01] b₁,b₂,(0,1 (#) ),((#) 0,1)) " = L[01] (b₁,b₂ (#) ),((#) b₁,b₂) )

proof end;

theorem Th22: :: TREAL_1:22

I[01] is connected

proof end;

theorem Th23: :: TREAL_1:23

for b₁, b₂ being real number st b₁ <= b₂ holds
Closed-Interval-TSpace b₁,b₂ is connected

proof end;

theorem Th24: :: TREAL_1:24

for b₁ being continuous Function of I[01] ,I[01] ex b₂ being Point of I[01] st b₁ . b₂ = b₂

proof end;

theorem Th25: :: TREAL_1:25

for b₁, b₂ being real number st b₁ <= b₂ holds
for b₃ being continuous Function of (Closed-Interval-TSpace b₁,b₂),(Closed-Interval-TSpace b₁,b₂) ex b₄ being Point of (Closed-Interval-TSpace b₁,b₂) st b₃ . b₄ = b₄

proof end;

theorem Th26: :: TREAL_1:26

for b₁, b₂ being non empty SubSpace of R^1
for b₃ being continuous Function of b₁,b₂ st ex b₄, b₅ being Real st
( b₄ <= b₅ & [.b₄,b₅.] c= the carrier of b₁ & [.b₄,b₅.] c= the carrier of b₂ & b₃ .: [.b₄,b₅.] c= [.b₄,b₅.] ) holds
ex b₄ being Point of b₁ st b₃ . b₄ = b₄

proof end;

theorem Th27: :: TREAL_1:27

for b₁, b₂ being non empty SubSpace of R^1
for b₃ being continuous Function of b₁,b₂ st ex b₄, b₅ being Real st
( b₄ <= b₅ & [.b₄,b₅.] c= the carrier of b₁ & b₃ .: [.b₄,b₅.] c= [.b₄,b₅.] ) holds
ex b₄ being Point of b₁ st b₃ . b₄ = b₄

proof end;