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

theorem Th1: :: JORDAN5A:1

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 n being Nat
for p1, p2 being Point of (TOP-REAL n)
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 (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 Nat holds TOP-REAL n is pathwise_connected

proof end;

registration

let n be Nat;

cluster TOP-REAL n -> pathwise_connected ;

coherence
TOP-REAL n is pathwise_connected by Lm2;

end;

registration

let n be Nat;

cluster non empty strict TopSpace-like T_0 T_1 T_2 compact for 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:4

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 by COMPTS_1:17, PRE_TOPC:27;

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 Lm3, Lm4;

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[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 Th9: :: JORDAN5A:9

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 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 (Closed-Interval-MSpace (a,b)) 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 (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 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 Th13: :: JORDAN5A:13

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 Th14: :: JORDAN5A:14

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;

:: On the monotonicity of continuous maps

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)) 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:16

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 Th15, TOPMETR:20;

theorem :: JORDAN5A:17

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: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, 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: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 (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:21

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: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 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 b₁ being Subset of REAL st
( not b₁ is empty & b₁ is finite & b₁ is real-bounded )

proof end;

end;

Lm8: R^1 = TopStruct(# the carrier of RealSpace,(Family_open_set RealSpace) #)
by PCOMPS_1:def 5, TOPMETR:def 6;

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 b₁ being Subset of REAL st b₁ = [.a,b.] holds
b₁ 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 b₁ being Subset of REAL st b₁ is finite holds
b₁ is compact by Th25, TOPMETR:17;

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;