:: Intermediate Value Theorem and Thickness of Simple Closed Curves :: by Yatsuka Nakamura and Andrzej Trybulec :: :: Received November 13, 1997 :: Copyright (c) 1997-2012 Association of Mizar Users begin 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 proofend; theorem Th2: :: TOPREAL5:2 for ra, rb being real number st ra <= rb holds [#] (Closed-Interval-TSpace (ra,rb)) is connected proofend; theorem Th3: :: TOPREAL5:3 for A being Subset of R^1 for a being real number st not a in A & ex b, d being real number st ( b in A & d in A & b < a & a < d ) holds not A is connected proofend; :: [WP: ] 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 proofend; 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 ) proofend; ::Intermediate Value Theorem < theorem Th6: :: TOPREAL5:6 for ra, rb, a, b being real number st ra < rb holds for f being continuous Function of (Closed-Interval-TSpace (ra,rb)),R^1 for d being real number st f . ra = a & f . rb = b & a < d & d < b holds ex rc being Element of REAL st ( f . rc = d & ra < rc & rc < rb ) proofend; theorem Th7: :: TOPREAL5:7 for ra, rb, a, b being real number st ra < rb holds for f being continuous Function of (Closed-Interval-TSpace (ra,rb)),R^1 for d being real number st f . ra = a & f . rb = b & a > d & d > b holds ex rc being Element of REAL st ( f . rc = d & ra < rc & rc < rb ) proofend; :: [WP: ] Bolzano_theorem_(intermediate_value) theorem :: TOPREAL5:8 for ra, rb being real number for g being continuous Function of (Closed-Interval-TSpace (ra,rb)),R^1 for s1, s2 being real number st ra < rb & s1 * s2 < 0 & s1 = g . ra & s2 = g . rb holds ex r1 being Element of REAL st ( g . r1 = 0 & ra < r1 & r1 < rb ) proofend; theorem Th9: :: TOPREAL5:9 for g being Function of I[01],R^1 for s1, s2 being real number st g is continuous & g . 0 <> g . 1 & s1 = g . 0 & s2 = g . 1 holds ex r1 being Element of REAL st ( 0 < r1 & r1 < 1 & g . r1 = (s1 + s2) / 2 ) proofend; begin theorem Th10: :: TOPREAL5:10 for f being Function of (TOP-REAL 2),R^1 st f = proj1 holds f is continuous proofend; theorem Th11: :: TOPREAL5:11 for f being Function of (TOP-REAL 2),R^1 st f = proj2 holds f is continuous proofend; 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 Element of 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 ) ) proofend; 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 Element of 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 ) ) proofend; 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 Element of REAL ex p being Point of (TOP-REAL 2) st ( p in P & not p `2 = r ) proofend; 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 Element of REAL ex p being Point of (TOP-REAL 2) st ( p in P & not p `1 = r ) proofend; 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 proofend; 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 proofend; 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 proofend; 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 proofend; :: Moved from JORDAN1B, AK, 23.02.2006 registration cluster being_simple_closed_curve -> non horizontal non vertical for Element of K6( the carrier of (TOP-REAL 2)); coherence for b1 being Simple_closed_curve holds ( not b1 is vertical & not b1 is horizontal ) proofend; end;