:: Some Properties of Real Maps
:: by Adam Grabowski and Yatsuka Nakamura
::
:: Received September 10, 1997
:: Copyright (c) 1997-2011 Association of Mizar Users

begin

theorem Th1: :: JORDAN5A:1

for n being Element of 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 Element of NAT holds
( the carrier of (Euclid n) = REAL n & the carrier of (TOP-REAL n) = REAL n )

proof end;

theorem :: JORDAN5A:2

canceled;

theorem Th3: :: JORDAN5A:3

for n being Element of 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 Element of 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 being_homeomorphism & f . 0 = p1 & f . 1 = p2 )

proof end;

Lm2: for n being Element of NAT holds TOP-REAL n is pathwise_connected

proof end;

registration

let n be Element of NAT ;
cluster TOP-REAL n -> pathwise_connected ;
coherence
TOP-REAL n is pathwise_connected by Lm2;

end;

registration

let n be Element of NAT ;
cluster non empty strict TopSpace-like T_0 T_1 T_2 compact SubSpace of TOP-REAL n;
existence
ex b₁ being SubSpace of TOP-REAL n st
( b₁ is compact & not b₁ is empty & b₁ is strict )

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

begin

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

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 | [.0,1.] is increasing or g | [.0,1.] is decreasing )

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 & ].(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 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 | [.a,b.] is continuous

proof end;

begin

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

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 being_homeomorphism & g . 0 = p1 & g . 1 = p2 & g . s2 = EX & 0 <= s2 & s2 <= 1 & ( for t being Real st 1 >= t & t > s2 holds
not g . t in Q ) ) )

proof end;