:: JORDAN5A semantic presentation

for n being Nat
for p, q being Point of (TOP-REAL n)
for P being Subset of (TOP-REAL n) st P is_an_arc_of p,q holds
P is compact

proof end;

Lm1: for n being Nat holds
( the carrier of (Euclid n) = REAL n & the carrier of (TOP-REAL n) = REAL n )

proof end;

theorem Th2: :: JORDAN5A:2

for r being real number holds
( ( 0 <= r & r <= 1 ) iff r in the carrier of I[01] )

proof end;

theorem Th3: :: JORDAN5A:3

for n being Nat
for p1, p2 being Point of (TOP-REAL n)
for r1, r2 being real number holds
( not ((1 - r1) * p1) + (r1 * p2) = ((1 - r2) * p1) + (r2 * p2) or r1 = r2 or p1 = p2 )

proof end;

theorem Th4: :: JORDAN5A:4

for n being Nat
for p1, p2 being Point of (TOP-REAL n) st p1 <> p2 holds
ex f being Function of I[01] ,((TOP-REAL n) | (LSeg p1,p2)) st
( ( for x being Real st x in [.0,1.] holds
f . x = ((1 - x) * p1) + (x * p2) ) & f is_homeomorphism & f . 0 = p1 & f . 1 = p2 )

proof end;

Lm2: for n being Nat holds TOP-REAL n is arcwise_connected

proof end;

registration

let n be Nat;
cluster TOP-REAL n -> arcwise_connected ;
coherence by Lm2;

end;

registration

let n be Nat;
cluster non empty strict compact SubSpace of TOP-REAL n;
existence

proof end;

end;

theorem :: JORDAN5A:5

for a, b being Point of (TOP-REAL 2)
for f being Path of a,b
for P being non empty compact SubSpace of TOP-REAL 2
for g being Function of I[01] ,P st f is one-to-one & g = f & [#] P = rng f holds
g is_homeomorphism

proof end;

Lm3: for X being Subset of REAL st X is open holds
X in Family_open_set RealSpace

proof end;

Lm4: for X being Subset of REAL st X in Family_open_set RealSpace holds
X is open

proof end;

theorem :: JORDAN5A:6

for X being Subset of REAL holds
( X in Family_open_set RealSpace iff X is open ) by Lm3, Lm4;

theorem Th7: :: JORDAN5A:7

for f being Function of R^1 ,R^1
for x being Point of R^1
for g being PartFunc of REAL , REAL
for x1 being Real st f is_continuous_at x & f = g & x = x1 holds
g is_continuous_in x1

proof end;

theorem Th8: :: JORDAN5A:8

for f being continuous Function of R^1 ,R^1
for g being PartFunc of REAL , REAL st f = g holds
g is_continuous_on REAL

proof end;

Lm5: for f being one-to-one continuous Function of R^1 ,R^1
for g being PartFunc of REAL , REAL holds
( not f = g or g is_increasing_on [.0,1.] or g is_decreasing_on [.0,1.] )

proof end;

theorem :: JORDAN5A:9

for f being one-to-one continuous Function of R^1 ,R^1 holds
( for x, y being Point of I[01]
for p, q, fx, fy being Real st x = p & y = q & p < q & fx = f . x & fy = f . y holds
fx < fy or for x, y being Point of I[01]
for p, q, fx, fy being Real st x = p & y = q & p < q & fx = f . x & fy = f . y holds
fx > fy )

proof end;

theorem Th10: :: JORDAN5A:10

for r, gg, a, b being Real
for x being Element of (Closed-Interval-MSpace a,b) st a <= b & x = r & gg > 0 & ].(r - gg),(r + gg).[ c= [.a,b.] holds
].(r - gg),(r + gg).[ = Ball x,gg

proof end;

theorem Th11: :: JORDAN5A:11

for a, b being Real
for X being Subset of REAL st a < b & not a in X & not b in X & X in Family_open_set (Closed-Interval-MSpace a,b) holds
X is open

proof end;

theorem Th12: :: JORDAN5A:12

for X being open Subset of REAL
for a, b being Real st X c= [.a,b.] holds
( not a in X & not b in X )

proof end;

theorem Th13: :: JORDAN5A:13

for a, b being Real
for X being Subset of REAL
for V being Subset of (Closed-Interval-MSpace a,b) st a <= b & V = X & X is open holds
V in Family_open_set (Closed-Interval-MSpace a,b)

proof end;

Lm6: for a, b, c being real number st a <= b holds
( c in the carrier of (Closed-Interval-TSpace a,b) iff ( a <= c & c <= b ) )

proof end;

Lm7: for a, b, c, d being Real
for f being Function of (Closed-Interval-TSpace a,b),(Closed-Interval-TSpace c,d)
for x being Point of (Closed-Interval-TSpace a,b)
for g being PartFunc of REAL , REAL
for x1 being Real st a < b & c < d & f is_continuous_at x & x <> a & x <> b & f . a = c & f . b = d & f is one-to-one & f = g & x = x1 holds
g is_continuous_in x1

proof end;

theorem Th14: :: JORDAN5A:14

for a, b, c, d, x1 being Real
for f being Function of (Closed-Interval-TSpace a,b),(Closed-Interval-TSpace c,d)
for x being Point of (Closed-Interval-TSpace a,b)
for g being PartFunc of REAL , REAL st a < b & c < d & f is_continuous_at x & f . a = c & f . b = d & f is one-to-one & f = g & x = x1 holds
g | [.a,b.] is_continuous_in x1

proof end;

theorem Th15: :: JORDAN5A:15

for a, b, c, d being Real
for f being Function of (Closed-Interval-TSpace a,b),(Closed-Interval-TSpace c,d)
for g being PartFunc of REAL , REAL st f is continuous & f is one-to-one & a < b & c < d & f = g & f . a = c & f . b = d holds
g is_continuous_on [.a,b.]

proof end;

theorem Th16: :: JORDAN5A:16

for a, b, c, d being Real
for f being Function of (Closed-Interval-TSpace a,b),(Closed-Interval-TSpace c,d) st a < b & c < d & f is continuous & f is one-to-one & f . a = c & f . b = d holds
for x, y being Point of (Closed-Interval-TSpace a,b)
for p, q, fx, fy being Real st x = p & y = q & p < q & fx = f . x & fy = f . y holds
fx < fy

proof end;

theorem :: JORDAN5A:17

for f being one-to-one continuous Function of I[01] ,I[01] st f . 0 = 0 & f . 1 = 1 holds
for x, y being Point of I[01]
for p, q, fx, fy being Real st x = p & y = q & p < q & fx = f . x & fy = f . y holds
fx < fy by Th16, TOPMETR:27;

theorem :: JORDAN5A:18

for a, b, c, d being Real
for f being Function of (Closed-Interval-TSpace a,b),(Closed-Interval-TSpace c,d)
for P being non empty Subset of (Closed-Interval-TSpace a,b)
for PP, QQ being Subset of R^1 st a < b & c < d & PP = P & f is continuous & f is one-to-one & PP is compact & f . a = c & f . b = d & f .: P = QQ holds
f . (lower_bound ([#] PP)) = lower_bound ([#] QQ)

proof end;

theorem :: JORDAN5A:19

for a, b, c, d being Real
for f being Function of (Closed-Interval-TSpace a,b),(Closed-Interval-TSpace c,d)
for P, Q being non empty Subset of (Closed-Interval-TSpace a,b)
for PP, QQ being Subset of R^1 st a < b & c < d & PP = P & QQ = Q & f is continuous & f is one-to-one & PP is compact & f . a = c & f . b = d & f .: P = Q holds
f . (upper_bound ([#] PP)) = upper_bound ([#] QQ)

proof end;

theorem :: JORDAN5A:20

for a, b being real number st a <= b holds
( lower_bound [.a,b.] = a & upper_bound [.a,b.] = b )

proof end;

theorem :: JORDAN5A:21

for a, b, c, d, e, f, g, h being Real
for F being Function of (Closed-Interval-TSpace a,b),(Closed-Interval-TSpace c,d) st a < b & c < d & e < f & a <= e & f <= b & F is_homeomorphism & F . a = c & F . b = d & g = F . e & h = F . f holds
F .: [.e,f.] = [.g,h.]

proof end;

theorem :: JORDAN5A:22

for P, Q being Subset of (TOP-REAL 2)
for p1, p2 being Point of (TOP-REAL 2) st P meets Q & P /\ Q is closed & P is_an_arc_of p1,p2 holds
ex EX being Point of (TOP-REAL 2) st
( EX in P /\ Q & ex g being Function of I[01] ,((TOP-REAL 2) | P) ex s2 being Real st
( g is_homeomorphism & g . 0 = p1 & g . 1 = p2 & g . s2 = EX & 0 <= s2 & s2 <= 1 & ( for t being Real st 0 <= t & t < s2 holds
not g . t in Q ) ) )

proof end;

theorem :: JORDAN5A:23

proof end;