:: by Adam Grabowski and Yatsuka Nakamura

::

:: Received September 10, 1997

:: Copyright (c) 1997-2012 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

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 Th2: :: JORDAN5A:2

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 )

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 Th3: :: JORDAN5A:3

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 )

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 ;

existence

ex b_{1} being SubSpace of TOP-REAL n st

( b_{1} is compact & not b_{1} is empty & b_{1} is strict )

end;
existence

ex b

( b

proof 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

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

:: Equivalence of analytical and topological definitions of continuity

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

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

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 )

( 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)

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

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 )

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

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

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

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

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

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

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)

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)

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, 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.]

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

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

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

existence

ex b_{1} being Subset of REAL st

( not b_{1} is empty & b_{1} is finite & b_{1} is real-bounded )

end;
ex b

( not b

proof end;

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

by PCOMPS_1:def 5, TOPMETR:def 6;

registration

let a, b be real number ;

coherence

for b_{1} being Subset of REAL st b_{1} = [.a,b.] holds

b_{1} is compact
by RCOMP_1:6;

end;
coherence

for b

b

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 )

for B being Subset of R^1 st A = B holds

( A is compact iff B is compact )

proof end;

registration

coherence

for b_{1} being Subset of REAL st b_{1} is finite holds

b_{1} is compact
by Th25, TOPMETR:17;

end;
for b

b

:::registration

::: cluster finite -> compact for Subset of REAL;

::: coherence;

:::end;

:::registration

::: let a, b be real number;

::: cluster [.a,b.] -> compact for Subset of REAL;

::: coherence;

:::end;

::: cluster finite -> compact for Subset of REAL;

::: coherence;

:::end;

:::registration

::: let a, b be real number;

::: cluster [.a,b.] -> compact for Subset of REAL;

::: coherence;

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

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;