:: Intermediate Value Theorem and Thickness of Simple Closed Curves
:: by Yatsuka Nakamura and Andrzej Trybulec
::
:: Received November 13, 1997
:: Copyright (c) 1997-2016 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;
definitions TARSKI;
equalities STRUCT_0, RLVECT_1;
theorems BORSUK_1, EUCLID, FUNCT_1, FUNCT_2, PRE_TOPC, RCOMP_1, TARSKI,
TOPMETR, TOPS_2, TOPREAL1, TOPREAL2, TOPREAL3, METRIC_1, CONNSP_1,
TREAL_1, XREAL_0, PSCOMP_1, TMAP_1, FINSEQ_1, SPPOL_2, JORDAN2B,
XBOOLE_0, XBOOLE_1, TSEP_1, XREAL_1, SPPOL_1, XXREAL_0, XXREAL_1,
RELAT_1, RLVECT_1;
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;
Lm1: for f being continuous Function of X,Y, g being continuous Function of Y,
Z holds g*f is continuous Function of X,Z;
theorem Th1:
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
proof
let A,B1,B2 be Subset of X;
assume that
A1: B1 is open & B2 is open & B1 meets A and
A2: B2 meets A and
A3: A c= B1 \/ B2 and
A4: B1 misses B2;
reconsider C1=B1 /\ A, C2=B2 /\ A as Subset of X;
A5: A=(B1 \/ B2)/\A by A3,XBOOLE_1:28
.=C1 \/ C2 by XBOOLE_1:23;
A6: C2 <> {} by A2,XBOOLE_0:def 7;
A7: A is connected iff for P,Q being Subset of X st A = P \/ Q & P,Q
are_separated holds P = {}X or Q = {}X by CONNSP_1:15;
A8: C1 c= B1 & C2 c= B2 by XBOOLE_1:17;
B1,B2 are_separated & C1 <> {} by A1,A4,TSEP_1:37,XBOOLE_0:def 7;
hence thesis by A7,A5,A8,A6,CONNSP_1:7;
end;
theorem Th2:
for ra,rb st ra<=rb holds [#](Closed-Interval-TSpace(ra,rb)) is connected
proof
let ra,rb;
assume ra<=rb;
then Closed-Interval-TSpace(ra,rb) is connected by TREAL_1:20;
hence thesis by CONNSP_1:27;
end;
theorem Th3:
for A being Subset of R^1,a st not a in A & ex b,d st b in A & d
in A & ba};
set B1={r:ra;
r in REAL by XREAL_0:def 1;
hence thesis by A9;
end;
then reconsider C2=B2 as Subset of R^1 by METRIC_1:def 13,TOPMETR:12,def 6;
B1 c= REAL
proof
let x be object;
assume x in B1;
then consider r such that
A10: r=x and ra;
x in B1 by A12,XBOOLE_0:def 4;
then ex r1 st r1=x & r1d & d>b holds ex rc
st f.rc =d & rad and
A6: d>b;
A7: dom f=the carrier of Closed-Interval-TSpace(ra,rb) by FUNCT_2:def 1;
A8: [#](Closed-Interval-TSpace(ra,rb)) is connected by A1,Th2;
now
assume
A9: for rc st rad;
A10: now
assume d in f.:([#](Closed-Interval-TSpace(ra,rb)));
then consider x being object such that
A11: x in dom f and
x in [#](Closed-Interval-TSpace(ra,rb)) and
A12: d=f.x by FUNCT_1:def 6;
x in [.ra,rb.] by A2,A11;
then reconsider r=x as Real;
r<=rb by A2,A11,XXREAL_1:1;
then
A13: rb>r by A4,A6,A12,XXREAL_0:1;
ra<=r by A2,A11,XXREAL_1:1;
then ra0 & s2<0 or s1<0 & s2>0 by A2,XREAL_1:133;
hence thesis by A1,Th6,Th7;
end;
theorem Th9:
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 0g.1 and
A3: s1=g.0 & s2=g.1;
now
per cases by A2,A3,XXREAL_0:1;
case
s1 p2 and
A5: p1 in P and
A6: p2 in P and
A7: P1 is_an_arc_of p1,p2 and
A8: P2 is_an_arc_of p1,p2 and
A9: P = P1 \/ P2 and
A10: P1 /\ P2 = {p1,p2} by A1,TOPREAL2:6;
A11: p1`2=r0 by A3,A5;
A12: p2`2=r0 by A3,A6;
then
A13: p1`2=p2`2 by A3,A5;
A14: now
assume p1`1=p2`1;
then p1=|[p2`1,p2`2]| by A13,EUCLID:53;
hence contradiction by A4,EUCLID:53;
end;
consider f2 being Function of I[01], (TOP-REAL 2)|P2 such that
A15: f2 is being_homeomorphism and
A16: f2.0 = p1 and
A17: f2.1 = p2 by A8,TOPREAL1:def 1;
f2 is continuous by A15,TOPS_2:def 5;
then consider g2 being Function of I[01],R^1 such that
A18: g2 is continuous and
A19: for r,q2 st r in the carrier of I[01] & q2= f2.r holds q2`1=g2.r by Th12;
A20: [#]((TOP-REAL 2)|P2) = P2 by PRE_TOPC:def 5;
1 in {0,1} by TARSKI:def 2;
then
A21: 1 in the carrier of I[01] by A2,BORSUK_1:40,XBOOLE_0:def 3;
then
A22: p2`1=g2.1 by A17,A19;
0 in {0,1} by TARSKI:def 2;
then
A23: 0 in the carrier of I[01] by A2,BORSUK_1:40,XBOOLE_0:def 3;
then p1`1=g2.0 by A16,A19;
then consider r2 such that
A24: 0 p2 and
A5: p1 in P and
A6: p2 in P and
A7: P1 is_an_arc_of p1,p2 and
A8: P2 is_an_arc_of p1,p2 and
A9: P = P1 \/ P2 and
A10: P1 /\ P2 = {p1,p2} by A1,TOPREAL2:6;
A11: p1`1=r0 by A3,A5;
A12: p2`1=r0 by A3,A6;
then
A13: p1`1=p2`1 by A3,A5;
A14: now
assume p1`2=p2`2;
then p1=|[p2`1,p2`2]| by A13,EUCLID:53;
hence contradiction by A4,EUCLID:53;
end;
consider f2 being Function of I[01], (TOP-REAL 2)|P2 such that
A15: f2 is being_homeomorphism and
A16: f2.0 = p1 and
A17: f2.1 = p2 by A8,TOPREAL1:def 1;
f2 is continuous by A15,TOPS_2:def 5;
then consider g2 being Function of I[01],R^1 such that
A18: g2 is continuous and
A19: for r,q2 st r in the carrier of I[01] & q2= f2.r holds q2`2=g2.r by Th13;
A20: [#]((TOP-REAL 2)|P2) = P2 by PRE_TOPC:def 5;
1 in {0,1} by TARSKI:def 2;
then
A21: 1 in the carrier of I[01] by A2,BORSUK_1:40,XBOOLE_0:def 3;
then
A22: p2`2=g2.1 by A17,A19;
0 in {0,1} by TARSKI:def 2;
then
A23: 0 in the carrier of I[01] by A2,BORSUK_1:40,XBOOLE_0:def 3;
then p1`2=g2.0 by A16,A19;
then consider r2 such that
A24: 0 S-bound(C)
proof
let C be compact non empty Subset of TOP-REAL 2;
assume
A1: C is being_simple_closed_curve;
now
assume
A2: N-bound C <= S-bound C;
for p st p in C holds p`2=S-bound C
proof
let p;
assume p in C;
then
A3: S-bound C <= p`2 & p`2 <= N-bound C by PSCOMP_1:24;
then S-bound C <= N-bound C by XXREAL_0:2;
then S-bound C = N-bound C by A2,XXREAL_0:1;
hence thesis by A3,XXREAL_0:1;
end;
hence contradiction by A1,Th14;
end;
hence thesis;
end;
theorem Th17:
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)
proof
let C be compact non empty Subset of TOP-REAL 2;
assume
A1: C is being_simple_closed_curve;
now
assume
A2: E-bound C <= W-bound C;
for p st p in C holds p`1=W-bound C
proof
let p;
assume p in C;
then
A3: W-bound C <= p`1 & p`1 <= E-bound C by PSCOMP_1:24;
then W-bound C <= E-bound C by XXREAL_0:2;
then W-bound C = E-bound C by A2,XXREAL_0:1;
hence thesis by A3,XXREAL_0:1;
end;
hence contradiction by A1,Th15;
end;
hence thesis;
end;
theorem
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)
proof
let P be compact non empty Subset of TOP-REAL 2;
assume
A1: P is being_simple_closed_curve;
now
A2: |[lower_bound (proj1|S-most P), S-bound P]|=S-min(P) &
|[upper_bound (proj1|N-most P),
N-bound P]|=N-max(P) by PSCOMP_1:def 22,def 26;
assume S-min(P)=N-max(P);
then S-bound P= N-bound P by A2,SPPOL_2:1;
hence contradiction by A1,Th16;
end;
hence thesis;
end;
theorem
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)
proof
let P be compact non empty Subset of TOP-REAL 2;
assume
A1: P is being_simple_closed_curve;
now
A2: |[W-bound P, lower_bound (proj2|W-most P)]|=W-min(P) &
|[E-bound P, upper_bound (proj2
| E-most P)]|=E-max(P) by PSCOMP_1:def 19,def 23;
assume W-min(P)=E-max(P);
then W-bound P= E-bound P by A2,SPPOL_2:1;
hence contradiction by A1,Th17;
end;
hence thesis;
end;
:: Moved from JORDAN1B, AK, 23.02.2006
registration
cluster -> non vertical non horizontal for Simple_closed_curve;
coherence
proof
let S be Simple_closed_curve;
consider p1 be object such that
A1: p1 in S by XBOOLE_0:def 1;
reconsider p1 as Point of TOP-REAL 2 by A1;
ex p2 be Point of TOP-REAL 2 st p2 in S & p2`1 <> p1`1 by Th15;
hence S is non vertical by A1,SPPOL_1:def 3;
ex p2 be Point of TOP-REAL 2 st p2 in S & p2`2 <> p1`2 by Th14;
hence thesis by A1,SPPOL_1:def 2;
end;
end;