:: by Yatsuka Nakamura and Andrzej Trybulec

::

:: Received November 13, 1997

:: Copyright (c) 1997-2017 Association of Mizar Users

Lm1: for X, Y, Z being non empty TopSpace

for f being continuous Function of X,Y

for g being continuous Function of Y,Z holds g * f is continuous Function of X,Z

;

theorem Th1: :: TOPREAL5:1

for X being non empty TopSpace

for A, B1, B2 being Subset of X st B1 is open & B2 is open & B1 meets A & B2 meets A & A c= B1 \/ B2 & B1 misses B2 holds

not A is connected

for A, B1, B2 being Subset of X st B1 is open & B2 is open & B1 meets A & B2 meets A & A c= B1 \/ B2 & B1 misses B2 holds

not A is connected

proof end;

theorem Th3: :: TOPREAL5:3

for A being Subset of R^1

for a being Real st not a in A & ex b, d being Real st

( b in A & d in A & b < a & a < d ) holds

not A is connected

for a being Real st not a in A & ex b, d being Real st

( b in A & d in A & b < a & a < d ) holds

not A is connected

proof end;

:: Intermediate Value Theorem

theorem :: TOPREAL5:4

for X being non empty TopSpace

for xa, xb being Point of X

for a, b, d being Real

for f being continuous Function of X,R^1 st X is connected & f . xa = a & f . xb = b & a <= d & d <= b holds

ex xc being Point of X st f . xc = d

for xa, xb being Point of X

for a, b, d being Real

for f being continuous Function of X,R^1 st X is connected & f . xa = a & f . xb = b & a <= d & d <= b holds

ex xc being Point of X st f . xc = d

proof end;

theorem :: TOPREAL5:5

for X being non empty TopSpace

for xa, xb being Point of X

for B being Subset of X

for a, b, d being Real

for f being continuous Function of X,R^1 st B is connected & f . xa = a & f . xb = b & a <= d & d <= b & xa in B & xb in B holds

ex xc being Point of X st

( xc in B & f . xc = d )

for xa, xb being Point of X

for B being Subset of X

for a, b, d being Real

for f being continuous Function of X,R^1 st B is connected & f . xa = a & f . xb = b & a <= d & d <= b & xa in B & xb in B holds

ex xc being Point of X st

( xc in B & f . xc = d )

proof end;

::Intermediate Value Theorem <

theorem Th6: :: TOPREAL5:6

for ra, rb, a, b being Real st ra < rb holds

for f being continuous Function of (Closed-Interval-TSpace (ra,rb)),R^1

for d being Real st f . ra = a & f . rb = b & a < d & d < b holds

ex rc being Real st

( f . rc = d & ra < rc & rc < rb )

for f being continuous Function of (Closed-Interval-TSpace (ra,rb)),R^1

for d being Real st f . ra = a & f . rb = b & a < d & d < b holds

ex rc being Real st

( f . rc = d & ra < rc & rc < rb )

proof end;

theorem Th7: :: TOPREAL5:7

for ra, rb, a, b being Real st ra < rb holds

for f being continuous Function of (Closed-Interval-TSpace (ra,rb)),R^1

for d being Real st f . ra = a & f . rb = b & a > d & d > b holds

ex rc being Real st

( f . rc = d & ra < rc & rc < rb )

for f being continuous Function of (Closed-Interval-TSpace (ra,rb)),R^1

for d being Real st f . ra = a & f . rb = b & a > d & d > b holds

ex rc being Real st

( f . rc = d & ra < rc & rc < rb )

proof end;

theorem :: TOPREAL5:8

for ra, rb being Real

for g being continuous Function of (Closed-Interval-TSpace (ra,rb)),R^1

for s1, s2 being Real st ra < rb & s1 * s2 < 0 & s1 = g . ra & s2 = g . rb holds

ex r1 being Real st

( g . r1 = 0 & ra < r1 & r1 < rb )

for g being continuous Function of (Closed-Interval-TSpace (ra,rb)),R^1

for s1, s2 being Real st ra < rb & s1 * s2 < 0 & s1 = g . ra & s2 = g . rb holds

ex r1 being Real st

( g . r1 = 0 & ra < r1 & r1 < rb )

proof end;

theorem Th9: :: TOPREAL5:9

for g being Function of I[01],R^1

for s1, s2 being Real st g is continuous & g . 0 <> g . 1 & s1 = g . 0 & s2 = g . 1 holds

ex r1 being Real st

( 0 < r1 & r1 < 1 & g . r1 = (s1 + s2) / 2 )

for s1, s2 being Real st g is continuous & g . 0 <> g . 1 & s1 = g . 0 & s2 = g . 1 holds

ex r1 being Real st

( 0 < r1 & r1 < 1 & g . r1 = (s1 + s2) / 2 )

proof end;

theorem Th12: :: TOPREAL5:12

for P being non empty Subset of (TOP-REAL 2)

for f being Function of I[01],((TOP-REAL 2) | P) st f is continuous holds

ex g being Function of I[01],R^1 st

( g is continuous & ( for r being Real

for q being Point of (TOP-REAL 2) st r in the carrier of I[01] & q = f . r holds

q `1 = g . r ) )

for f being Function of I[01],((TOP-REAL 2) | P) st f is continuous holds

ex g being Function of I[01],R^1 st

( g is continuous & ( for r being Real

for q being Point of (TOP-REAL 2) st r in the carrier of I[01] & q = f . r holds

q `1 = g . r ) )

proof end;

theorem Th13: :: TOPREAL5:13

for P being non empty Subset of (TOP-REAL 2)

for f being Function of I[01],((TOP-REAL 2) | P) st f is continuous holds

ex g being Function of I[01],R^1 st

( g is continuous & ( for r being Real

for q being Point of (TOP-REAL 2) st r in the carrier of I[01] & q = f . r holds

q `2 = g . r ) )

for f being Function of I[01],((TOP-REAL 2) | P) st f is continuous holds

ex g being Function of I[01],R^1 st

( g is continuous & ( for r being Real

for q being Point of (TOP-REAL 2) st r in the carrier of I[01] & q = f . r holds

q `2 = g . r ) )

proof end;

theorem Th14: :: TOPREAL5:14

for P being non empty Subset of (TOP-REAL 2) st P is being_simple_closed_curve holds

for r being Real ex p being Point of (TOP-REAL 2) st

( p in P & not p `2 = r )

for r being Real ex p being Point of (TOP-REAL 2) st

( p in P & not p `2 = r )

proof end;

theorem Th15: :: TOPREAL5:15

for P being non empty Subset of (TOP-REAL 2) st P is being_simple_closed_curve holds

for r being Real ex p being Point of (TOP-REAL 2) st

( p in P & not p `1 = r )

for r being Real ex p being Point of (TOP-REAL 2) st

( p in P & not p `1 = r )

proof end;

theorem Th16: :: TOPREAL5:16

for C being non empty compact Subset of (TOP-REAL 2) st C is being_simple_closed_curve holds

N-bound C > S-bound C

N-bound C > S-bound C

proof end;

theorem Th17: :: TOPREAL5:17

for C being non empty compact Subset of (TOP-REAL 2) st C is being_simple_closed_curve holds

E-bound C > W-bound C

E-bound C > W-bound C

proof end;

theorem :: TOPREAL5:18

for P being non empty compact Subset of (TOP-REAL 2) st P is being_simple_closed_curve holds

S-min P <> N-max P

S-min P <> N-max P

proof end;

theorem :: TOPREAL5:19

for P being non empty compact Subset of (TOP-REAL 2) st P is being_simple_closed_curve holds

W-min P <> E-max P

W-min P <> E-max P

proof end;

:: Moved from JORDAN1B, AK, 23.02.2006

registration

for b_{1} being Simple_closed_curve holds

( not b_{1} is vertical & not b_{1} is horizontal )
end;

cluster being_simple_closed_curve -> non horizontal non vertical for Element of K16( the carrier of (TOP-REAL 2));

coherence for b

( not b

proof end;