Volume 9, 1997

University of Bialystok

Copyright (c) 1997 Association of Mizar Users

### The abstract of the Mizar article:

### Intermediate Value Theorem and Thickness of Simple Closed Curves

**by****Yatsuka Nakamura, and****Andrzej Trybulec**- Received November 13, 1997
- MML identifier: TOPREAL5

- [ Mizar article, MML identifier index ]

environ vocabulary PRE_TOPC, EUCLID, ARYTM, RCOMP_1, BOOLE, CONNSP_1, SUBSET_1, RELAT_2, RELAT_1, FUNCT_1, ORDINAL2, TOPMETR, PCOMPS_1, METRIC_1, ARYTM_1, ABSVALUE, BORSUK_1, ARYTM_3, FUNCT_5, FINSEQ_1, MCART_1, TOPREAL2, TOPREAL1, TOPS_2, COMPTS_1, PSCOMP_1, REALSET1; notation TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, XREAL_0, REAL_1, RELAT_1, FUNCT_1, STRUCT_0, PRE_TOPC, TOPS_2, COMPTS_1, RCOMP_1, FINSEQ_1, METRIC_1, PCOMPS_1, EUCLID, TOPMETR, TOPREAL1, TOPREAL2, TMAP_1, CONNSP_1, ABSVALUE, BORSUK_1, PSCOMP_1, JORDAN2B; constructors REAL_1, ABSVALUE, TOPS_2, RCOMP_1, TOPMETR, TOPREAL1, TOPREAL2, TMAP_1, CONNSP_1, PSCOMP_1, COMPTS_1, JORDAN2B; clusters FUNCT_1, PRE_TOPC, METRIC_1, TOPMETR, STRUCT_0, EUCLID, BORSUK_1, PSCOMP_1, XREAL_0, RELSET_1, ARYTM_3, MEMBERED, ORDINAL2; requirements REAL, NUMERALS, BOOLE, SUBSET, ARITHM; begin ::1. INTERMEDIATE VALUE THEOREMS AND BOLZANO THEOREM reserve x,x1 for set; reserve a,b,d,ra,rb,r0,s1,s2 for real number; reserve r,s,r1,r2,r3,rc for Element of REAL; reserve p,q,q1,q2 for Point of TOP-REAL 2; reserve X,Y,Z for non empty TopSpace; theorem :: TOPREAL5:1 for a,b,c being real number holds c in [.a,b.] iff a<=c & c <=b; canceled 2; theorem :: TOPREAL5:4 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 A is not connected; theorem :: TOPREAL5:5 for f being continuous map of X,Y, A being Subset of X st A is connected holds f.:A is connected; theorem :: TOPREAL5:6 for ra,rb st ra<=rb holds [#](Closed-Interval-TSpace(ra,rb)) is connected; ::The proof of the following is almost same as TREAL_1:4 theorem :: TOPREAL5:7 for A being Subset of R^1,a st A={r:a<r} holds A is open; ::The proof of the following is almost same as TREAL_1:4 theorem :: TOPREAL5:8 for A being Subset of R^1,a st A={r:a>r} holds A is open; theorem :: TOPREAL5:9 for A being Subset of R^1,a st not a in A & ex b,d st b in A & d in A & b<a & a<d holds not A is connected; theorem :: TOPREAL5:10 ::General Intermediate Value Point Theorem for X being non empty TopSpace,xa,xb being Point of X, a,b,d being Real,f being continuous map of X,R^1 st X is connected & f.xa=a & f.xb=b & a<=d & d<=b ex xc being Point of X st f.xc =d; theorem :: TOPREAL5:11 ::General Intermediate Value Theorem II for X being non empty TopSpace,xa,xb being Point of X, B being Subset of X, a,b,d being Real,f being continuous map of X,R^1 st B is connected & f.xa=a & f.xb=b & a<=d & d<=b & xa in B & xb in B ex xc being Point of X st xc in B & f.xc =d; ::Intermediate Value Theorem < theorem :: TOPREAL5:12 for ra,rb,a,b st ra<rb for f being continuous map of Closed-Interval-TSpace(ra,rb),R^1,d st f.ra=a & f.rb=b & a<d & d<b ex rc st f.rc =d & ra<rc & rc <rb; theorem :: TOPREAL5:13 ::Intermediate Value Theorem > for ra,rb,a,b st ra<rb holds for f being continuous map of Closed-Interval-TSpace(ra,rb),R^1,d st f.ra=a & f.rb=b & a>d & d>b holds ex rc st f.rc =d & ra<rc & rc <rb; theorem :: TOPREAL5:14 ::The Bolzano Theorem for ra,rb for g being continuous map of Closed-Interval-TSpace(ra,rb),R^1,s1,s2 st ra<rb & s1*s2<0 & s1=g.ra & s2=g.rb ex r1 st g.r1=0 & ra<r1 & r1<rb; theorem :: TOPREAL5:15 for g being map of I[01],R^1,s1,s2 st g is continuous & g.0<>g.1 & s1=g.0 & s2=g.1 holds ex r1 st 0<r1 & r1<1 & g.r1=(s1+s2)/2; begin ::2. SIMPLE CLOSED CURVES ARE NOT FLAT theorem :: TOPREAL5:16 for f being map of TOP-REAL 2,R^1 st f=proj1 holds f is continuous; theorem :: TOPREAL5:17 for f being map of TOP-REAL 2,R^1 st f=proj2 holds f is continuous; theorem :: TOPREAL5:18 for P being non empty Subset of TOP-REAL 2, f being map of I[01], (TOP-REAL 2)|P st f is continuous ex g being map of I[01],R^1 st g is continuous & for r,q st r in the carrier of I[01] & q= f.r holds q`1=g.r; theorem :: TOPREAL5:19 for P being non empty Subset of TOP-REAL 2, f being map of I[01], (TOP-REAL 2)|P st f is continuous ex g being map of I[01],R^1 st g is continuous & for r,q st r in the carrier of I[01] & q= f.r holds q`2=g.r; theorem :: TOPREAL5:20 for P being non empty Subset of TOP-REAL 2 st P is being_simple_closed_curve holds not (ex r st for p st p in P holds p`2=r); theorem :: TOPREAL5:21 for P being non empty Subset of TOP-REAL 2 st P is being_simple_closed_curve holds not (ex r st for p st p in P holds p`1=r); theorem :: TOPREAL5:22 for C being compact non empty Subset of TOP-REAL 2 st C is_simple_closed_curve holds N-bound(C) > S-bound(C); theorem :: TOPREAL5:23 for C being compact non empty Subset of TOP-REAL 2 st C is_simple_closed_curve holds E-bound(C) > W-bound(C); theorem :: TOPREAL5:24 for P being compact non empty Subset of TOP-REAL 2 st P is_simple_closed_curve holds S-min(P)<>N-max(P); theorem :: TOPREAL5:25 for P being compact non empty Subset of TOP-REAL 2 st P is_simple_closed_curve holds W-min(P)<>E-max(P);

Back to top