:: Intermediate Value Theorem and Thickness of Simple Closed Curves
:: by Yatsuka Nakamura and Andrzej Trybulec
::
:: Received November 13, 1997
:: Copyright (c) 1997-2026 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 & b<a & a<d holds not A is connected
proof
let A be Subset of R^1,a;
assume that
A1: not a in A and
A2: ex b,d st b in A & d in A & b<a & a<d;
consider b,d such that
A3: b in A and
A4: d in A and
A5: b<a and
A6: a<d by A2;
set B2={s:s>a};
set B1={r:r<a};
A7: A c= B1 \/ B2
proof
let x be object;
assume
A8: x in A;
then reconsider r=x as Real;
r<a or a<r by A1,A8,XXREAL_0:1;
then r in B1 or r in B2;
hence thesis by XBOOLE_0:def 3;
end;
B2 c= REAL
proof
let x be object;
assume x in B2;
then consider r such that
A9: r=x and r>a;
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 r<a;
r in REAL by XREAL_0:def 1;
hence thesis by A10;
end;
then reconsider C1=B1 as Subset of R^1 by METRIC_1:def 13,TOPMETR:12,def 6;
A11: now
assume B1 meets B2;
then consider x being object such that
A12: x in B1 /\ B2 by XBOOLE_0:4;
x in B2 by A12,XBOOLE_0:def 4;
then
A13: ex r2 st r2=x & r2>a;
x in B1 by A12,XBOOLE_0:def 4;
then ex r1 st r1=x & r1<a;
hence contradiction by A13;
end;
reconsider r1 = d as Element of REAL by XREAL_0:def 1;
r1 in B2 by A6;
then d in B2 /\ A by A4,XBOOLE_0:def 4;
then
A14: B2 meets A by XBOOLE_0:4;
reconsider r = b as Element of REAL by XREAL_0:def 1;
r in B1 by A5;
then b in B1 /\ A by A3,XBOOLE_0:def 4;
then
A15: B1 meets A by XBOOLE_0:4;
C1 is open & C2 is open by JORDAN2B:24,25;
hence thesis by A11,A15,A14,A7,Th1;
end;
::$N Intermediate Value Theorem
::$L https://en.wikipedia.org/wiki/Intermediate_value_theorem Intermediate Value Theorem
theorem
::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
proof
let X be non empty TopSpace,xa,xb be Point of X,
a,b,d be Real,f be
continuous Function of X,R^1;
assume that
A1: X is connected and
A2: f.xa=a & f.xb=b and
A3: a<=d & d<=b;
now
assume ( not a=d)& not d=b;
then
A4: a<d & d<b by A3,XXREAL_0:1;
now
assume
A5: not ex rc being Point of X st f.rc=d;
A6: now
assume d in f.:([#](X));
then ex x being object
st x in the carrier of X & x in [#](X) & d = f.x by
FUNCT_2:64;
hence contradiction by A5;
end;
dom f=the carrier of X by FUNCT_2:def 1;
then
A7: a in f.:([#](X)) & b in f.:([#](X)) by A2,FUNCT_1:def 6;
[#](X) is connected by A1,CONNSP_1:27;
hence contradiction by A4,A6,A7,Th3,TOPS_2:61;
end;
hence thesis;
end;
hence thesis by A2;
end;
theorem ::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
proof
let X be non empty TopSpace, xa,xb be Point of X, B be Subset of X, a,b,d be
Real,f be continuous Function of X,R^1;
assume that
A1: B is connected and
A2: f.xa=a & f.xb=b and
A3: a<=d & d<=b and
A4: xa in B & xb in B;
now
assume ( not a=d)& not d=b;
then
A5: a<d & d<b by A3,XXREAL_0:1;
now
assume
A6: not ex rc being Point of X st rc in B & f.rc=d;
A7: now
assume d in f.:B;
then ex x being object
st x in the carrier of X & x in B & d = f.x by FUNCT_2:64;
hence contradiction by A6;
end;
dom f=the carrier of X by FUNCT_2:def 1;
then a in f.:B & b in f.:B by A2,A4,FUNCT_1:def 6;
hence contradiction by A1,A5,A7,Th3,TOPS_2:61;
end;
hence thesis;
end;
hence thesis by A2,A4;
end;
::Intermediate Value Theorem <
theorem Th6:
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
proof
let ra,rb,a,b;
assume
A1: ra<rb;
let f be continuous Function of Closed-Interval-TSpace(ra,rb),R^1,d;
assume that
A2: f.ra=a and
A3: f.rb=b and
A4: a<d and
A5: d<b;
now
reconsider C=f.:([#](Closed-Interval-TSpace(ra,rb))) as Subset of R^1;
A6: dom f=the carrier of Closed-Interval-TSpace(ra,rb) by FUNCT_2:def 1;
A7: the carrier of Closed-Interval-TSpace(ra,rb)=[.ra,rb.] by A1,TOPMETR:18;
then rb in [#](Closed-Interval-TSpace(ra,rb)) by A1,XXREAL_1:1;
then
A8: b in f.:([#](Closed-Interval-TSpace(ra,rb))) by A3,A6,FUNCT_1:def 6;
assume
A9: not ex rc st (f.rc) =d & ra<rc & rc <rb;
A10: now
assume d in f.:([#](Closed-Interval-TSpace(ra,rb)));
then consider x being object such that
A11: x in the carrier of Closed-Interval-TSpace(ra,rb) and
x in [#](Closed-Interval-TSpace(ra,rb)) and
A12: d = f.x by FUNCT_2:64;
reconsider r=x as Real by A11;
r<=rb by A7,A11,XXREAL_1:1;
then
A13: r<rb by A3,A5,A12,XXREAL_0:1;
ra<=r by A7,A11,XXREAL_1:1;
then ra<r by A2,A4,A12,XXREAL_0:1;
hence contradiction by A9,A12,A13;
end;
ra in [#](Closed-Interval-TSpace(ra,rb)) by A1,A7,XXREAL_1:1;
then a in f.:([#](Closed-Interval-TSpace(ra,rb))) by A2,A6,FUNCT_1:def 6;
then not C is connected by A4,A5,A10,A8,Th3;
hence contradiction by A1,Th2,TOPS_2:61;
end;
hence thesis;
end;
theorem Th7:
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
proof
let ra,rb,a,b;
assume
A1: ra<rb;
then
A2: the carrier of Closed-Interval-TSpace(ra,rb)=[.ra,rb.] by TOPMETR:18;
let f be continuous Function of Closed-Interval-TSpace(ra,rb),R^1,d;
assume that
A3: f.ra=a and
A4: f.rb=b and
A5: a>d 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 ra<rc & rc <rb holds (f.rc)<>d;
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 ra<r by A3,A5,A12,XXREAL_0:1;
hence contradiction by A9,A12,A13;
end;
rb in [.ra,rb.] by A1,XXREAL_1:1;
then
A14: b in f.:([#](Closed-Interval-TSpace(ra,rb))) by A4,A2,A7,FUNCT_1:def 6;
ra in [.ra,rb.] by A1,XXREAL_1:1;
then a in f.:([#](Closed-Interval-TSpace(ra,rb))) by A3,A2,A7,FUNCT_1:def 6
;
hence contradiction by A5,A6,A8,A10,A14,Th3,TOPS_2:61;
end;
hence thesis;
end;
::$N Bolzano theorem (intermediate value)
theorem ::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
proof
let ra,rb;
let g be continuous Function of Closed-Interval-TSpace(ra,rb),R^1,s1,s2;
assume that
A1: ra<rb and
A2: s1*s2<0;
s1>0 & 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 0<r1 & r1<1 & g.r1=(s1+s2)/2
proof
let g be Function of I[01],R^1,s1,s2;
assume that
A1: g is continuous and
A2: g.0<>g.1 and
A3: s1=g.0 & s2=g.1;
now
per cases by A2,A3,XXREAL_0:1;
case
s1<s2;
then s1<(s1+s2)/2 & (s1+s2)/2<s2 by XREAL_1:226;
hence ex rc st (g.rc) =(s1+s2)/2 & 0<rc & rc <1 by A1,A3,Th6,TOPMETR:20;
end;
case
s2<s1;
then s2<(s1+s2)/2 & (s1+s2)/2<s1 by XREAL_1:226;
hence ex rc st (g.rc) =(s1+s2)/2 & 0<rc & rc <1 by A1,A3,Th7,TOPMETR:20;
end;
end;
hence thesis;
end;
begin ::2. SIMPLE CLOSED CURVES ARE NOT FLAT
theorem Th10:
for f being Function of TOP-REAL 2,R^1 st f=proj1 holds f is continuous
proof
let f be Function of TOP-REAL 2,R^1;
assume f=proj1;
then 1 in Seg 2 & for p being Element of TOP-REAL 2 holds f.p=p/.1 by
FINSEQ_1:1,JORDAN2B:30;
hence thesis by JORDAN2B:18;
end;
theorem Th11:
for f being Function of TOP-REAL 2,R^1 st f=proj2 holds f is continuous
proof
let f be Function of TOP-REAL 2,R^1;
assume f=proj2;
then 2 in Seg 2 & for p being Element of TOP-REAL 2 holds f.p=p/.2 by
FINSEQ_1:1,JORDAN2B:30;
hence thesis by JORDAN2B:18;
end;
theorem Th12:
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
proof
reconsider rj=proj1 as Function of (TOP-REAL 2),R^1 by TOPMETR:17;
let P be non empty Subset of TOP-REAL 2, f be Function of I[01], (TOP-REAL 2
)|P;
assume
A1: f is continuous;
reconsider f1=f as Function;
set h=(proj1|P)*f;
A2: [#]((TOP-REAL 2)|P)=P by PRE_TOPC:def 5;
then
A3: rng f1 c= P by RELAT_1:def 19;
rj is continuous Function of TOP-REAL 2,R^1 by Th10;
then rj|((TOP-REAL 2)|P) is continuous Function of ((TOP-REAL 2)|P),R^1;
then rj|P is continuous Function of ((TOP-REAL 2)|P),R^1 by A2,TMAP_1:def 3;
then reconsider h2=h as continuous Function of I[01],R^1 by A1,Lm1;
take h2;
thus h2 is continuous;
let r be Real,q be Point of TOP-REAL 2;
assume that
A4: r in the carrier of I[01] and
A5: q= f.r;
A6: dom proj1=the carrier of TOP-REAL 2 by FUNCT_2:def 1;
A7: r in dom f1 by A4,FUNCT_2:def 1;
then f1.r in rng f1 by FUNCT_1:def 3;
then
A8: q in dom proj1 /\ P by A5,A3,A6,XBOOLE_0:def 4;
thus h2.r = (proj1|P).q by A5,A7,FUNCT_1:13
.= proj1.q by A8,FUNCT_1:48
.= q`1 by PSCOMP_1:def 5;
end;
theorem Th13:
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
proof
reconsider rj=proj2 as Function of (TOP-REAL 2),R^1 by TOPMETR:17;
let P be non empty Subset of TOP-REAL 2, f be Function of I[01], (TOP-REAL 2
)|P;
assume
A1: f is continuous;
reconsider f1=f as Function;
set h=(proj2|P)*f;
A2: [#]((TOP-REAL 2)|P)=P by PRE_TOPC:def 5;
then
A3: rng f1 c= P by RELAT_1:def 19;
rj is continuous by Th11;
then rj|((TOP-REAL 2)|P) is continuous Function of ((TOP-REAL 2)|P),R^1;
then rj|P is continuous Function of ((TOP-REAL 2)|P),R^1 by A2,TMAP_1:def 3;
then reconsider h2=h as continuous Function of I[01],R^1 by A1,Lm1;
take h2;
thus h2 is continuous;
let r be Real,q be Point of TOP-REAL 2;
assume that
A4: r in the carrier of I[01] and
A5: q= f.r;
A6: dom proj2=the carrier of TOP-REAL 2 by FUNCT_2:def 1;
A7: r in dom f1 by A4,FUNCT_2:def 1;
then f1.r in rng f1 by FUNCT_1:def 3;
then
A8: q in dom proj2 /\ P by A5,A3,A6,XBOOLE_0:def 4;
thus h2.r = (proj2|P).q by A5,A7,FUNCT_1:13
.= proj2.q by A8,FUNCT_1:48
.= q`2 by PSCOMP_1:def 6;
end;
theorem Th14:
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)
proof
let P be non empty Subset of TOP-REAL 2;
assume
A1: P is being_simple_closed_curve;
now
A2: [.0,1.] = ].0,1.[ \/ {0,1} by XXREAL_1:128;
given r0 such that
A3: for p st p in P holds p`2=r0;
consider p1,p2 being Point of TOP-REAL 2, P1,P2 being non empty Subset of
TOP-REAL 2 such that
A4: p1 <> 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<r2 & r2<1 and
A25: g2.r2=(p1`1+p2`1)/2 by A18,A22,A14,Th9;
A26: [.0,1.] = {r3 : 0<=r3 & r3<=1 } by RCOMP_1:def 1;
then
A27: r2 in the carrier of I[01] by A24,BORSUK_1:40;
dom f2=the carrier of I[01] by FUNCT_2:def 1;
then
A28: f2.r2 in rng f2 by A27,FUNCT_1:def 3;
then
A29: f2.r2 in P by A9,A20,XBOOLE_0:def 3;
f2.r2 in P2 by A28,A20;
then reconsider p4=f2.r2 as Point of (TOP-REAL 2);
A30: [#]((TOP-REAL 2)|P1) = P1 by PRE_TOPC:def 5;
consider f1 being Function of I[01], (TOP-REAL 2)|P1 such that
A31: f1 is being_homeomorphism and
A32: f1.0 = p1 and
A33: f1.1 = p2 by A7,TOPREAL1:def 1;
f1 is continuous by A31,TOPS_2:def 5;
then consider g1 being Function of I[01],R^1 such that
A34: g1 is continuous and
A35: for r,q1 st r in the carrier of I[01] & q1= f1.r holds q1`1=g1.r by Th12;
A36: p2`1=g1.1 by A33,A35,A21;
p1`1=g1.0 by A32,A35,A23;
then consider r1 such that
A37: 0<r1 & r1<1 and
A38: g1.r1=(p1`1+p2`1)/2 by A34,A36,A14,Th9;
A39: r1 in the carrier of I[01] by A37,A26,BORSUK_1:40;
then r1 in dom f1 by FUNCT_2:def 1;
then
A40: f1.r1 in rng f1 by FUNCT_1:def 3;
then f1.r1 in P1 by A30;
then reconsider p3=f1.r1 as Point of (TOP-REAL 2);
f1.r1 in P by A9,A40,A30,XBOOLE_0:def 3;
then
A41: p3`2=r0 by A3
.=p4`2 by A3,A29;
p3`1= (p1`1+p2`1)/2 by A35,A38,A39
.=p4`1 by A19,A25,A27;
then f1.r1=f2.r2 by A41,TOPREAL3:6;
then
A42: f1.r1 in P1/\P2 by A40,A30,A28,A20,XBOOLE_0:def 4;
now
per cases by A10,A42,TARSKI:def 2;
case
A43: f1.r1=p1;
A44: ((1/2)*p1+(1/2)*p2)`2= ((1/2)*p1)`2+((1/2)*p2)`2 by TOPREAL3:2
.=(1/2)*(p1`2)+((1/2)*p2)`2 by TOPREAL3:4
.=(1/2)*r0+(1/2)*r0 by A11,A12,TOPREAL3:4
.=r0;
p1`1=2"*(p1`1)+ (p2`1)/2 by A35,A38,A39,A43
.=(2"*p1)`1+ 2"*(p2`1) by TOPREAL3:4
.=(2"*p1)`1+ (2"*p2)`1 by TOPREAL3:4
.=((1/2)*p1+(1/2)*p2)`1 by TOPREAL3:2;
then p1=(1/2)*p1+(1/2)*p2 by A11,A44,TOPREAL3:6;
then 1*p1-(1/2)*p1=(1/2)*p1+(1/2)*p2-(1/2)*p1 by RLVECT_1:def 8;
then 1*p1-(1/2)*p1=(1/2)*p2+((1/2)*p1-(1/2)*p1) by RLVECT_1:def 3;
then 1*p1-(1/2)*p1=(1/2)*p2+(0.TOP-REAL 2) by RLVECT_1:5;
then 1*p1-(1/2)*p1=(1/2)*p2 by RLVECT_1:4;
then (1-(1/2))*p1=(1/2)*p2 by RLVECT_1:35;
hence contradiction by A4,RLVECT_1:36;
end;
case
A45: f1.r1=p2;
A46: ((1/2)*p1+(1/2)*p2)`2= ((1/2)*p1)`2+((1/2)*p2)`2 by TOPREAL3:2
.=(1/2)*(p1`2)+((1/2)*p2)`2 by TOPREAL3:4
.=(1/2)*r0+(1/2)*r0 by A11,A12,TOPREAL3:4
.=r0;
p2`1=2"*(p1`1)+ (p2`1)/2 by A35,A38,A39,A45
.=(2"*p1)`1+ 2"*(p2`1) by TOPREAL3:4
.=(2"*p1)`1+ (2"*p2)`1 by TOPREAL3:4
.=((1/2)*p1+(1/2)*p2)`1 by TOPREAL3:2;
then p2=(1/2)*p1+(1/2)*p2 by A12,A46,TOPREAL3:6;
then 1*p2-(1/2)*p2=(1/2)*p1+(1/2)*p2-(1/2)*p2 by RLVECT_1:def 8;
then 1*p2-(1/2)*p2=(1/2)*p1+((1/2)*p2-(1/2)*p2) by RLVECT_1:def 3;
then 1*p2-(1/2)*p2=(1/2)*p1+(0.TOP-REAL 2) by RLVECT_1:5;
then 1*p2-(1/2)*p2=(1/2)*p1 by RLVECT_1:4;
then (1-(1/2))*p2=(1/2)*p1 by RLVECT_1:35;
hence contradiction by A4,RLVECT_1:36;
end;
end;
hence contradiction;
end;
hence thesis;
end;
theorem Th15:
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)
proof
let P be non empty Subset of TOP-REAL 2;
assume
A1: P is being_simple_closed_curve;
now
A2: [.0,1.] = ].0,1.[ \/ {0,1} by XXREAL_1:128;
given r0 such that
A3: for p st p in P holds p`1=r0;
consider p1,p2 being Point of TOP-REAL 2, P1,P2 being non empty Subset of
TOP-REAL 2 such that
A4: p1 <> 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<r2 & r2<1 and
A25: g2.r2=(p1`2+p2`2)/2 by A18,A22,A14,Th9;
A26: [.0,1.] = {r3 : 0<=r3 & r3<=1 } by RCOMP_1:def 1;
then
A27: r2 in the carrier of I[01] by A24,BORSUK_1:40;
dom f2=the carrier of I[01] by FUNCT_2:def 1;
then
A28: f2.r2 in rng f2 by A27,FUNCT_1:def 3;
then
A29: f2.r2 in P by A9,A20,XBOOLE_0:def 3;
f2.r2 in P2 by A28,A20;
then reconsider p4=f2.r2 as Point of (TOP-REAL 2);
A30: [#]((TOP-REAL 2)|P1) = P1 by PRE_TOPC:def 5;
consider f1 being Function of I[01], (TOP-REAL 2)|P1 such that
A31: f1 is being_homeomorphism and
A32: f1.0 = p1 and
A33: f1.1 = p2 by A7,TOPREAL1:def 1;
f1 is continuous by A31,TOPS_2:def 5;
then consider g1 being Function of I[01],R^1 such that
A34: g1 is continuous and
A35: for r,q1 st r in the carrier of I[01] & q1= f1.r holds q1`2=g1.r by Th13;
A36: p2`2=g1.1 by A33,A35,A21;
p1`2=g1.0 by A32,A35,A23;
then consider r1 such that
A37: 0<r1 & r1<1 and
A38: g1.r1=(p1`2+p2`2)/2 by A34,A36,A14,Th9;
A39: r1 in the carrier of I[01] by A37,A26,BORSUK_1:40;
then r1 in dom f1 by FUNCT_2:def 1;
then
A40: f1.r1 in rng f1 by FUNCT_1:def 3;
then f1.r1 in P1 by A30;
then reconsider p3=f1.r1 as Point of (TOP-REAL 2);
f1.r1 in P by A9,A40,A30,XBOOLE_0:def 3;
then
A41: p3`1=r0 by A3
.=p4`1 by A3,A29;
p3`2= (p1`2+p2`2)/2 by A35,A38,A39
.=p4`2 by A19,A25,A27;
then f1.r1=f2.r2 by A41,TOPREAL3:6;
then
A42: f1.r1 in P1/\P2 by A40,A30,A28,A20,XBOOLE_0:def 4;
now
per cases by A10,A42,TARSKI:def 2;
case
A43: f1.r1=p1;
A44: ((1/2)*p1+(1/2)*p2)`1= ((1/2)*p1)`1+((1/2)*p2)`1 by TOPREAL3:2
.=(1/2)*(p1`1)+((1/2)*p2)`1 by TOPREAL3:4
.=(1/2)*r0+(1/2)*r0 by A11,A12,TOPREAL3:4
.=r0;
p1`2=2"*(p1`2)+ (p2`2)/2 by A35,A38,A39,A43
.=(2"*p1)`2+ 2"*(p2`2) by TOPREAL3:4
.=(2"*p1)`2+ (2"*p2)`2 by TOPREAL3:4
.=((1/2)*p1+(1/2)*p2)`2 by TOPREAL3:2;
then p1=(1/2)*p1+(1/2)*p2 by A11,A44,TOPREAL3:6;
then 1*p1-(1/2)*p1=(1/2)*p1+(1/2)*p2-(1/2)*p1 by RLVECT_1:def 8;
then 1*p1-(1/2)*p1=(1/2)*p2+((1/2)*p1-(1/2)*p1) by RLVECT_1:def 3;
then 1*p1-(1/2)*p1=(1/2)*p2+(0.TOP-REAL 2) by RLVECT_1:5;
then 1*p1-(1/2)*p1=(1/2)*p2 by RLVECT_1:4;
then (1-(1/2))*p1=(1/2)*p2 by RLVECT_1:35;
hence contradiction by A4,RLVECT_1:36;
end;
case
A45: f1.r1=p2;
A46: ((1/2)*p1+(1/2)*p2)`1= ((1/2)*p1)`1+((1/2)*p2)`1 by TOPREAL3:2
.=(1/2)*(p1`1)+((1/2)*p2)`1 by TOPREAL3:4
.=(1/2)*r0+(1/2)*r0 by A11,A12,TOPREAL3:4
.=r0;
p2`2=2"*(p1`2)+ (p2`2)/2 by A35,A38,A39,A45
.=(2"*p1)`2+ 2"*(p2`2) by TOPREAL3:4
.=(2"*p1)`2+ (2"*p2)`2 by TOPREAL3:4
.=((1/2)*p1+(1/2)*p2)`2 by TOPREAL3:2;
then p2=(1/2)*p1+(1/2)*p2 by A12,A46,TOPREAL3:6;
then 1*p2-(1/2)*p2=(1/2)*p1+(1/2)*p2-(1/2)*p2 by RLVECT_1:def 8;
then 1*p2-(1/2)*p2=(1/2)*p1+((1/2)*p2-(1/2)*p2) by RLVECT_1:def 3;
then 1*p2-(1/2)*p2=(1/2)*p1+(0.TOP-REAL 2) by RLVECT_1:5;
then 1*p2-(1/2)*p2=(1/2)*p1 by RLVECT_1:4;
then (1-(1/2))*p2=(1/2)*p1 by RLVECT_1:35;
hence contradiction by A4,RLVECT_1:36;
end;
end;
hence contradiction;
end;
hence thesis;
end;
theorem Th16:
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)
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;