:: Some Properties of Real Maps
:: by Adam Grabowski and Yatsuka Nakamura
::
:: Copyright (c) 1997-2021 Association of Mizar Users

theorem Th1: :: JORDAN5A:1
for n being Nat
for p, q being Point of ()
for P being Subset of () st P is_an_arc_of p,q holds
P is compact
proof end;

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

proof end;

theorem Th2: :: JORDAN5A:2
for n being Nat
for p1, p2 being Point of ()
for r1, r2 being Real holds
( not ((1 - r1) * p1) + (r1 * p2) = ((1 - r2) * p1) + (r2 * p2) or r1 = r2 or p1 = p2 )
proof end;

theorem Th3: :: JORDAN5A:3
for n being Nat
for p1, p2 being Point of () st p1 <> p2 holds
ex f being Function of I,(() | (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 Nat holds TOP-REAL n is pathwise_connected
proof end;

registration
let n be Nat;
coherence by Lm2;
end;

registration
let n be Nat;
existence
ex b1 being SubSpace of TOP-REAL n st
( b1 is compact & not b1 is empty & b1 is strict )
proof end;
end;

theorem :: JORDAN5A:4
for a, b being Point of ()
for f being Path of a,b
for P being non empty compact SubSpace of TOP-REAL 2
for g being Function of I,P st f is one-to-one & g = f & [#] P = rng f holds
g is being_homeomorphism by ;

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;

:: Equivalence of analytical and topological definitions of continuity
theorem Th5: :: JORDAN5A:5
for X being Subset of REAL holds
( X in Family_open_set RealSpace iff X is open ) by ;

theorem Th6: :: JORDAN5A:6
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 Th7: :: JORDAN5A:7
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:8
for f being one-to-one continuous Function of R^1,R^1 holds
( for x, y being Point of I
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
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 Th9: :: JORDAN5A:9
for r, gg, a, b being Real
for x being Element of () st a <= b & x = r & ].(r - gg),(r + gg).[ c= [.a,b.] holds
].(r - gg),(r + gg).[ = Ball (x,gg)
proof end;

theorem Th10: :: JORDAN5A:10
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 () holds
X is open
proof end;

theorem Th11: :: JORDAN5A:11
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 Th12: :: JORDAN5A:12
for a, b being Real
for X being Subset of REAL
for V being Subset of () st V = X & X is open holds
V in Family_open_set ()
proof end;

Lm6: for a, b, c being Real st a <= b holds
( c in the carrier of () iff ( a <= c & c <= b ) )

proof end;

Lm7: for a, b, c, d being Real
for f being Function of (),()
for x being Point of ()
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 Th13: :: JORDAN5A:13
for a, b, c, d, x1 being Real
for f being Function of (),()
for x being Point of ()
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 Th14: :: JORDAN5A:14
for a, b, c, d being Real
for f being Function of (),()
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;

:: On the monotonicity of continuous maps
theorem Th15: :: JORDAN5A:15
for a, b, c, d being Real
for f being Function of (),() 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 ()
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:16
for f being one-to-one continuous Function of I,I st f . 0 = 0 & f . 1 = 1 holds
for x, y being Point of I
for p, q, fx, fy being Real st x = p & y = q & p < q & fx = f . x & fy = f . y holds
fx < fy by ;

theorem :: JORDAN5A:17
for a, b, c, d being Real
for f being Function of (),()
for P being non empty Subset of ()
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:18
for a, b, c, d being Real
for f being Function of (),()
for P, Q being non empty Subset of ()
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:19
for a, b being Real st a <= b holds
( lower_bound [.a,b.] = a & upper_bound [.a,b.] = b )
proof end;

theorem :: JORDAN5A:20
for a, b, c, d, e, f, g, h being Real
for F being Function of (),() 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:21
for P, Q being Subset of ()
for p1, p2 being Point of () st P meets Q & P /\ Q is closed & P is_an_arc_of p1,p2 holds
ex EX being Point of () st
( EX in P /\ Q & ex g being Function of I,(() | 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:22
for P, Q being Subset of ()
for p1, p2 being Point of () st P meets Q & P /\ Q is closed & P is_an_arc_of p1,p2 holds
ex EX being Point of () st
( EX in P /\ Q & ex g being Function of I,(() | 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;

:: from TOPREAL6, 2011.07.29, A.T.
registration
cluster non empty V52() V53() V54() finite real-bounded for Element of K16(REAL);
existence
ex b1 being Subset of REAL st
( not b1 is empty & b1 is finite & b1 is real-bounded )
proof end;
end;

Lm8: R^1 = TopStruct(# the carrier of RealSpace, #)
by ;

theorem Th23: :: JORDAN5A:23
for A being Subset of REAL
for B being Subset of R^1 st A = B holds
( A is closed iff B is closed )
proof end;

theorem :: JORDAN5A:24
for A being Subset of REAL
for B being Subset of R^1 st A = B holds
Cl A = Cl B
proof end;

registration
let a, b be Real;
cluster K276(a,b) -> compact for Subset of REAL;
coherence
for b1 being Subset of REAL st b1 = [.a,b.] holds
b1 is compact
by RCOMP_1:6;
end;

theorem Th25: :: JORDAN5A:25
for A being Subset of REAL
for B being Subset of R^1 st A = B holds
( A is compact iff B is compact )
proof end;

registration
cluster finite -> compact for Element of K16(REAL);
coherence
for b1 being Subset of REAL st b1 is finite holds
b1 is compact
by ;
end;

theorem :: JORDAN5A:26
for a, b being Real holds
( a <> b iff Cl ].a,b.[ = [.a,b.] )
proof end;

theorem :: JORDAN5A:27
for T being TopStruct
for f being RealMap of T
for g being Function of T,R^1 st f = g holds
( f is continuous iff g is continuous )
proof end;