:: Intermediate Value Theorem and Thickness of Simple Closed Curves
::  by Yatsuka Nakamura and Andrzej Trybulec
::
:: Received November 13, 1997
:: Copyright (c) 1997-2021 Association of Mizar Users
::           (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.

environ

 vocabularies NUMBERS, SUBSET_1, PRE_TOPC, EUCLID, XBOOLE_0, ORDINAL2, FUNCT_1,
      RELAT_1, RCOMP_1, TARSKI, RELAT_2, CONNSP_1, XXREAL_0, TOPMETR, ARYTM_3,
      REAL_1, STRUCT_0, XXREAL_1, CARD_1, BORSUK_1, FINSEQ_1, PARTFUN1,
      MCART_1, TOPREAL2, TOPREAL1, TOPS_2, ARYTM_1, SUPINF_2, PSCOMP_1,
      SPPOL_1, SEQ_4;
 notations TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, XREAL_0,
      REAL_1, RELAT_1, FUNCT_1, RELSET_1, PARTFUN1, STRUCT_0, PRE_TOPC, TOPS_2,
      COMPTS_1, RCOMP_1, FINSEQ_1, RLVECT_1, EUCLID, TOPMETR, TOPREAL1,
      TOPREAL2, TMAP_1, CONNSP_1, SPPOL_1, PSCOMP_1, XXREAL_0;
 constructors REAL_1, RCOMP_1, CONNSP_1, TOPS_2, COMPTS_1, TMAP_1, TOPMETR,
      TOPREAL1, TOPREAL2, SPPOL_1, PSCOMP_1, BINOP_2, MONOID_0, PCOMPS_1;
 registrations XBOOLE_0, RELSET_1, FUNCT_2, NUMBERS, XREAL_0, MEMBERED,
      STRUCT_0, PRE_TOPC, BORSUK_1, EUCLID, TOPMETR, TOPREAL2, JORDAN2B,
      MONOID_0, TMAP_1;
 requirements REAL, NUMERALS, BOOLE, SUBSET, ARITHM;


begin ::1.   INTERMEDIATE VALUE THEOREMS AND BOLZANO THEOREM

reserve x for set;
reserve a,b,d,ra,rb,r0,s1,s2 for Real;
reserve r,s,r1,r2,r3,rc for 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,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:2
  for ra,rb st ra<=rb holds [#](Closed-Interval-TSpace(ra,rb)) is connected;

theorem :: TOPREAL5:3
  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;

::$N Intermediate Value Theorem
theorem :: TOPREAL5:4
 ::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 Function 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:5 ::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 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 ex xc being Point of X st xc
  in B & f.xc =d;

::Intermediate Value Theorem <

theorem :: TOPREAL5:6
  for ra,rb,a,b st ra<rb for f being continuous Function 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:7
  for ra,rb,a,b st ra<rb holds for f being continuous Function 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;

::$N Bolzano theorem (intermediate value)
theorem :: TOPREAL5:8 ::The Bolzano Theorem
  for ra,rb for g being continuous Function 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:9
  for g being Function 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:10
  for f being Function of TOP-REAL 2,R^1 st f=proj1 holds f is continuous;

theorem :: TOPREAL5:11
  for f being Function of TOP-REAL 2,R^1 st f=proj2 holds f is continuous;

theorem :: TOPREAL5:12
  for P being non empty Subset of TOP-REAL 2, f being Function of
I[01], (TOP-REAL 2)|P st f is continuous ex g being Function 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:13
  for P being non empty Subset of TOP-REAL 2, f being Function of
I[01], (TOP-REAL 2)|P st f is continuous ex g being Function 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:14
  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:15
  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:16
  for C being compact non empty Subset of TOP-REAL 2 st C is
  being_simple_closed_curve holds N-bound(C) > S-bound(C);

theorem :: TOPREAL5:17
  for C being compact non empty Subset of TOP-REAL 2 st C is
  being_simple_closed_curve holds E-bound(C) > W-bound(C);

theorem :: TOPREAL5:18
  for P being compact non empty Subset of TOP-REAL 2 st P is
  being_simple_closed_curve holds S-min(P)<>N-max(P);

theorem :: TOPREAL5:19
  for P being compact non empty Subset of TOP-REAL 2 st P is
  being_simple_closed_curve holds W-min(P)<>E-max(P);

:: Moved from JORDAN1B, AK, 23.02.2006

registration
  cluster -> non vertical non horizontal for Simple_closed_curve;
end;