:: A Decomposition of Simple Closed Curves and an Order of Their Points
:: by Yatsuka Nakamura and Andrzej Trybulec
::
:: Received December 19, 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, REAL_1, SUBSET_1, PRE_TOPC, EUCLID, XXREAL_0, ARYTM_3,
XBOOLE_0, RELAT_1, RCOMP_1, FUNCT_1, ORDINAL2, STRUCT_0, MCART_1,
FINSEQ_1, TARSKI, PARTFUN1, TOPREAL1, RELAT_2, BORSUK_1, TOPS_2, CARD_1,
TOPMETR, XXREAL_1, JORDAN5C, JORDAN3, ARYTM_1, TREAL_1, VALUED_1,
TOPREAL2, PSCOMP_1, XXREAL_2, SEQ_4, METRIC_1, COMPLEX1, RLTOPSP1,
JORDAN6, FUNCT_2, NAT_1;
notations TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, XXREAL_0,
XXREAL_2, XREAL_0, COMPLEX1, REAL_1, RCOMP_1, FUNCT_1, RELSET_1,
PARTFUN1, FUNCT_2, BINOP_1, FINSEQ_1, STRUCT_0, TOPREAL1, TOPREAL2,
CONNSP_1, TSEP_1, TOPMETR, PRE_TOPC, TOPS_2, COMPTS_1, BORSUK_1, EUCLID,
RLTOPSP1, METRIC_1, SEQ_4, JORDAN5C, TREAL_1, PSCOMP_1;
constructors REAL_1, COMPLEX1, RCOMP_1, CONNSP_1, TOPS_2, COMPTS_1, TSEP_1,
TOPREAL1, TOPREAL2, TREAL_1, PSCOMP_1, JORDAN5C, SEQ_4, MONOID_0,
BINOP_2, PCOMPS_1, BINOP_1, NUMBERS;
registrations RELSET_1, FUNCT_2, XXREAL_0, XREAL_0, MEMBERED, STRUCT_0,
PRE_TOPC, COMPTS_1, METRIC_1, BORSUK_1, TSEP_1, EUCLID, TOPMETR,
TOPREAL1, TOPREAL2, BORSUK_2, MONOID_0, JORDAN2B, MEASURE6, BINOP_2,
VALUED_0, ORDINAL1;
requirements REAL, NUMERALS, BOOLE, SUBSET, ARITHM;
definitions TARSKI, PRE_TOPC, JORDAN5C, XBOOLE_0, XXREAL_2;
equalities XBOOLE_0, PSCOMP_1, STRUCT_0;
expansions TARSKI, PRE_TOPC, JORDAN5C, XBOOLE_0, XXREAL_2;
theorems TARSKI, RCOMP_1, TOPMETR, TOPS_1, METRIC_1, FUNCT_1, FUNCT_2,
FINSEQ_1, ABSVALUE, PRE_TOPC, TOPS_2, JORDAN1, JORDAN5B, JORDAN5C,
TOPREAL1, TOPREAL5, SUBSET_1, TREAL_1, PSCOMP_1, RELAT_1, TOPREAL2,
JORDAN2B, ENUMSET1, TOPREAL3, JORDAN5A, BORSUK_1, COMPTS_1, CONNSP_1,
ZFMISC_1, TSEP_1, SEQ_4, RELSET_1, XREAL_0, SPRECT_1, XBOOLE_0, XBOOLE_1,
XREAL_1, EUCLID, GOBOARD7, XXREAL_0, XXREAL_1, XXREAL_2;
schemes DOMAIN_1;
begin :: Middle Points of Arcs
reserve x,y for set;
reserve s,r for Real;
reserve r1,r2 for Real;
reserve n for Nat;
reserve p,q,q1,q2 for Point of TOP-REAL 2;
theorem Th1:
r<=s implies r <= (r+s)/2 & (r+s)/2 <= s
proof
assume
A1: r<=s;
per cases by A1,XXREAL_0:1;
suppose r<s;
hence thesis by XREAL_1:226;
end;
suppose r=s;
hence thesis;
end;
end;
theorem Th2:
for TX being non empty TopSpace, P being Subset of TX,
A being Subset of TX|P, B being Subset of TX
st B is closed & A=B/\P holds A is closed
proof
let TX be non empty TopSpace,P be Subset of TX, A be Subset of TX|P,
B be Subset of TX;
assume that
A1: B is closed and
A2: A=B/\P;
[#](TX|P)=P by PRE_TOPC:def 5;
hence thesis by A1,A2,PRE_TOPC:13;
end;
theorem Th3:
for TX,TY being non empty TopSpace,
P being non empty Subset of TY,f being Function of TX,TY|P
holds f is Function of TX,TY & for f2 being Function of TX,TY
st f2=f & f is continuous holds f2 is continuous
proof
let TX,TY be non empty TopSpace,
P be non empty Subset of TY,f be Function of TX,TY|P;
A1: the carrier of TY|P = [#](TY|P) .=P by PRE_TOPC:def 5;
hence f is Function of TX,TY by FUNCT_2:7;
let f2 be Function of TX,TY such that
A2: f2=f and
A3: f is continuous;
let P1 be Subset of TY;
assume
A4: P1 is closed;
reconsider P3=P1/\P as Subset of TY|P by TOPS_2:29;
A5: P3 is closed by A4,Th2;
f2"P=the carrier of TX by A1,A2,FUNCT_2:40
.=dom f2 by FUNCT_2:def 1;
then f2"P1=f2"P1 /\ f2"P by RELAT_1:132,XBOOLE_1:28
.=f"P3 by A2,FUNCT_1:68;
hence thesis by A3,A5;
end;
theorem Th4:
for r being Real, P being Subset of TOP-REAL 2
st P={p where p is Point of TOP-REAL 2: p`1>=r} holds P is closed
proof
let r be Real,P be Subset of TOP-REAL 2;
assume
A1: P={p where p is Point of TOP-REAL 2: p`1>=r};
A2: 1 in Seg 2 by FINSEQ_1:1;
A3: P` c= {p where p is Point of TOP-REAL 2: p`1<r}
proof
let x be object;
assume
A4: x in P`;
then x in (the carrier of (TOP-REAL 2)) \ P by SUBSET_1:def 4;
then
A5: not x in P by XBOOLE_0:def 5;
reconsider q=x as Point of TOP-REAL 2 by A4;
q`1<r by A1,A5;
hence thesis;
end;
{p where p is Point of TOP-REAL 2: p`1<r} c= P`
proof
let x be object;
assume x in {p where p is Point of TOP-REAL 2: p`1<r};
then
A6: ex p being Point of TOP-REAL 2 st ( p=x)&( p`1<r);
now
assume x in {q where q is Point of TOP-REAL 2: q`1>=r};
then ex q being Point of TOP-REAL 2 st ( q=x)&( q`1>=r);
hence contradiction by A6;
end;
then x in (the carrier of TOP-REAL 2) \P by A1,A6,XBOOLE_0:def 5;
hence thesis by SUBSET_1:def 4;
end;
then
A7: P`={p where p is Point of TOP-REAL 2: p`1<r} by A3;
A8: P`c= {p where p is Point of TOP-REAL 2: r>p/.1}
proof
let x be object;
assume x in P`;
then consider p being Point of TOP-REAL 2 such that
A9: p=x and
A10: p`1<r by A7;
p/.1<r by A10,JORDAN2B:29;
hence thesis by A9;
end;
{p where p is Point of TOP-REAL 2: r>p/.1} c= P`
proof
let x be object;
assume x in {p where p is Point of TOP-REAL 2: r>p/.1};
then consider q being Point of TOP-REAL 2 such that
A11: q=x and
A12: r>q/.1;
q`1<r by A12,JORDAN2B:29;
hence thesis by A7,A11;
end;
then
A13: P`={p where p is Point of TOP-REAL 2: r>p/.1} by A8;
reconsider P1 = P` as Subset of TOP-REAL 2;
P1 is open by A2,A13,JORDAN2B:12;
hence thesis by TOPS_1:3;
end;
theorem Th5:
for r being Real, P being Subset of TOP-REAL 2
st P={p where p is Point of TOP-REAL 2: p`1<=r} holds P is closed
proof
let r be Real, P be Subset of TOP-REAL 2;
assume
A1: P={p where p is Point of TOP-REAL 2: p`1<=r};
A2: 1 in Seg 2 by FINSEQ_1:1;
A3: P` c= {p where p is Point of TOP-REAL 2: p`1>r}
proof
let x be object;
assume
A4: x in P`;
then x in (the carrier of (TOP-REAL 2)) \ P by SUBSET_1:def 4;
then
A5: not x in P by XBOOLE_0:def 5;
reconsider q=x as Point of TOP-REAL 2 by A4;
q`1>r by A1,A5;
hence thesis;
end;
{p where p is Point of TOP-REAL 2: p`1>r} c= P`
proof
let x be object;
assume x in {p where p is Point of TOP-REAL 2: p`1>r};
then
A6: ex p being Point of TOP-REAL 2 st ( p=x)&( p`1>r);
now
assume x in {q where q is Point of TOP-REAL 2: q`1<=r};
then ex q being Point of TOP-REAL 2 st ( q=x)&( q`1<=r);
hence contradiction by A6;
end;
then x in (the carrier of TOP-REAL 2) \P by A1,A6,XBOOLE_0:def 5;
hence thesis by SUBSET_1:def 4;
end;
then
A7: P`={p where p is Point of TOP-REAL 2: p`1>r} by A3;
A8: P`c= {p where p is Point of TOP-REAL 2: r<p/.1}
proof
let x be object;
assume x in P`;
then consider p being Point of TOP-REAL 2 such that
A9: p=x and
A10: p`1>r by A7;
p/.1>r by A10,JORDAN2B:29;
hence thesis by A9;
end;
{p where p is Point of TOP-REAL 2: r<p/.1} c= P`
proof
let x be object;
assume x in {p where p is Point of TOP-REAL 2: r<p/.1};
then consider q being Point of TOP-REAL 2 such that
A11: q=x and
A12: r<q/.1;
q`1>r by A12,JORDAN2B:29;
hence thesis by A7,A11;
end;
then
A13: P`={p where p is Point of TOP-REAL 2: r<p/.1} by A8;
reconsider P1 = P` as Subset of TOP-REAL 2;
P1 is open by A2,A13,JORDAN2B:13;
hence thesis by TOPS_1:3;
end;
theorem Th6:
for r being Real,P being Subset of TOP-REAL 2
st P={p where p is Point of TOP-REAL 2: p`1=r} holds P is closed
proof
let r be Real,P be Subset of TOP-REAL 2;
assume
A1: P={p where p is Point of TOP-REAL 2: p`1=r};
defpred P[Point of TOP-REAL 2] means $1`1>=r;
{p where p is Element of TOP-REAL 2 : P[p]}
is Subset of TOP-REAL 2 from DOMAIN_1:sch 7;
then reconsider P1={p where p is Point of TOP-REAL 2: p`1>=r}
as Subset of TOP-REAL 2;
A2: P1 is closed by Th4;
defpred Q[Point of TOP-REAL 2] means $1`1<=r;
{p where p is Element of TOP-REAL 2 : Q[p]}
is Subset of TOP-REAL 2 from DOMAIN_1:sch 7;
then reconsider P2={p where p is Point of TOP-REAL 2: p`1<=r}
as Subset of TOP-REAL 2;
A3: P2 is closed by Th5;
A4: P c= P1 /\ P2
proof
let x be object;
assume x in P;
then
A5: ex p being Point of TOP-REAL 2 st p=x & p`1=r by A1;
then
A6: x in P1;
x in P2 by A5;
hence thesis by A6,XBOOLE_0:def 4;
end;
P1 /\ P2 c= P
proof
let x be object;
assume
A7: x in P1 /\ P2;
then
A8: x in P1 by XBOOLE_0:def 4;
A9: x in P2 by A7,XBOOLE_0:def 4;
consider q1 being Point of TOP-REAL 2 such that
A10: q1=x and
A11: q1`1>=r by A8;
ex q2 being Point of TOP-REAL 2 st ( q2=x)&( q2`1<=r) by A9;
then q1`1=r by A10,A11,XXREAL_0:1;
hence thesis by A1,A10;
end;
then P=P1 /\ P2 by A4;
hence thesis by A2,A3,TOPS_1:8;
end;
theorem Th7:
for r being Real, P being Subset of TOP-REAL 2
st P={p where p is Point of TOP-REAL 2: p`2>=r} holds P is closed
proof
let r be Real, P be Subset of TOP-REAL 2;
assume
A1: P={p where p is Point of TOP-REAL 2: p`2>=r};
A2: 2 in Seg 2 by FINSEQ_1:1;
A3: P` c= {p where p is Point of TOP-REAL 2: p`2<r}
proof
let x be object;
assume
A4: x in P`;
then x in (the carrier of (TOP-REAL 2)) \ P by SUBSET_1:def 4;
then
A5: not x in P by XBOOLE_0:def 5;
reconsider q=x as Point of TOP-REAL 2 by A4;
q`2<r by A1,A5;
hence thesis;
end;
{p where p is Point of TOP-REAL 2: p`2<r} c= P`
proof
let x be object;
assume x in {p where p is Point of TOP-REAL 2: p`2<r};
then
A6: ex p being Point of TOP-REAL 2 st ( p=x)&( p`2<r);
now
assume x in {q where q is Point of TOP-REAL 2: q`2>=r};
then ex q being Point of TOP-REAL 2 st ( q=x)&( q`2>=r);
hence contradiction by A6;
end;
then x in (the carrier of TOP-REAL 2) \P by A1,A6,XBOOLE_0:def 5;
hence thesis by SUBSET_1:def 4;
end;
then
A7: P`={p where p is Point of TOP-REAL 2: p`2<r} by A3;
A8: P`c= {p where p is Point of TOP-REAL 2: r>p/.2}
proof
let x be object;
assume x in P`;
then consider p being Point of TOP-REAL 2 such that
A9: p=x and
A10: p`2<r by A7;
p/.2<r by A10,JORDAN2B:29;
hence thesis by A9;
end;
{p where p is Point of TOP-REAL 2: r>p/.2} c= P`
proof
let x be object;
assume x in {p where p is Point of TOP-REAL 2: r>p/.2};
then consider q being Point of TOP-REAL 2 such that
A11: q=x and
A12: r>q/.2;
q`2<r by A12,JORDAN2B:29;
hence thesis by A7,A11;
end;
then
A13: P`={p where p is Point of TOP-REAL 2: r>p/.2} by A8;
reconsider P1 = P` as Subset of TOP-REAL 2;
P1 is open by A2,A13,JORDAN2B:12;
hence thesis by TOPS_1:3;
end;
theorem Th8:
for r being Real, P being Subset of TOP-REAL 2
st P={p where p is Point of TOP-REAL 2: p`2<=r} holds P is closed
proof
let r be Real, P be Subset of TOP-REAL 2;
assume
A1: P={p where p is Point of TOP-REAL 2: p`2<=r};
A2: 2 in Seg 2 by FINSEQ_1:1;
A3: P` c= {p where p is Point of TOP-REAL 2: p`2>r}
proof
let x be object;
assume
A4: x in P`;
then x in (the carrier of (TOP-REAL 2)) \ P by SUBSET_1:def 4;
then
A5: not x in P by XBOOLE_0:def 5;
reconsider q=x as Point of TOP-REAL 2 by A4;
q`2>r by A1,A5;
hence thesis;
end;
{p where p is Point of TOP-REAL 2: p`2>r} c= P`
proof
let x be object;
assume x in {p where p is Point of TOP-REAL 2: p`2>r};
then
A6: ex p being Point of TOP-REAL 2 st ( p=x)&( p`2>r);
now
assume x in {q where q is Point of TOP-REAL 2: q`2<=r};
then ex q being Point of TOP-REAL 2 st ( q=x)&( q`2<=r);
hence contradiction by A6;
end;
then x in (the carrier of TOP-REAL 2) \P by A1,A6,XBOOLE_0:def 5;
hence thesis by SUBSET_1:def 4;
end;
then
A7: P`={p where p is Point of TOP-REAL 2: p`2>r} by A3;
A8: P`c= {p where p is Point of TOP-REAL 2: r<p/.2}
proof
let x be object;
assume x in P`;
then consider p being Point of TOP-REAL 2 such that
A9: p=x and
A10: p`2>r by A7;
p/.2>r by A10,JORDAN2B:29;
hence thesis by A9;
end;
{p where p is Point of TOP-REAL 2: r<p/.2} c= P`
proof
let x be object;
assume x in {p where p is Point of TOP-REAL 2: r<p/.2};
then consider q being Point of TOP-REAL 2 such that
A11: q=x and
A12: r<q/.2;
q`2>r by A12,JORDAN2B:29;
hence thesis by A7,A11;
end;
then
A13: P`={p where p is Point of TOP-REAL 2: r<p/.2} by A8;
reconsider P1 = P` as Subset of TOP-REAL 2;
P1 is open by A2,A13,JORDAN2B:13;
hence thesis by TOPS_1:3;
end;
theorem Th9:
for r being Real, P being Subset of TOP-REAL 2
st P={p where p is Point of TOP-REAL 2: p`2=r} holds P is closed
proof
let r be Real, P be Subset of TOP-REAL 2;
assume
A1: P={p where p is Point of TOP-REAL 2: p`2=r};
defpred P[Point of TOP-REAL 2] means $1`2>=r;
{p where p is Element of TOP-REAL 2 : P[p]}
is Subset of TOP-REAL 2 from DOMAIN_1:sch 7;
then reconsider P1={p where p is Point of TOP-REAL 2: p`2>=r}
as Subset of TOP-REAL 2;
A2: P1 is closed by Th7;
defpred Q[Point of TOP-REAL 2] means $1`2<=r;
{p where p is Element of TOP-REAL 2 : Q[p]}
is Subset of TOP-REAL 2 from DOMAIN_1:sch 7;
then reconsider P2={p where p is Point of TOP-REAL 2: p`2<=r}
as Subset of TOP-REAL 2;
A3: P2 is closed by Th8;
A4: P c= P1 /\ P2
proof
let x be object;
assume x in P;
then
A5: ex p being Point of TOP-REAL 2 st ( p=x)&( p`2=r) by A1;
then
A6: x in P1;
x in P2 by A5;
hence thesis by A6,XBOOLE_0:def 4;
end;
P1 /\ P2 c= P
proof
let x be object;
assume
A7: x in P1 /\ P2;
then
A8: x in P1 by XBOOLE_0:def 4;
A9: x in P2 by A7,XBOOLE_0:def 4;
consider q1 being Point of TOP-REAL 2 such that
A10: q1=x and
A11: q1`2>=r by A8;
ex q2 being Point of TOP-REAL 2 st ( q2=x)&( q2`2<=r) by A9;
then q1`2=r by A10,A11,XXREAL_0:1;
hence thesis by A1,A10;
end;
then P=P1 /\ P2 by A4;
hence thesis by A2,A3,TOPS_1:8;
end;
theorem Th10:
for P being Subset of TOP-REAL n, p1,p2 being Point of TOP-REAL n st
P is_an_arc_of p1,p2 holds P is connected
proof
let P be Subset of TOP-REAL n, p1,p2 be Point of TOP-REAL n;
assume
A1: P is_an_arc_of p1,p2;
then consider f being Function of I[01], (TOP-REAL n)|P such that
A2: f is being_homeomorphism and f.0 = p1
and f.1 = p2 by TOPREAL1:def 1;
reconsider P9 = P as non empty Subset of TOP-REAL n by A1,TOPREAL1:1;
A3: f is continuous Function of I[01],(TOP-REAL n)|P9 by A2,TOPS_2:def 5;
A4: [#]I[01] is connected by CONNSP_1:27,TREAL_1:19;
A5: rng f=[#]((TOP-REAL n)|P) by A2,TOPS_2:def 5;
A6: [#]((TOP-REAL n)|P)=P by PRE_TOPC:def 5;
dom f=[#]I[01] by A2,TOPS_2:def 5;
then
A7: P=f.:([#]I[01]) by A5,A6,RELAT_1:113;
f.:([#]I[01]) is connected by A3,A4,TOPS_2:61;
hence thesis by A7,CONNSP_1:23;
end;
theorem
for P being Subset of TOP-REAL 2,p1,p2
being Point of TOP-REAL 2 st P is_an_arc_of p1,p2 holds P is closed
by COMPTS_1:7,JORDAN5A:1;
theorem Th12:
for P being Subset of TOP-REAL 2,
p1,p2 being Point of TOP-REAL 2 st P is_an_arc_of p1,p2
ex q being Point of TOP-REAL 2 st q in P & q`1 = (p1`1+p2`1)/2
proof
let P be Subset of (TOP-REAL 2), p1,p2 be Point of TOP-REAL 2;
assume
A1: P is_an_arc_of p1,p2;
then
A2: p1 in P by TOPREAL1:1;
reconsider P9 = P as non empty Subset of TOP-REAL 2 by A1,TOPREAL1:1;
consider f being Function of I[01], (TOP-REAL 2)|P9 such that
A3: f is being_homeomorphism and
A4: f.0 = p1 and
A5: f.1 = p2 by A1,TOPREAL1:def 1;
A6: f is continuous by A3,TOPS_2:def 5;
consider h being Function of TOP-REAL 2,R^1 such that
A7: for p being Element of TOP-REAL 2 holds h.p=p/.1 by JORDAN2B:1;
1 in Seg 2 by FINSEQ_1:1;
then
A8: h is continuous by A7,JORDAN2B:18;
A9: the carrier of (TOP-REAL 2)|P = [#]((TOP-REAL 2)|P)
.=P9 by PRE_TOPC:def 5;
then
A10: f is Function of the carrier of I[01],the carrier of TOP-REAL 2
by FUNCT_2:7;
reconsider f1=f as Function of I[01],TOP-REAL 2 by A9,FUNCT_2:7;
A11: f1 is continuous by A6,Th3;
reconsider g= h*f as Function of I[01],R^1 by A10;
A12: dom f=[.0,1.] by BORSUK_1:40,FUNCT_2:def 1;
then
A13: 0 in dom f by XXREAL_1:1;
A14: 1 in dom f by A12,XXREAL_1:1;
A15: g.0 =h.(f.0) by A13,FUNCT_1:13
.=p1/.1 by A4,A7
.=p1`1 by JORDAN2B:29;
A16: g.1 =h.(f.1) by A14,FUNCT_1:13
.=p2/.1 by A5,A7
.=p2`1 by JORDAN2B:29;
per cases;
suppose g.0<>g.1;
then consider r1 being Real such that
A17: 0<r1 and
A18: r1<1 and
A19: g.r1=(p1`1+p2`1)/2 by A8,A11,A15,A16,TOPREAL5:9;
A20: r1 in [.0,1.] by A17,A18,XXREAL_1:1;
A21: r1 in the carrier of I[01] by A17,A18,BORSUK_1:40,XXREAL_1:1;
then reconsider q1=f.r1 as Point of TOP-REAL 2 by A10,FUNCT_2:5;
g.r1= h.(f.r1) by A12,A20,FUNCT_1:13
.=q1/.1 by A7
.=q1`1 by JORDAN2B:29;
hence thesis by A9,A19,A21,FUNCT_2:5;
end;
suppose g.0=g.1;
hence thesis by A2,A15,A16;
end;
end;
theorem Th13:
for P,Q being Subset of TOP-REAL 2,
p1,p2 being Point of TOP-REAL 2 st P is_an_arc_of p1,p2 &
Q={q:q`1=(p1`1+p2`1)/2} holds P meets Q & P /\ Q is closed
proof
let P,Q be Subset of TOP-REAL 2, p1,p2 be Point of TOP-REAL 2;
reconsider W = P as Subset of TOP-REAL 2;
assume
A1: P is_an_arc_of p1,p2 & Q={q:q`1=(p1`1+p2`1)/2};
consider f being Function of TOP-REAL 2,R^1 such that
A2: for p being Element of TOP-REAL 2 holds f.p=p/.1 by JORDAN2B:1;
reconsider P9 = P as non empty Subset of TOP-REAL 2 by A1,TOPREAL1:1;
A3: 1 in Seg 2 by FINSEQ_1:1;
A4: dom f=the carrier of TOP-REAL 2 by FUNCT_2:def 1;
A5: [#]((TOP-REAL 2)|P)=P by PRE_TOPC:def 5;
then
A6: the carrier of (TOP-REAL 2)|P9=P9;
A7: dom (f|P)=(the carrier of TOP-REAL 2)/\P by A4,RELAT_1:61
.=P by XBOOLE_1:28;
rng (f|P) c= the carrier of R^1 by RELAT_1:def 19;
then reconsider g=f|P as Function
of (TOP-REAL 2)|P,R^1 by A5,A7,FUNCT_2:def 1,RELSET_1:4;
reconsider g as continuous Function of (TOP-REAL 2)|P9,R^1 by A2,A3,
JORDAN2B:18,TOPMETR:7;
A8: p1 in P by A1,TOPREAL1:1;
A9: p2 in P by A1,TOPREAL1:1;
reconsider p19=p1, p29=p2 as Point of (TOP-REAL 2)|P by A1,A5,TOPREAL1:1;
A10: g.p19=f.p1 by A8,FUNCT_1:49
.=p1/.1 by A2
.=p1`1 by JORDAN2B:29;
A11: g.p29=f.p2 by A9,FUNCT_1:49
.=p2/.1 by A2
.=p2`1 by JORDAN2B:29;
W is connected by A1,Th10;
then
A12: (TOP-REAL 2)|P is connected by CONNSP_1:def 3;
A13: now per cases;
case
A14: p1`1<=p2`1;
then
A15: p1`1<=(p1`1+p2`1)/2 by Th1;
(p1`1+p2`1)/2<=p2`1 by A14,Th1;
then consider xc being Point of (TOP-REAL 2)|P such that
A16: g.xc=(p1`1+p2`1)/2 by A10,A11,A12,A15,TOPREAL5:4;
xc in P by A6;
then reconsider pc=xc as Point of TOP-REAL 2;
g.xc =f.xc by A5,FUNCT_1:49
.=pc/.1 by A2
.=pc`1 by JORDAN2B:29;
then xc in Q by A1,A16;
hence P meets Q by A6,XBOOLE_0:3;
end;
case
A17: p1`1>p2`1;
then
A18: p2`1<=(p1`1+p2`1)/2 by Th1;
(p1`1+p2`1)/2<=p1`1 by A17,Th1;
then consider xc being Point of (TOP-REAL 2)|P such that
A19: g.xc=(p1`1+p2`1)/2 by A10,A11,A12,A18,TOPREAL5:4;
xc in P by A6;
then reconsider pc=xc as Point of TOP-REAL 2;
g.xc =f.xc by A5,FUNCT_1:49
.=pc/.1 by A2
.=pc`1 by JORDAN2B:29;
then xc in Q by A1,A19;
hence P meets Q by A6,XBOOLE_0:3;
end;
end;
reconsider P1 = P, Q1 = Q as Subset of TOP-REAL 2;
A20: P1 is closed by A1,COMPTS_1:7,JORDAN5A:1;
Q1 is closed by A1,Th6;
hence thesis by A13,A20,TOPS_1:8;
end;
theorem Th14:
for P,Q being Subset of TOP-REAL 2,
p1,p2 being Point of TOP-REAL 2 st P is_an_arc_of p1,p2 &
Q={q:q`2=(p1`2+p2`2)/2} holds P meets Q & P /\ Q is closed
proof
let P,Q1 be Subset of TOP-REAL 2, p1,p2 be Point of TOP-REAL 2;
assume
A1: P is_an_arc_of p1,p2 & Q1={q:q`2=(p1`2+p2`2)/2};
consider f being Function of TOP-REAL 2,R^1 such that
A2: for p being Element of TOP-REAL 2 holds f.p=p/.2 by JORDAN2B:1;
reconsider P9 = P as non empty Subset of TOP-REAL 2 by A1,TOPREAL1:1;
A3: 2 in Seg 2 by FINSEQ_1:1;
A4: dom f=the carrier of TOP-REAL 2 by FUNCT_2:def 1;
A5: [#]((TOP-REAL 2)|P)=P by PRE_TOPC:def 5;
then
A6: the carrier of (TOP-REAL 2)|P9=P9;
A7: dom (f|P)=(the carrier of TOP-REAL 2)/\P by A4,RELAT_1:61
.=P by XBOOLE_1:28;
rng (f|P) c= the carrier of R^1 by RELAT_1:def 19;
then reconsider g=f|P as Function
of (TOP-REAL 2)|P,R^1 by A5,A7,FUNCT_2:def 1,RELSET_1:4;
reconsider g as continuous Function of (TOP-REAL 2)|P9,R^1 by A2,A3,
JORDAN2B:18,TOPMETR:7;
A8: p1 in P by A1,TOPREAL1:1;
A9: p2 in P by A1,TOPREAL1:1;
reconsider p19=p1, p29=p2 as Point of (TOP-REAL 2)|P by A1,A5,TOPREAL1:1;
A10: g.p19=f.p1 by A8,FUNCT_1:49
.=p1/.2 by A2
.=p1`2 by JORDAN2B:29;
A11: g.p29=f.p2 by A9,FUNCT_1:49
.=p2/.2 by A2
.=p2`2 by JORDAN2B:29;
reconsider W = P as Subset of TOP-REAL 2;
W is connected by A1,Th10;
then
A12: (TOP-REAL 2)|P is connected by CONNSP_1:def 3;
A13: now per cases;
case
A14: p1`2<=p2`2;
then
A15: p1`2<=(p1`2+p2`2)/2 by Th1;
(p1`2+p2`2)/2<=p2`2 by A14,Th1;
then consider xc being Point of (TOP-REAL 2)|P such that
A16: g.xc=(p1`2+p2`2)/2 by A10,A11,A12,A15,TOPREAL5:4;
xc in P by A6;
then reconsider pc=xc as Point of TOP-REAL 2;
g.xc =f.xc by A5,FUNCT_1:49
.=pc/.2 by A2
.=pc`2 by JORDAN2B:29;
then xc in Q1 by A1,A16;
hence P meets Q1 by A6,XBOOLE_0:3;
end;
case
A17: p1`2>p2`2;
then
A18: p2`2<=(p1`2+p2`2)/2 by Th1;
(p1`2+p2`2)/2<=p1`2 by A17,Th1;
then consider xc being Point of (TOP-REAL 2)|P such that
A19: g.xc=(p1`2+p2`2)/2 by A10,A11,A12,A18,TOPREAL5:4;
xc in P by A6;
then reconsider pc=xc as Point of TOP-REAL 2;
g.xc =f.xc by A5,FUNCT_1:49
.=pc/.2 by A2
.=pc`2 by JORDAN2B:29;
then xc in Q1 by A1,A19;
hence P meets Q1 by A6,XBOOLE_0:3;
end;
end;
reconsider P1 = P, Q2 = Q1 as Subset of TOP-REAL 2;
A20: P1 is closed by A1,COMPTS_1:7,JORDAN5A:1;
Q2 is closed by A1,Th9;
hence thesis by A13,A20,TOPS_1:8;
end;
definition
let P be Subset of TOP-REAL 2, p1,p2 be Point of TOP-REAL 2;
func x_Middle(P,p1,p2) -> Point of TOP-REAL 2 means
:Def1:
for Q being Subset of TOP-REAL 2 st Q={q:q`1=(p1`1+p2`1)/2}
holds it=First_Point(P,p1,p2,Q);
existence
proof
{q:q`1=(p1`1+p2`1)/2} c= the carrier of TOP-REAL 2
proof
let x be object;
assume x in {q:q`1=(p1`1+p2`1)/2};
then ex q being Point of TOP-REAL 2 st ( q=x)&( q`1=(p1`1+p2`1)/2 );
hence thesis;
end;
then reconsider Q1={q:q`1=(p1`1+p2`1)/2} as Subset of TOP-REAL 2;
reconsider q2=First_Point(P,p1,p2,Q1) as Point of TOP-REAL 2;
for Q being Subset of TOP-REAL 2 st Q={q:q`1=(p1`1+p2`1)/2}
holds q2=First_Point(P,p1,p2,Q);
hence thesis;
end;
uniqueness
proof
let q3,q4 be Point of TOP-REAL 2;
assume
A1: (for Q1 being Subset of TOP-REAL 2 st Q1={q1:q1`1=(p1`1+p2`1)/2}
holds q3=First_Point(P,p1,p2,Q1)) & for Q2 being Subset of TOP-REAL 2 st
Q2={q2:q2`1=(p1`1+p2`1)/2} holds q4=First_Point(P,p1,p2,Q2);
{q1:q1`1=(p1`1+p2`1)/2} c= the carrier of TOP-REAL 2
proof
let x be object;
assume x in {q1:q1`1=(p1`1+p2`1)/2};
then ex q being Point of TOP-REAL 2 st ( q=x)&( q`1=(p1`1+p2`1)/2 );
hence thesis;
end;
then reconsider Q3={q2:q2`1=(p1`1+p2`1)/2} as Subset of TOP-REAL 2;
q3=First_Point(P,p1,p2,Q3) by A1;
hence thesis by A1;
end;
end;
definition
let P be Subset of TOP-REAL 2, p1,p2 be Point of TOP-REAL 2;
func y_Middle(P,p1,p2) -> Point of TOP-REAL 2 means
:Def2:
for Q being Subset of TOP-REAL 2 st Q={q:q`2=(p1`2+p2`2)/2}
holds it=First_Point(P,p1,p2,Q);
existence
proof
{q:q`2=(p1`2+p2`2)/2} c= the carrier of TOP-REAL 2
proof
let x be object;
assume x in {q:q`2=(p1`2+p2`2)/2};
then ex q being Point of TOP-REAL 2 st ( q=x)&( q`2=(p1`2+p2`2)/2 );
hence thesis;
end;
then reconsider Q1={q:q`2=(p1`2+p2`2)/2} as Subset of TOP-REAL 2;
reconsider q2=First_Point(P,p1,p2,Q1) as Point of TOP-REAL 2;
for Q being Subset of TOP-REAL 2 st Q={q:q`2=(p1`2+p2`2)/2}
holds q2=First_Point(P,p1,p2,Q);
hence thesis;
end;
uniqueness
proof
let q3,q4 be Point of TOP-REAL 2;
assume
A1: (for Q1 being Subset of TOP-REAL 2 st Q1={q1:q1`2=(p1`2+p2`2)/2}
holds q3=First_Point(P,p1,p2,Q1)) & for Q2 being Subset of TOP-REAL 2 st
Q2={q2:q2`2=(p1`2+p2`2)/2} holds q4=First_Point(P,p1,p2,Q2);
{q1:q1`2=(p1`2+p2`2)/2} c= the carrier of TOP-REAL 2
proof
let x be object;
assume x in {q1:q1`2=(p1`2+p2`2)/2};
then ex q being Point of TOP-REAL 2 st ( q=x)&( q`2=(p1`2+p2`2)/2 );
hence thesis;
end;
then reconsider Q3={q2:q2`2=(p1`2+p2`2)/2} as Subset of TOP-REAL 2;
q3=First_Point(P,p1,p2,Q3) by A1;
hence thesis by A1;
end;
end;
theorem
for P being Subset of TOP-REAL 2,
p1,p2 being Point of TOP-REAL 2 st P is_an_arc_of p1,p2 holds
x_Middle(P,p1,p2) in P & y_Middle(P,p1,p2) in P
proof
let P be Subset of TOP-REAL 2, p1,p2 be Point of TOP-REAL 2;
assume
A1: P is_an_arc_of p1,p2;
deffunc F(Point of TOP-REAL 2)=$1;
defpred P[Point of TOP-REAL 2] means $1`1=(p1`1+p2`1)/2;
reconsider Q={F(q):P[q]} as Subset of TOP-REAL 2 from DOMAIN_1:sch 8;
A2: x_Middle(P,p1,p2)=First_Point(P,p1,p2,Q) by Def1;
A3: P meets Q by A1,Th13;
P /\ Q is closed by A1,Th13;
then
A4: x_Middle(P,p1,p2) in P /\ Q by A1,A2,A3,JORDAN5C:def 1;
defpred Q[Point of TOP-REAL 2] means $1`2=(p1`2+p2`2)/2;
reconsider Q2={F(q):Q[q]} as Subset of TOP-REAL 2 from DOMAIN_1:sch 8;
A5: y_Middle(P,p1,p2)=First_Point(P,p1,p2,Q2) by Def2;
A6: P meets Q2 by A1,Th14;
P /\ Q2 is closed by A1,Th14;
then y_Middle(P,p1,p2) in P /\ Q2 by A1,A5,A6,JORDAN5C:def 1;
hence thesis by A4,XBOOLE_0:def 4;
end;
theorem
for P being Subset of TOP-REAL 2,
p1,p2 being Point of TOP-REAL 2 st P is_an_arc_of p1,p2 holds
p1=x_Middle(P,p1,p2) iff p1`1=p2`1
proof
let P be Subset of TOP-REAL 2, p1,p2 be Point of TOP-REAL 2;
assume
A1: P is_an_arc_of p1,p2;
A2: now
assume
A3: p1=x_Middle(P,p1,p2);
deffunc F(Point of TOP-REAL 2)=$1;
defpred P[Point of TOP-REAL 2] means $1`1=(p1`1+p2`1)/2;
reconsider Q1={F(q):P[q]} as Subset of TOP-REAL 2 from DOMAIN_1:sch 8;
A4: P meets Q1 by A1,Th13;
A5: P /\ Q1 is closed by A1,Th13;
x_Middle(P,p1,p2)=First_Point(P,p1,p2,Q1) by Def1;
then p1 in P /\ Q1 by A1,A3,A4,A5,JORDAN5C:def 1;
then p1 in Q1 by XBOOLE_0:def 4;
then ex q st q=p1 & q`1=(p1`1+p2`1)/2;
hence p1`1=p2`1;
end;
now
assume
A6: p1`1=p2`1;
for Q being Subset of TOP-REAL 2 st Q={q:q`1=(p1`1+p2`1)/2}
holds p1=First_Point(P,p1,p2,Q)
proof
let Q be Subset of TOP-REAL 2;
assume
A7: Q={q:q`1=(p1`1+p2`1)/2};
then
A8: p1 in Q by A6;
P /\ Q is closed by A1,A7,Th13;
hence thesis by A1,A8,JORDAN5C:3;
end;
hence p1=x_Middle(P,p1,p2) by Def1;
end;
hence thesis by A2;
end;
theorem
for P being Subset of TOP-REAL 2,
p1,p2 being Point of TOP-REAL 2 st P is_an_arc_of p1,p2 holds
p1=y_Middle(P,p1,p2) iff p1`2=p2`2
proof
let P be Subset of TOP-REAL 2, p1,p2 be Point of TOP-REAL 2;
assume
A1: P is_an_arc_of p1,p2;
A2: now
assume
A3: p1=y_Middle(P,p1,p2);
deffunc F(Point of TOP-REAL 2)=$1;
defpred P[Point of TOP-REAL 2] means $1`2=(p1`2+p2`2)/2;
reconsider Q1={F(q):P[q]} as Subset of TOP-REAL 2 from DOMAIN_1:sch 8;
A4: P meets Q1 by A1,Th14;
A5: P /\ Q1 is closed by A1,Th14;
y_Middle(P,p1,p2)=First_Point(P,p1,p2,Q1) by Def2;
then p1 in P /\ Q1 by A1,A3,A4,A5,JORDAN5C:def 1;
then p1 in Q1 by XBOOLE_0:def 4;
then ex q st ( q=p1)&( q`2=(p1`2+p2`2)/2);
hence p1`2=p2`2;
end;
now
assume
A6: p1`2=p2`2;
for Q being Subset of TOP-REAL 2 st Q={q:q`2=(p1`2+p2`2)/2}
holds p1=First_Point(P,p1,p2,Q)
proof
let Q be Subset of TOP-REAL 2;
assume
A7: Q={q:q`2=(p1`2+p2`2)/2};
then
A8: p1 in Q by A6;
P /\ Q is closed by A1,A7,Th14;
hence thesis by A1,A8,JORDAN5C:3;
end;
hence p1=y_Middle(P,p1,p2) by Def2;
end;
hence thesis by A2;
end;
begin ::Segments of Arcs
theorem Th18:
for P being Subset of TOP-REAL 2,
p1,p2,q1,q2 being Point of TOP-REAL 2 st P is_an_arc_of p1,p2
& LE q1,q2,P,p1,p2 holds LE q2,q1,P,p2,p1
proof
let P be Subset of TOP-REAL 2, p1,p2,q1,q2 be Point of TOP-REAL 2;
assume that
A1: P is_an_arc_of p1,p2 and
A2: LE q1,q2,P,p1,p2;
thus q2 in P & q1 in P by A2;
reconsider P9 = P as non empty Subset of TOP-REAL 2 by A1,TOPREAL1:1;
let f be Function of I[01], (TOP-REAL 2)|P, s1, s2 be Real;
assume that
A3: f is being_homeomorphism and
A4: f.0 = p2 and
A5: f.1 = p1 and
A6: f.s1 = q2 and
A7: 0 <= s1 and
A8: s1 <= 1 and
A9: f.s2 = q1 and
A10: 0 <= s2 and
A11: s2 <= 1;
A12: 1-0>=1-s1 by A7,XREAL_1:13;
A13: 1-0>=1-s2 by A10,XREAL_1:13;
A14: 1-1<=1-s1 by A8,XREAL_1:13;
A15: 1-1<=1-s2 by A11,XREAL_1:13;
set Ex = L[01]((0,1)(#),(#)(0,1));
A16: Ex is being_homeomorphism by TREAL_1:18;
set g = f * Ex;
A17: Ex.(0,1)(#) = 0 by BORSUK_1:def 14,TREAL_1:5,9;
A18: Ex.(#)(0,1) = 1 by BORSUK_1:def 15,TREAL_1:5,9;
dom f = [#]I[01] by A3,TOPS_2:def 5;
then rng Ex = dom f by A16,TOPMETR:20,TOPS_2:def 5;
then dom g = dom Ex by RELAT_1:27;
then
A19: dom g = [#]I[01] by A16,TOPMETR:20,TOPS_2:def 5;
reconsider g as Function
of I[01], (TOP-REAL 2)|P9 by TOPMETR:20;
A20: g is being_homeomorphism by A3,A16,TOPMETR:20,TOPS_2:57;
A21: (1-s1) in dom g by A12,A14,A19,BORSUK_1:43;
A22: (1-s2) in dom g by A13,A15,A19,BORSUK_1:43;
A23: g.0 = p1 by A5,A18,A19,BORSUK_1:def 14,FUNCT_1:12,TREAL_1:5;
A24: g.1 = p2 by A4,A17,A19,BORSUK_1:def 15,FUNCT_1:12,TREAL_1:5;
reconsider qs1=1-s1,qs2=1-s2 as Point of Closed-Interval-TSpace(0,1)
by A12,A13,A14,A15,BORSUK_1:43,TOPMETR:20;
A25: Ex.qs1 = (1-(1-s1))*1+(1-s1)*0 by BORSUK_1:def 14,def 15,TREAL_1:5,def 3
.=s1;
A26: Ex.qs2 = (1-(1-s2))*1+(1-s2)*0 by BORSUK_1:def 14,def 15,TREAL_1:5,def 3
.=s2;
A27: g.(1-s1) = q2 by A6,A21,A25,FUNCT_1:12;
g.(1-s2) = q1 by A9,A22,A26,FUNCT_1:12;
then 1-s2<=1-s1 by A2,A12,A13,A14,A20,A23,A24,A27;
then s1<=1-(1-s2) by XREAL_1:11;
hence thesis;
end;
definition
let P be Subset of TOP-REAL 2, p1,p2,q1 be Point of TOP-REAL 2;
func L_Segment(P,p1,p2,q1) -> Subset of TOP-REAL 2 equals
{q : LE q,q1,P,p1,p2};
coherence
proof
{q : LE q,q1,P,p1,p2} c= the carrier of TOP-REAL 2
proof
let x be object;
assume x in {q : LE q,q1,P,p1,p2};
then ex q st ( q=x)&( LE q,q1,P,p1,p2);
hence thesis;
end;
hence thesis;
end;
end;
definition
let P be Subset of TOP-REAL 2, p1,p2,q1 be Point of TOP-REAL 2;
func R_Segment(P,p1,p2,q1) -> Subset of TOP-REAL 2 equals
{q: LE q1,q,P,p1,p2};
coherence
proof
{q : LE q1,q,P,p1,p2} c= the carrier of TOP-REAL 2
proof
let x be object;
assume x in {q : LE q1,q,P,p1,p2};
then ex q st ( q=x)&( LE q1,q,P,p1,p2);
hence thesis;
end;
hence thesis;
end;
end;
theorem Th19:
for P being Subset of TOP-REAL 2, p1,p2,q1 being Point of TOP-REAL 2
holds L_Segment(P,p1,p2,q1) c= P
proof
let P be Subset of TOP-REAL 2, p1,p2,q1 be Point of TOP-REAL 2;
let x be object;
assume x in L_Segment(P,p1,p2,q1);
then ex q st q=x & LE q,q1,P,p1,p2;
hence thesis;
end;
theorem Th20:
for P being Subset of TOP-REAL 2, p1,p2,q1 being Point of TOP-REAL 2
holds R_Segment(P,p1,p2,q1) c= P
proof
let P be Subset of TOP-REAL 2, p1,p2,q1 be Point of TOP-REAL 2;
let x be object;
assume x in R_Segment(P,p1,p2,q1);
then ex q st q=x & LE q1,q,P,p1,p2;
hence thesis;
end;
theorem
for P being Subset of TOP-REAL 2,
p1,p2 being Point of TOP-REAL 2 st P is_an_arc_of p1,p2 holds
L_Segment(P,p1,p2,p1)={p1}
proof
let P be Subset of TOP-REAL 2, p1,p2 be Point of TOP-REAL 2;
assume
A1: P is_an_arc_of p1,p2;
then
A2: p1 in P by TOPREAL1:1;
thus L_Segment(P,p1,p2,p1) c= {p1}
proof
let x be object;
assume x in L_Segment(P,p1,p2,p1);
then consider q such that
A3: q=x and
A4: LE q,p1,P,p1,p2;
q in P by A4;
then LE p1,q,P,p1,p2 by A1,JORDAN5C:10;
then q=p1 by A1,A4,JORDAN5C:12;
hence thesis by A3,TARSKI:def 1;
end;
let x be object;
assume x in {p1};
then
A5: x=p1 by TARSKI:def 1;
LE p1,p1,P,p1,p2 by A2,JORDAN5C:9;
hence thesis by A5;
end;
theorem
for P being Subset of TOP-REAL 2,
p1,p2 being Point of TOP-REAL 2 st P is_an_arc_of p1,p2 holds
L_Segment(P,p1,p2,p2)=P
proof
let P be Subset of TOP-REAL 2, p1,p2 be Point of TOP-REAL 2;
assume
A1: P is_an_arc_of p1,p2;
thus L_Segment(P,p1,p2,p2) c= P by Th19;
let x be object;
assume
A2: x in P;
then reconsider p=x as Point of TOP-REAL 2;
LE p,p2,P,p1,p2 by A1,A2,JORDAN5C:10;
hence thesis;
end;
theorem
for P being Subset of TOP-REAL 2,
p1,p2 being Point of TOP-REAL 2 st P is_an_arc_of p1,p2 holds
R_Segment(P,p1,p2,p2)={p2}
proof
let P be Subset of TOP-REAL 2, p1,p2 be Point of TOP-REAL 2;
assume
A1: P is_an_arc_of p1,p2;
then
A2: p2 in P by TOPREAL1:1;
thus R_Segment(P,p1,p2,p2) c= {p2}
proof
let x be object;
assume x in R_Segment(P,p1,p2,p2);
then consider q such that
A3: q=x and
A4: LE p2,q,P,p1,p2;
q in P by A4;
then LE q,p2,P,p1,p2 by A1,JORDAN5C:10;
then q=p2 by A1,A4,JORDAN5C:12;
hence thesis by A3,TARSKI:def 1;
end;
let x be object;
assume x in {p2};
then
A5: x=p2 by TARSKI:def 1;
LE p2,p2,P,p1,p2 by A2,JORDAN5C:9;
hence thesis by A5;
end;
theorem
for P being Subset of TOP-REAL 2,p1,p2 being
Point of TOP-REAL 2 st P is_an_arc_of p1,p2 holds R_Segment(P,p1,p2,p1)=P
proof
let P be Subset of TOP-REAL 2, p1,p2 be Point of TOP-REAL 2;
assume
A1: P is_an_arc_of p1,p2;
thus R_Segment(P,p1,p2,p1) c= P by Th20;
let x be object;
assume
A2: x in P;
then reconsider p=x as Point of TOP-REAL 2;
LE p1,p,P,p1,p2 by A1,A2,JORDAN5C:10;
hence thesis;
end;
theorem
for P being Subset of TOP-REAL 2,
p1,p2,q1 being Point of TOP-REAL 2 st P is_an_arc_of p1,p2
holds
R_Segment(P,p1,p2,q1)=L_Segment(P,p2,p1,q1)
proof
let P be Subset of TOP-REAL 2, p1,p2,q1 be Point of TOP-REAL 2;
assume that
A1: P is_an_arc_of p1,p2;
A2: {q: LE q1,q,P,p1,p2} c= {q2 : LE q2,q1,P,p2,p1}
proof
let x be object;
assume x in {q: LE q1,q,P,p1,p2};
then consider q such that
A3: q=x and
A4: LE q1,q,P,p1,p2;
LE q,q1,P,p2,p1 by A1,A4,Th18;
hence thesis by A3;
end;
{q2 : LE q2,q1,P,p2,p1} c= {q: LE q1,q,P,p1,p2}
proof
let x be object;
assume x in {q: LE q,q1,P,p2,p1};
then consider q such that
A5: q=x and
A6: LE q,q1,P,p2,p1;
LE q1,q,P,p1,p2 by A1,A6,Th18,JORDAN5B:14;
hence thesis by A5;
end;
hence thesis by A2;
end;
definition
let P be Subset of TOP-REAL 2, p1,p2,q1,q2 be Point of TOP-REAL 2;
func Segment(P,p1,p2,q1,q2) -> Subset of TOP-REAL 2 equals
R_Segment(P,p1,p2,q1) /\ L_Segment(P,p1,p2,q2);
correctness;
end;
theorem
for P being Subset of TOP-REAL 2, p1,p2,q1,q2 being Point of TOP-REAL 2
holds Segment(P,p1,p2,q1,q2)={q:LE q1,q,P,p1,p2 & LE q,q2,P,p1,p2}
proof
let P be Subset of TOP-REAL 2, p1,p2,q1,q2 be Point of TOP-REAL 2;
thus Segment(P,p1,p2,q1,q2) c= {q:LE q1,q,P,p1,p2 & LE q,q2,P,p1,p2}
proof
let x be object;
assume
A1: x in Segment(P,p1,p2,q1,q2);
then
A2: x in R_Segment(P,p1,p2,q1) by XBOOLE_0:def 4;
A3: x in L_Segment(P,p1,p2,q2) by A1,XBOOLE_0:def 4;
A4: ex q st ( q=x)&( LE q1,q,P,p1,p2) by A2;
ex p st ( p=x)&( LE p,q2,P,p1,p2) by A3;
hence thesis by A4;
end;
let x be object;
assume x in {q:LE q1,q,P,p1,p2 & LE q,q2,P,p1,p2};
then
A5: ex q st ( q=x)&( LE q1,q,P,p1,p2)&( LE q,q2,P,p1,p2);
then
A6: x in R_Segment(P,p1,p2,q1);
x in L_Segment(P,p1,p2,q2) by A5;
hence thesis by A6,XBOOLE_0:def 4;
end;
theorem
for P being Subset of TOP-REAL 2, p1,p2,q1,q2 being Point of TOP-REAL 2
st P is_an_arc_of p1,p2 & LE q2,q1,P,p2,p1
holds LE q1,q2,P,p1,p2 by Th18,JORDAN5B:14;
theorem Th28:
for P being Subset of TOP-REAL 2, p1,p2,q being Point of TOP-REAL 2 st
P is_an_arc_of p1,p2
holds L_Segment(P,p1,p2,q)=R_Segment(P,p2,p1,q)
proof
let P be Subset of TOP-REAL 2, p1,p2,q be Point of TOP-REAL 2;
assume that
A1: P is_an_arc_of p1,p2;
thus L_Segment(P,p1,p2,q) c= R_Segment(P,p2,p1,q)
proof
let x be object;
assume x in L_Segment(P,p1,p2,q);
then consider p such that
A2: p=x and
A3: LE p,q,P,p1,p2;
LE q,p,P,p2,p1 by A1,A3,Th18;
hence thesis by A2;
end;
let x be object;
assume x in R_Segment(P,p2,p1,q);
then consider p such that
A4: p=x and
A5: LE q,p,P,p2,p1;
LE p,q,P,p1,p2 by A1,A5,Th18,JORDAN5B:14;
hence thesis by A4;
end;
theorem
for P being Subset of TOP-REAL 2, p1,p2,q1,q2 being Point of TOP-REAL 2 st
P is_an_arc_of p1,p2
holds Segment(P,p1,p2,q1,q2)=Segment(P,p2,p1,q2,q1)
proof
let P be Subset of TOP-REAL 2, p1,p2,q1,q2 be Point of TOP-REAL 2;
assume
A1: P is_an_arc_of p1,p2;
then L_Segment(P,p1,p2,q2)=R_Segment(P,p2,p1,q2) by Th28;
hence thesis by A1,Th28,JORDAN5B:14;
end;
begin ::Decomposition of a Simple Closed Curve into Two Arcs
definition
let s be Real;
func Vertical_Line(s) -> Subset of TOP-REAL 2 equals
{p where p is Point of TOP-REAL 2: p`1=s};
correctness
proof
{p where p is Point of TOP-REAL 2: p`1=s} c= the carrier of (TOP-REAL 2 )
proof
let x be object;
assume x in {p where p is Point of TOP-REAL 2: p`1=s};
then ex p being Point of TOP-REAL 2 st p=x & p`1=s;
hence thesis;
end;
hence thesis;
end;
func Horizontal_Line(s) -> Subset of TOP-REAL 2 equals
{p: p`2=s};
correctness
proof
{p where p is Point of TOP-REAL 2: p`2=s} c= the carrier of (TOP-REAL 2 )
proof
let x be object;
assume x in {p where p is Point of TOP-REAL 2: p`2=s};
then ex p being Point of TOP-REAL 2 st p=x & p`2=s;
hence thesis;
end;
hence thesis;
end;
end;
theorem
for r being Real holds
Vertical_Line(r) is closed & Horizontal_Line(r) is closed by Th6,Th9;
theorem Th31:
for r being Real,p being Point of TOP-REAL 2 holds
p in Vertical_Line(r) iff p`1=r
proof
let r be Real,p be Point of TOP-REAL 2;
hereby
assume p in Vertical_Line(r);
then ex q being Point of TOP-REAL 2 st q=p & q`1=r;
hence p`1=r;
end;
assume p`1 = r;
hence thesis;
end;
theorem
for r being Real,p being Point of TOP-REAL 2 holds
p in Horizontal_Line(r) iff p`2=r
proof
let r be Real,p be Point of TOP-REAL 2;
hereby
assume p in Horizontal_Line(r);
then ex q being Point of TOP-REAL 2 st q=p & q`2=r;
hence p`2=r;
end;
assume p`2 = r;
hence thesis;
end;
theorem Th33:
for P being Subset of TOP-REAL 2 st P is being_simple_closed_curve
ex P1,P2 being non empty Subset of TOP-REAL 2 st
P1 is_an_arc_of W-min(P),E-max(P) & P2 is_an_arc_of E-max(P),W-min(P)
& P1 /\ P2={W-min(P),E-max(P)} & P1 \/ P2=P
& First_Point(P1,W-min(P),E-max(P),
Vertical_Line((W-bound(P)+E-bound(P))/2))`2>
Last_Point(P2,E-max(P),W-min(P), Vertical_Line((W-bound(P)+E-bound(P))/2))`2
proof
let P be Subset of TOP-REAL 2;
assume P is being_simple_closed_curve;
then reconsider P as Simple_closed_curve;
A1: W-min(P) in P by SPRECT_1:13;
A2: E-max(P) in P by SPRECT_1:14;
W-min(P)<>E-max(P) by TOPREAL5:19;
then consider P01,P02 being non empty Subset of TOP-REAL 2 such that
A3: P01 is_an_arc_of W-min(P),E-max(P) and
A4: P02 is_an_arc_of W-min(P),E-max(P) and
A5: P = P01 \/ P02 and
A6: P01 /\ P02 = {W-min(P),E-max(P)} by A1,A2,TOPREAL2:5;
reconsider P01,P02 as non empty Subset of TOP-REAL 2;
A7: P01 is_an_arc_of E-max(P),W-min(P) by A3,JORDAN5B:14;
A8: P02 is_an_arc_of E-max(P),W-min(P) by A4,JORDAN5B:14;
reconsider P001=P01, P002=P02 as non empty Subset of TOP-REAL 2;
A9: (E-max P)`1 = E-bound P by EUCLID:52;
A10: Vertical_Line((W-bound(P)+E-bound(P))/2) is closed by Th6;
P01 is closed by A3,COMPTS_1:7,JORDAN5A:1;
then
A11: P01/\Vertical_Line((W-bound(P)+E-bound(P))/2) is closed by A10,TOPS_1:8;
A12: Vertical_Line((W-bound(P)+E-bound(P))/2) is closed by Th6;
P02 is closed by A4,COMPTS_1:7,JORDAN5A:1;
then
A13: P02/\Vertical_Line((W-bound(P)+E-bound(P))/2) is closed by A12,TOPS_1:8;
consider q1 being Point of TOP-REAL 2 such that
A14: q1 in P001 and
A15: q1`1 = ((W-min(P))`1+(E-max(P))`1)/2 by A3,Th12;
A16: (W-min P)`1 = W-bound P by EUCLID:52;
(E-max P)`1 = E-bound P by EUCLID:52;
then q1 in {p where p is Point of TOP-REAL 2: p`1=(W-bound(P)+E-bound(P
))/2} by A15,A16;
then P01/\Vertical_Line((W-bound(P)+E-bound(P))/2) <> {}
by A14,XBOOLE_0:def 4;
then
A17: P01 meets Vertical_Line((W-bound(P)+E-bound(P))/2);
consider q2 being Point of TOP-REAL 2 such that
A18: q2 in P002 and
A19: q2`1 = ((W-min(P))`1+(E-max(P))`1)/2 by A4,Th12;
q2 in {p where p is Point of TOP-REAL 2: p`1=(W-bound(P)+E-bound(P ) ) / 2 }
by A9,A16,A19;
then P02/\Vertical_Line((W-bound(P)+E-bound(P))/2) <> {}
by A18,XBOOLE_0:def 4;
then
A20: P02 meets Vertical_Line((W-bound(P)+E-bound(P))/2);
per cases;
suppose First_Point(P01,W-min(P),E-max(P),
Vertical_Line((W-bound(P)+E-bound(P))/2))`2>
Last_Point(P02,E-max(P),W-min(P),
Vertical_Line((W-bound(P)+E-bound(P))/2))`2;
hence thesis by A3,A5,A6,A8;
end;
suppose
A21: First_Point(P01,W-min(P),E-max(P),
Vertical_Line((W-bound(P)+E-bound(P))/2))`2<=
Last_Point(P02,E-max(P),W-min(P),
Vertical_Line((W-bound(P)+E-bound(P))/2))`2;
now per cases by A21,XXREAL_0:1;
case
A22: First_Point(P01,W-min(P),E-max(P),
Vertical_Line((W-bound(P)+E-bound(P))/2))`2<
Last_Point(P02,E-max(P),W-min(P),
Vertical_Line((W-bound(P)+E-bound(P))/2))`2;
A23: First_Point(P01,W-min(P),E-max(P),
Vertical_Line((W-bound(P)+E-bound(P))/2)) =
Last_Point(P01,E-max(P),W-min(P),
Vertical_Line((W-bound(P)+E-bound(P))/2)) by A3,A11,A17,JORDAN5C:18;
Last_Point(P02,E-max(P),W-min(P),
Vertical_Line((W-bound(P)+E-bound(P))/2))
= First_Point(P02,W-min(P),E-max(P),
Vertical_Line((W-bound(P)+E-bound(P))/2)) by A4,A13,A20,JORDAN5C:18;
hence ex P1,P2 being non empty Subset of TOP-REAL 2 st
P1 is_an_arc_of W-min(P),E-max(P) & P2 is_an_arc_of E-max(P),W-min(P)
& P1 /\ P2={W-min(P),E-max(P)} & P1 \/ P2=P
& First_Point(P1,W-min(P),E-max(P),
Vertical_Line((W-bound(P)+E-bound(P))/2))`2>
Last_Point(P2,E-max(P),W-min(P),
Vertical_Line((W-bound(P)+E-bound(P))/2))`2 by A4,A5,A6,A7,A22,A23;
end;
case
A24: First_Point(P01,W-min(P),E-max(P),
Vertical_Line((W-bound(P)+E-bound(P))/2))`2=
Last_Point(P02,E-max(P),W-min(P),
Vertical_Line((W-bound(P)+E-bound(P))/2))`2;
set p=First_Point(P01,W-min(P),E-max(P),
Vertical_Line((W-bound(P)+E-bound(P))/2));
set p9=Last_Point(P02,E-max(P),W-min(P),
Vertical_Line((W-bound(P)+E-bound(P))/2));
A25: p in P01/\ Vertical_Line((W-bound(P)+E-bound(P))/2)
by A3,A11,A17,JORDAN5C:def 1;
then
A26: p in P01 by XBOOLE_0:def 4;
p in Vertical_Line((W-bound(P)+E-bound(P))/2) by A25,XBOOLE_0:def 4;
then
A27: p`1=(W-bound(P)+E-bound(P))/2 by Th31;
A28: p9 in P02/\ Vertical_Line((W-bound(P)+E-bound(P))/2)
by A8,A13,A20,JORDAN5C:def 2;
then
A29: p9 in P02 by XBOOLE_0:def 4;
p9 in Vertical_Line((W-bound(P)+E-bound(P))/2) by A28,XBOOLE_0:def 4;
then p9`1=(W-bound(P)+E-bound(P))/2 by Th31;
then p=p9 by A24,A27,TOPREAL3:6;
then p in P01 /\ P02 by A26,A29,XBOOLE_0:def 4;
then p=W-min(P) or p=E-max(P) by A6,TARSKI:def 2;
hence contradiction by A9,A16,A27,TOPREAL5:17;
end;
end;
then consider P1,P2 being non empty Subset of TOP-REAL 2 such that
A30: P1 is_an_arc_of W-min(P),E-max(P) and
A31: P2 is_an_arc_of E-max(P),W-min(P) and
A32: P1 /\ P2={W-min(P),E-max(P)} and
A33: P1 \/ P2=P and
A34: First_Point(P1,W-min(P),E-max(P), Vertical_Line((W-bound(P)+E-bound
(P))/2))`2> Last_Point(P2,E-max(P),W-min(P), Vertical_Line((W-bound(P)+E-bound(
P))/2))`2;
reconsider P1,P2 as non empty Subset of TOP-REAL 2;
take P1, P2;
thus thesis by A30,A31,A32,A33,A34;
end;
end;
begin ::Uniqueness of Decomposition of a Simple Closed Curve
theorem Th34:
for P being Subset of I[01] st
P=(the carrier of I[01]) \{0,1} holds P is open
proof
let P be Subset of I[01];
assume
A1: P=(the carrier of I[01]) \{0,1};
A2: 0 in [.0,1.] by XXREAL_1:1;
A3: 1 in [.0,1.] by XXREAL_1:1;
reconsider Q0={0} as Subset of I[01] by A2,BORSUK_1:40,ZFMISC_1:31;
reconsider Q1={1} as Subset of I[01] by A3,BORSUK_1:40,ZFMISC_1:31;
Q0 \/ Q1 is closed by A2,A3,BORSUK_1:40,TOPS_1:9;
then [#](I[01])\(Q0 \/ Q1) is open;
hence thesis by A1,ENUMSET1:1;
end;
theorem
for P being Subset of R^1, r,s being Real st P=].r,s.[ holds P is open
proof
let P be Subset of R^1, r,s be Real;
assume
A1: P=].r,s.[;
{r1:r<r1} c= REAL
proof
let x be object;
assume x in {r1:r<r1};
then consider r1 such that
A2: ( r1=x)&( r<r1);
r1 in REAL by XREAL_0:def 1;
hence thesis by A2;
end;
then reconsider P1={r1 where r1 is Real:r<r1} as Subset of R^1
by TOPMETR:17;
{r2:s>r2} c= REAL
proof
let x be object;
assume x in {r2:s>r2};
then consider r2 such that
A3: ( r2=x)&( s>r2);
r2 in REAL by XREAL_0:def 1;
hence thesis by A3;
end;
then reconsider P2={r2 where r2 is Real:s>r2} as Subset of R^1
by TOPMETR:17;
A4: P1 is open by JORDAN2B:25;
A5: P2 is open by JORDAN2B:24;
A6: P c= P1 /\ P2
proof
let x be object;
assume
A7: x in P;
then reconsider r1=x as Real;
A8: r<r1 by A1,A7,XXREAL_1:4;
A9: r1<s by A1,A7,XXREAL_1:4;
A10: x in P1 by A8;
x in P2 by A9;
hence thesis by A10,XBOOLE_0:def 4;
end;
P1 /\ P2 c= P
proof
let x be object;
assume
A11: x in P1 /\ P2;
then
A12: x in P1 by XBOOLE_0:def 4;
A13: x in P2 by A11,XBOOLE_0:def 4;
A14: ex r1 st ( r1=x)&( r<r1) by A12;
ex r2 st ( r2=x)&( s>r2) by A13;
hence thesis by A1,A14,XXREAL_1:4;
end;
then P=P1 /\ P2 by A6;
hence thesis by A4,A5,TOPS_1:11;
end;
theorem Th36:
for P7 being Subset of I[01] st
P7=(the carrier of I[01]) \{0,1} holds P7<>{} & P7 is connected
proof
let P7 be Subset of I[01];
assume
A1: P7=(the carrier of I[01]) \{0,1};
A2: 1/2 in [.0,1.] by XXREAL_1:1;
A3: not 1/2 in {0,1} by TARSKI:def 2;
A4: [#](I[01]|P7)=P7 by PRE_TOPC:def 5;
for A,B being Subset of I[01]|P7
st [#](I[01]|P7) = A \/ B & A <> {}(I[01]|P7)
& B <> {}(I[01]|P7) & A is open & B is open holds A meets B
proof
let A,B be Subset of I[01]|P7;
assume that
A5: [#](I[01]|P7) = A \/ B and
A6: A <> {}(I[01]|P7) and
A7: B <> {}(I[01]|P7) and
A8: A is open and
A9: B is open;
assume
A10: A misses B;
A11: ].0,1.[ misses {0,1} by XXREAL_1:86;
A12: P7=(].0,1.[ \/ {0,1})\{0,1} by A1,BORSUK_1:40,XXREAL_1:128
.=].0,1.[ \{0,1} by XBOOLE_1:40
.=].0,1.[ by A11,XBOOLE_1:83;
reconsider D1=[.0,1.] as Subset of R^1 by TOPMETR:17;
reconsider P1=P7 as Subset of R^1 by A12,TOPMETR:17;
I[01]=R^1|D1 by TOPMETR:19,20;
then
A13: I[01]|P7=R^1|P1 by BORSUK_1:40,PRE_TOPC:7;
P1={r1:0<r1 & r1<1} by A12,RCOMP_1:def 2;
then P1 is open by JORDAN2B:26;
then
A14: I[01]|P7 is non empty open SubSpace of R^1
by A1,A2,A3,A4,A13,BORSUK_1:40,TSEP_1:16,XBOOLE_0:def 5;
reconsider P = A, Q = B as non empty Subset of REAL
by A4,A6,A7,A12,XBOOLE_1:1;
reconsider A0 = P, B0 = Q as non empty Subset of R^1
by METRIC_1:def 13,TOPMETR:12,def 6;
A15: A0 is open by A8,A14,TSEP_1:17;
A16: B0 is open by A9,A14,TSEP_1:17;
set xp = the Element of P;
reconsider xp as Real;
A17: xp in P;
0 is LowerBound of P
proof
let r be ExtReal;
assume r in P;
then r in ].0,1.[ by A4,A12;
then r in {w where w is Real: 0<w & w<1} by RCOMP_1:def 2;
then ex u being Real st u = r & 0<u & u<1;
hence 0 <= r;
end;
then
A18: P is bounded_below;
0 is LowerBound of Q
proof
let r be ExtReal;
assume r in Q;
then r in ].0,1.[ by A4,A12;
then r in {w where w is Real: 0<w & w<1} by RCOMP_1:def 2;
then ex u being Real st u = r & 0<u & u<1;
hence 0 <= r;
end;
then
A19: Q is bounded_below;
reconsider l = lower_bound Q as Element of REAL by XREAL_0:def 1;
reconsider m = l as Point of RealSpace by METRIC_1:def 13;
reconsider t = m as Point of R^1 by TOPMETR:12,def 6;
A20: not l in Q
proof
assume l in Q;
then consider s being Real such that
A21: s > 0 and
A22: Ball(m,s) c= B0 by A16,TOPMETR:15,def 6;
reconsider s as Element of REAL by XREAL_0:def 1;
reconsider s2 = l-s/2 as Element of REAL by XREAL_0:def 1;
reconsider e1 = s2 as Point of RealSpace by METRIC_1:def 13;
s/2<s by A21,XREAL_1:216;
then |.l - (l-s/2).| < s by A21,ABSVALUE:def 1;
then (the distance of RealSpace).(m,e1) < s by METRIC_1:def 12,def 13;
then dist(m,e1) < s by METRIC_1:def 1;
then e1 in {z where z is Element of RealSpace : dist(m,z)<s};
then l-s/2 in Ball(m,s) by METRIC_1:17;
then l<=l-s/2 by A19,A22,SEQ_4:def 2;
then l+s/2<=l by XREAL_1:19;
then l+s/2-l<=l-l by XREAL_1:9;
hence contradiction by A21,XREAL_1:139;
end;
A23: now
assume
A24: l<=0;
0<xp by A4,A12,A17,XXREAL_1:4;
then consider r5 being Real such that
A25: r5 in Q and
A26: r5<l+(xp-l) by A19,A24,SEQ_4:def 2;
reconsider r5 as Real;
A27: {s5 where s5 is Real:s5 in P & r5<s5} c= P
proof
let y be object;
assume y in {s5 where s5 is Real:s5 in P & r5<s5};
then ex s5 being Real st s5=y & s5 in P & r5<s5;
hence thesis;
end;
then reconsider P5={s5 where s5 is Real:s5 in P & r5<s5}
as Subset of REAL by XBOOLE_1:1;
set PP5={s5 where s5 is Real:s5 in P & r5<s5};
A28: xp in P5 by A26;
A29: P5 is bounded_below by A18,A27,XXREAL_2:44;
reconsider l5 = lower_bound P5 as Element of REAL by XREAL_0:def 1;
reconsider m5 = l5 as Point of RealSpace by METRIC_1:def 13;
A30: now
assume
A31: l5<=r5;
now
assume l5<r5;
then r5-l5>0 by XREAL_1:50;
then consider r be Real such that
A32: r in P5 and
A33: r<l5+(r5-l5) by A28,A29,SEQ_4:def 2;
ex s6 being Real st ( s6=r)&( s6 in P)&( r5<s6) by A32;
hence contradiction by A33;
end;
then l5=r5 by A31,XXREAL_0:1;
then consider r7 being Real such that
A34: r7 > 0 and
A35: Ball(m5,r7) c= B0 by A16,A25,TOPMETR:15,def 6;
consider r9 being Real such that
A36: r9 in P5 and
A37: r9<l5+r7 by A28,A29,A34,SEQ_4:def 2;
reconsider r9 as Element of REAL by XREAL_0:def 1;
reconsider e8=r9 as Point of RealSpace by METRIC_1:def 13;
l5<=r9 by A29,A36,SEQ_4:def 2;
then
A38: r9-l5>=0 by XREAL_1:48;
r9-l5<l5+r7-l5 by A37,XREAL_1:9;
then |.r9 - l5.| < r7 by A38,ABSVALUE:def 1;
then (the distance of RealSpace).(e8,m5) < r7
by METRIC_1:def 12,def 13;
then dist(e8,m5) < r7 by METRIC_1:def 1;
then e8 in {z where z is Element of RealSpace : dist(m5,z)<r7};
then e8 in Ball(m5,r7) by METRIC_1:17;
hence contradiction by A10,A27,A35,A36,XBOOLE_0:3;
end;
A39: 0<r5 by A4,A12,A25,XXREAL_1:4;
A40: l5-r5>0 by A30,XREAL_1:50;
set q = the Element of P5;
A41: q in P5 by A28;
reconsider q1=q as Real;
q1 in P by A27,A41;
then
A42: q1<1 by A4,A12,XXREAL_1:4;
l5<=q1 by A28,A29,SEQ_4:def 2;
then l5<1 by A42,XXREAL_0:2;
then l5 in ].0,1.[ by A30,A39,XXREAL_1:4;
then
A43: l5 in P or l5 in Q by A4,A5,A12,XBOOLE_0:def 3;
now
assume l5 in P;
then consider s5 being Real such that
A44: s5 > 0 and
A45: Ball(m5,s5) c= P by A15,TOPMETR:15,def 6;
reconsider s5 as Element of REAL by XREAL_0:def 1;
set s59=min(s5,l5-r5);
A46: s59>0 by A40,A44,XXREAL_0:21;
A47: s59<=s5 by XXREAL_0:17;
A48: s59/2<s59 by A46,XREAL_1:216;
s59<=l5-r5 by XXREAL_0:17;
then s59/2<l5-r5 by A48,XXREAL_0:2;
then s59/2+r5<l5-r5+r5 by XREAL_1:6;
then
A49: s59/2+r5-s59/2<l5-s59/2 by XREAL_1:9;
reconsider e1 = l5-s59/2 as Element of REAL by XREAL_0:def 1;
reconsider e1 as Point of RealSpace by METRIC_1:def 13;
s59/2<s59 by A46,XREAL_1:216;
then s59/2<s5 by A47,XXREAL_0:2;
then |.l5 - (l5-s59/2).| < s5 by A46,ABSVALUE:def 1;
then (real_dist).(l5,l5-s59/2) < s5 by METRIC_1:def 12;
then dist(m5,e1) < s5 by METRIC_1:def 1,def 13;
then e1 in {z where z is Element of RealSpace : dist(m5,z)<s5};
then l5-s59/2 in Ball(m5,s5) by METRIC_1:17;
then
A50: l5-s59/2 in {s7 where s7 is Real:s7 in P & r5<s7 } by A45,A49;
l5<l5+s59/2 by A46,XREAL_1:29,139;
then l5-s59/2<l5+s59/2-s59/2 by XREAL_1:9;
hence contradiction by A29,A50,SEQ_4:def 2;
end;
then consider s1 being Real such that
A51: s1 > 0 and
A52: Ball(m5,s1) c= B0 by A16,A43,TOPMETR:15,def 6;
s1/2>0 by A51,XREAL_1:139;
then consider r2 be Real such that
A53: r2 in P5 and
A54: r2<l5+s1/2 by A28,A29,SEQ_4:def 2;
reconsider r2 as Element of REAL by XREAL_0:def 1;
A55: l5<=r2 by A29,A53,SEQ_4:def 2;
reconsider s3 = r2-l5 as Element of REAL;
reconsider e1 = l5+s3 as Point of RealSpace by METRIC_1:def 13;
A56: r2-l5>=0 by A55,XREAL_1:48;
A57: r2-l5<l5+s1/2-l5 by A54,XREAL_1:14;
s1/2<s1 by A51,XREAL_1:216;
then
A58: l5+s3-l5<s1 by A57,XXREAL_0:2;
|.l5+s3 - l5.|=l5+s3-l5 by A56,ABSVALUE:def 1;
then (real_dist).(l5+s3,l5) < s1 by A58,METRIC_1:def 12;
then dist(e1,m5) < s1 by METRIC_1:def 1,def 13;
then l5+s3 in {z where z is Element of RealSpace : dist(m5,z)<s1};
then l5+s3 in Ball(m5,s1) by METRIC_1:17;
then
A59: l5+s3 in P5 /\ Q by A52,A53,XBOOLE_0:def 4;
P5 /\ Q c= P /\ Q by A27,XBOOLE_1:26;
hence contradiction by A10,A59;
end;
set q = the Element of Q;
A60: q in Q;
reconsider q1=q as Real;
A61: q1<1 by A4,A12,A60,XXREAL_1:4;
l<=q1 by A19,SEQ_4:def 2;
then l<1 by A61,XXREAL_0:2;
then l in ].0,1.[ by A23,XXREAL_1:4;
then
A62: t in A0 by A4,A5,A12,A20,XBOOLE_0:def 3;
A0 is open by A8,A14,TSEP_1:17;
then consider s1 being Real such that
A63: s1 > 0 and
A64: Ball(m,s1) c= A0 by A62,TOPMETR:15,def 6;
s1/2>0 by A63,XREAL_1:139;
then consider r2 be Real such that
A65: r2 in Q and
A66: r2<l+s1/2 by A19,SEQ_4:def 2;
reconsider r2 as Element of REAL by XREAL_0:def 1;
A67: l<=r2 by A19,A65,SEQ_4:def 2;
set s3=r2-l;
reconsider e1 = l+s3 as Point of RealSpace by METRIC_1:def 13;
A68: r2-l>=0 by A67,XREAL_1:48;
A69: r2-l<l+s1/2-l by A66,XREAL_1:14;
s1/2<s1 by A63,XREAL_1:216;
then
A70: l+s3-l<s1 by A69,XXREAL_0:2;
|.l+s3 - l.|=l+s3-l by A68,ABSVALUE:def 1;
then (real_dist).(l+s3,l) < s1 by A70,METRIC_1:def 12;
then dist(e1,m) < s1 by METRIC_1:def 1,def 13;
then l+s3 in {z where z is Element of RealSpace : dist(m,z)<s1};
then l+s3 in Ball(m,s1) by METRIC_1:17;
hence contradiction by A10,A64,A65,XBOOLE_0:3;
end;
then I[01]|P7 is connected by CONNSP_1:11;
hence thesis by A1,A2,A3,BORSUK_1:40,CONNSP_1:def 3,XBOOLE_0:def 5;
end;
theorem Th37:
for P being Subset of TOP-REAL n,
p1,p2 being Point of TOP-REAL n st P is_an_arc_of p1,p2 holds p1<>p2
proof
let P be Subset of TOP-REAL n, p1,p2 be Point of TOP-REAL n;
assume P is_an_arc_of p1,p2;
then consider f being Function of I[01], (TOP-REAL n)|P such that
A1: f is being_homeomorphism and
A2: f.0 = p1 and
A3: f.1 = p2 by TOPREAL1:def 1;
1 in [#](I[01]) by BORSUK_1:40,XXREAL_1:1;
then
A4: 1 in dom f by A1,TOPS_2:def 5;
A5: f is one-to-one by A1,TOPS_2:def 5;
0 in [#](I[01]) by BORSUK_1:40,XXREAL_1:1;
then 0 in dom f by A1,TOPS_2:def 5;
hence thesis by A2,A3,A4,A5,FUNCT_1:def 4;
end;
theorem
for P being Subset of TOP-REAL n, Q being Subset of (TOP-REAL n)|P,
p1,p2 being Point of TOP-REAL n st
P is_an_arc_of p1,p2 & Q=P\{p1,p2} holds Q is open
proof
let P be Subset of TOP-REAL n, Q be Subset of (TOP-REAL n)|P,
p1,p2 be Point of TOP-REAL n;
assume that
A1: P is_an_arc_of p1,p2 and
A2: Q=P\{p1,p2};
reconsider P9 = P as non empty Subset of TOP-REAL n by A1,TOPREAL1:1;
consider f being Function of I[01], (TOP-REAL n)|P9 such that
A3: f is being_homeomorphism and
A4: f.0 = p1 and
A5: f.1 = p2 by A1,TOPREAL1:def 1;
reconsider f1=f as Function;
A6: f" is being_homeomorphism by A3,TOPS_2:56;
reconsider g=f" as Function of (TOP-REAL n)|P,I[01];
reconsider g1=g as Function;
reconsider R=(the carrier of I[01])\{0,1} as Subset of I[01];
A7: [#]I[01] <> {};
A8: R is open by Th34;
A9: f is one-to-one by A3,TOPS_2:def 5;
A10: g is one-to-one by A6,TOPS_2:def 5;
A11: g is continuous by A3,TOPS_2:def 5;
A12: [#](I[01])=dom f by A3,TOPS_2:def 5;
0 in [#](I[01]) by BORSUK_1:40,XXREAL_1:1;
then
A13: 0 in dom f by A3,TOPS_2:def 5;
1 in [#](I[01]) by BORSUK_1:40,XXREAL_1:1;
then
A14: 1 in dom f by A3,TOPS_2:def 5;
rng f=[#]((TOP-REAL n)|P) by A3,TOPS_2:def 5;
then
A15: f""=f by A9,TOPS_2:51;
rng g= [#](I[01]) by A6,TOPS_2:def 5;
then g is onto by FUNCT_2:def 3;
then
A16: g1" =f1 by A10,A15,TOPS_2:def 4;
g"(R)=g1"(the carrier of I[01])\g1"({0,1}) by FUNCT_1:69
.=((g1").:(the carrier of I[01]))\g1"({0,1}) by A10,FUNCT_1:85
.=f1.:([#](I[01]))\ f1.:({0,1}) by A10,A16,FUNCT_1:85
.=rng f\ f.:({0,1}) by A12,RELAT_1:113
.=[#]((TOP-REAL n)|P)\ f.:({0,1}) by A3,TOPS_2:def 5
.=P\ f.:({0,1}) by PRE_TOPC:def 5
.=Q by A2,A4,A5,A13,A14,FUNCT_1:60;
hence thesis by A7,A8,A11,TOPS_2:43;
end;
::A proof of the following is almost same as JORDAN5A:1.
theorem Th39:
for P,P1,P2 being Subset of TOP-REAL n, Q being Subset of (TOP-REAL n)|P,
p1,p2 being Point of TOP-REAL n st
P2 is_an_arc_of p1,p2
& P1 \/ P2 = P & P1 /\ P2={p1,p2} & Q=P1\{p1,p2} holds Q is open
proof
let P,P1,P2 be Subset of TOP-REAL n, Q be Subset of (TOP-REAL n)|P,
p1,p2 be Point of TOP-REAL n;
assume that
A1: P2 is_an_arc_of p1,p2 and
A2: P1 \/ P2 = P and
A3: P1 /\ P2={p1,p2} and
A4: Q=P1\{p1,p2};
reconsider P21=P2 as Subset of TOP-REAL n;
A5: P21 is compact by A1,JORDAN5A:1;
p1 in P1 /\ P2 by A3,TARSKI:def 2;
then
A6: p1 in P2 by XBOOLE_0:def 4;
A7: [#]((TOP-REAL n)|P)=P by PRE_TOPC:def 5;
then reconsider P29=P21 as Subset of (TOP-REAL n)|P by A2,XBOOLE_1:7;
p2 in P1 /\ P2 by A3,TARSKI:def 2;
then
A8: p2 in P2 by XBOOLE_0:def 4;
P29 is compact by A5,A7,COMPTS_1:2;
then
A9: P29 is closed by COMPTS_1:7;
A10: P\P2= (P1 \P2) \/ (P2\P2) by A2,XBOOLE_1:42
.=(P1\P2) \/ {} by XBOOLE_1:37
.=P1\P2;
A11: P1\P2 c= Q
proof
let x be object;
assume
A12: x in P1\P2;
then
A13: x in P1 by XBOOLE_0:def 5;
not x in P2 by A12,XBOOLE_0:def 5;
then not x in {p1,p2} by A6,A8,TARSKI:def 2;
hence thesis by A4,A13,XBOOLE_0:def 5;
end;
Q c= P1\P2
proof
let x be object;
assume
A14: x in Q;
then
A15: x in P1 by A4,XBOOLE_0:def 5;
not x in {p1,p2} by A4,A14,XBOOLE_0:def 5;
then not x in P2 by A3,A15,XBOOLE_0:def 4;
hence thesis by A15,XBOOLE_0:def 5;
end;
then P1\P2=Q by A11;
then Q=P29` by A7,A10,SUBSET_1:def 4;
hence thesis by A9,TOPS_1:3;
end;
theorem Th40:
for P being Subset of TOP-REAL n, Q being Subset of (TOP-REAL n)|P,
p1,p2 being Point of TOP-REAL n st
P is_an_arc_of p1,p2 & Q=P\{p1,p2} holds Q is connected
proof
let P be Subset of TOP-REAL n, Q be Subset of (TOP-REAL n)|P,
p1,p2 be Point of TOP-REAL n;
assume that
A1: P is_an_arc_of p1,p2 and
A2: Q=P\{p1,p2};
reconsider P9 = P as non empty Subset of TOP-REAL n by A1,TOPREAL1:1;
consider f being Function of I[01], (TOP-REAL n)|P9 such that
A3: f is being_homeomorphism and
A4: f.0 = p1 and
A5: f.1 = p2 by A1,TOPREAL1:def 1;
reconsider P7=(the carrier of I[01]) \{0,1} as Subset of I[01];
A6: f is continuous by A3,TOPS_2:def 5;
A7: f is one-to-one by A3,TOPS_2:def 5;
Q=f.:P7
proof
[#]((TOP-REAL n)|P)=P by PRE_TOPC:def 5;
then
A8: rng f=P by A3,TOPS_2:def 5;
thus Q c= f.:P7
proof
let x be object;
assume
A9: x in Q;
then
A10: x in P by A2,XBOOLE_0:def 5;
A11: not x in {p1,p2} by A2,A9,XBOOLE_0:def 5;
consider z being object such that
A12: z in dom f and
A13: x=f.z by A8,A10,FUNCT_1:def 3;
now
assume z in {0,1};
then x=p1 or x=p2 by A4,A5,A13,TARSKI:def 2;
hence contradiction by A11,TARSKI:def 2;
end;
then z in P7 by A12,XBOOLE_0:def 5;
hence thesis by A12,A13,FUNCT_1:def 6;
end;
let y be object;
assume y in f.:P7;
then consider x being object such that
A14: x in dom f and
A15: x in P7 and
A16: y=f.x by FUNCT_1:def 6;
A17: not x in {0,1} by A15,XBOOLE_0:def 5;
then
A18: x<>0 by TARSKI:def 2;
A19: x<>1 by A17,TARSKI:def 2;
A20: y in P by A8,A14,A16,FUNCT_1:def 3;
now
assume
A21: y in {p1,p2};
reconsider f1=f as Function of the carrier of I[01],
the carrier of (TOP-REAL n)|P9;
now per cases by A16,A21,TARSKI:def 2;
case
A22: f.x=p1;
dom f1=the carrier of I[01] by FUNCT_2:def 1;
then 0 in dom f1 by BORSUK_1:40,XXREAL_1:1;
hence contradiction by A4,A7,A14,A18,A22,FUNCT_1:def 4;
end;
case
A23: f.x=p2;
dom f1=the carrier of I[01] by FUNCT_2:def 1;
then 1 in dom f1 by BORSUK_1:40,XXREAL_1:1;
hence contradiction by A5,A7,A14,A19,A23,FUNCT_1:def 4;
end;
end;
hence contradiction;
end;
hence thesis by A2,A20,XBOOLE_0:def 5;
end;
hence thesis by A6,Th36,TOPS_2:61;
end;
theorem Th41:
for GX being TopSpace, P1, P being Subset of GX, Q9 being Subset of GX|P1,
Q being Subset of GX|P st P1 c=P & Q=Q9 &
Q9 is connected holds Q is connected
proof
let GX be TopSpace, P1, P be Subset of GX, Q9 be Subset of GX|P1,
Q be Subset of GX|P;
assume that
A1: P1 c=P and
A2: Q=Q9 and
A3: Q9 is connected;
[#](GX|P)=P by PRE_TOPC:def 5;
then reconsider P19=P1 as Subset of GX|P by A1;
GX|P1=(GX|P)|P19 by A1,PRE_TOPC:7;
hence thesis by A2,A3,CONNSP_1:23;
end;
theorem Th42:
for P being Subset of TOP-REAL n, p1,p2 being Point of TOP-REAL n st
P is_an_arc_of p1,p2 ex p3 being Point of TOP-REAL n st
p3 in P & p3<>p1 & p3<>p2
proof
let P be Subset of TOP-REAL n, p1,p2 be Point of TOP-REAL n;
assume P is_an_arc_of p1,p2;
then consider f being Function of I[01], (TOP-REAL n)|P such that
A1: f is being_homeomorphism and
A2: f.0 = p1 and
A3: f.1 = p2 by TOPREAL1:def 1;
1/2 in [#]I[01] by BORSUK_1:40,XXREAL_1:1;
then
A4: 1/2 in dom f by A1,TOPS_2:def 5;
then f.(1/2) in rng f by FUNCT_1:def 3;
then f.(1/2) in the carrier of ((TOP-REAL n)|P);
then
A5: f.(1/2) in P by PRE_TOPC:8;
then reconsider p=f.(1/2) as Point of TOP-REAL n;
A6: f is one-to-one by A1,TOPS_2:def 5;
0 in [#](I[01]) by BORSUK_1:40,XXREAL_1:1;
then 0 in dom f by A1,TOPS_2:def 5;
then
A7: p1<>p by A2,A4,A6,FUNCT_1:def 4;
1 in [#](I[01]) by BORSUK_1:40,XXREAL_1:1;
then 1 in dom f by A1,TOPS_2:def 5;
then f.1<>f.(1/2) by A4,A6,FUNCT_1:def 4;
hence thesis by A3,A5,A7;
end;
theorem
for P being Subset of TOP-REAL n,
p1,p2 being Point of TOP-REAL n st P is_an_arc_of p1,p2 holds P\{p1,p2}<>{}
proof
let P be Subset of TOP-REAL n, p1,p2 be Point of TOP-REAL n;
assume P is_an_arc_of p1,p2;
then consider p3 being Point of TOP-REAL n such that
A1: p3 in P and
A2: p3<>p1 and
A3: p3<>p2 by Th42;
not p3 in {p1,p2} by A2,A3,TARSKI:def 2;
hence thesis by A1,XBOOLE_0:def 5;
end;
theorem
for P1 being Subset of TOP-REAL n, P being Subset of TOP-REAL n,
Q being Subset of (TOP-REAL n)|P, p1,p2 being Point of TOP-REAL n st
P1 is_an_arc_of p1,p2 & P1 c=P & Q=P1\{p1,p2} holds Q is connected
proof
let P1 be Subset of TOP-REAL n, P be Subset of TOP-REAL n,
Q be Subset of (TOP-REAL n)|P, p1,p2 be Point of TOP-REAL n;
assume that
A1: P1 is_an_arc_of p1,p2 and
A2: P1 c=P and
A3: Q=P1\{p1,p2};
[#]((TOP-REAL n)|P1)=P1 by PRE_TOPC:def 5;
then reconsider Q9=Q as Subset of (TOP-REAL n)|P1 by A3,XBOOLE_1:36;
Q9 is connected by A1,A3,Th40;
hence thesis by A2,Th41;
end;
theorem Th45:
for T,S,V being non empty TopSpace, P1 being non empty Subset of S,
P2 being Subset of S,
f being Function of T,S|P1, g being Function of S|P2,V st
P1 c= P2 & f is continuous & g is continuous
ex h being Function of T,V st h=g*f & h is continuous
proof
let T,S,V be non empty TopSpace, P1 be non empty Subset of S,
P2 be Subset of S, f be Function of T,S|P1, g be Function of S|P2,V;
assume that
A1: P1 c= P2 and
A2: f is continuous and
A3: g is continuous;
reconsider P3 = P2 as non empty Subset of S by A1,XBOOLE_1:3;
A4: [#](S|P1)=P1 by PRE_TOPC:def 5;
A5: [#](S|P2)=P2 by PRE_TOPC:def 5;
then reconsider f1=f as Function of T,S|P3 by A1,A4,FUNCT_2:7;
for F1 being Subset of S|P2 st F1 is closed holds f1"F1 is closed
proof
let F1 be Subset of S|P2;
assume
A6: F1 is closed;
reconsider P19=P1 as non empty Subset of S|P3 by A1,A5;
A7: [#](S|P1)=P1 by PRE_TOPC:def 5;
reconsider P4=F1/\P19 as Subset of (S|P3)|P19 by TOPS_2:29;
A8: S|P1=(S|P3)|P19 by A1,PRE_TOPC:7;
A9: P4 is closed by A6,Th2;
f1"P1=the carrier of T by A7,FUNCT_2:40
.=dom f1 by FUNCT_2:def 1;
then f1"F1=f1"F1 /\ f1"P1 by RELAT_1:132,XBOOLE_1:28
.=f"P4 by FUNCT_1:68;
hence thesis by A2,A8,A9;
end;
then f1 is continuous;
hence thesis by A3;
end;
theorem Th46:
for P1,P2 being Subset of TOP-REAL n, p1,p2 being Point of TOP-REAL n st
P1 is_an_arc_of p1,p2 & P2 is_an_arc_of p1,p2 & P1 c= P2 holds P1=P2
proof
let P1,P2 be Subset of TOP-REAL n, p1,p2 be Point of TOP-REAL n;
assume that
A1: P1 is_an_arc_of p1,p2 and
A2: P2 is_an_arc_of p1,p2 and
A3: P1 c= P2;
reconsider P19 = P1, P29 = P2
as non empty Subset of TOP-REAL n by A1,A2,TOPREAL1:1;
now
assume
A4: P2\P1<>{};
set p = the Element of P2\P1;
A5: p in P2 by A4,XBOOLE_0:def 5;
A6: not p in P1 by A4,XBOOLE_0:def 5;
consider f1 being Function of I[01],(TOP-REAL n)|P19 such that
A7: f1 is being_homeomorphism and
A8: f1.0=p1 and
A9: f1.1=p2 by A1,TOPREAL1:def 1;
A10: f1 is continuous by A7,TOPS_2:def 5;
consider f2 being Function of I[01],(TOP-REAL n)|P29 such that
A11: f2 is being_homeomorphism and
A12: f2.0=p1 and
A13: f2.1=p2 by A2,TOPREAL1:def 1;
reconsider f4=f2 as Function;
A14: f2 is one-to-one by A11,TOPS_2:def 5;
A15: rng f2=[#]((TOP-REAL n)|P2) by A11,TOPS_2:def 5;
A16: f2" is being_homeomorphism by A11,TOPS_2:56;
then
A17: dom (f2")=[#]((TOP-REAL n)|P2) by TOPS_2:def 5
.=P2 by PRE_TOPC:def 5;
f2" is continuous by A11,TOPS_2:def 5;
then consider h being Function of I[01],I[01] such that
A18: h=f2"*f1 and
A19: h is continuous by A3,A10,Th45;
reconsider h1=h as Function of Closed-Interval-TSpace(0,1),R^1
by BORSUK_1:40,FUNCT_2:7,TOPMETR:17,20;
for F1 being Subset of R^1 st F1 is closed holds h1"F1 is closed
proof
let F1 be Subset of R^1;
assume
A20: F1 is closed;
reconsider K=the carrier of I[01]
as Subset of R^1 by BORSUK_1:40,TOPMETR:17;
A21: I[01]=R^1|K by BORSUK_1:40,TOPMETR:19,20;
reconsider P3=F1/\K as Subset of R^1|K by TOPS_2:29;
A22: P3 is closed by A20,Th2;
h1"K=the carrier of I[01] by FUNCT_2:40
.=dom h1 by FUNCT_2:def 1;
then h1"F1=h1"F1 /\ h1"K by RELAT_1:132,XBOOLE_1:28
.=h"P3 by FUNCT_1:68;
hence thesis by A19,A21,A22,TOPMETR:20;
end;
then reconsider g=h1 as continuous Function of
Closed-Interval-TSpace(0,1),R^1 by PRE_TOPC:def 6;
A23: dom f1 =[#](I[01]) by A7,TOPS_2:def 5
.=[.0,1.] by BORSUK_1:40;
then
A24: 0 in dom f1 by XXREAL_1:1;
A25: 1 in dom f1 by A23,XXREAL_1:1;
A26: g.0=f2".p1 by A8,A18,A24,FUNCT_1:13;
A27: g.1=f2".p2 by A9,A18,A25,FUNCT_1:13;
A28: dom f2 =[#](I[01]) by A11,TOPS_2:def 5
.=[.0,1.] by BORSUK_1:40;
then
A29: 0 in dom f2 by XXREAL_1:1;
A30: 1 in dom f2 by A28,XXREAL_1:1;
A31: f2 is onto by A15,FUNCT_2:def 3;
then
A32: (f2").p1=(f4").p1 by A14,TOPS_2:def 4;
A33: ((f2)").p2=(f4").p2 by A14,A31,TOPS_2:def 4;
A34: g.0=0 by A12,A14,A26,A29,A32,FUNCT_1:32;
A35: g.1=1 by A13,A14,A27,A30,A33,FUNCT_1:32;
p in the carrier of (TOP-REAL n)|P29 by A5,PRE_TOPC:8;
then
A36: f2".p in the carrier of I[01] by FUNCT_2:5;
A37: now
assume f2".p in rng g;
then consider x being object such that
A38: x in dom g and
A39: f2".p=g.x by FUNCT_1:def 3;
A40: f2".p=f2".(f1.x) by A18,A38,A39,FUNCT_1:12;
A41: x in dom f1 by A18,A38,FUNCT_1:11;
A42: f1.x in dom (f2") by A18,A38,FUNCT_1:11;
f2" is one-to-one by A16,TOPS_2:def 5;
then p=f1.x by A5,A17,A40,A42,FUNCT_1:def 4;
then
A43: p in rng f1 by A41,FUNCT_1:def 3;
rng f1 =[#]((TOP-REAL n)|P1) by A7,TOPS_2:def 5
.=P1 by PRE_TOPC:def 5;
hence contradiction by A4,A43,XBOOLE_0:def 5;
end;
reconsider r=f2".p as Real;
A44: rng f2=[#]((TOP-REAL n)|P2) by A11,TOPS_2:def 5
.=P2 by PRE_TOPC:def 5;
A45: r<=1 by A36,BORSUK_1:40,XXREAL_1:1;
A46: now
assume
A47: r=0;
f2.r=f4.((f4").p) by A31,A14,TOPS_2:def 4
.=p by A5,A14,A44,FUNCT_1:35;
hence contradiction by A1,A6,A12,A47,TOPREAL1:1;
end;
A48: now
assume
A49: r=1;
f2.r= f4.((f4").p) by A31,A14,TOPS_2:def 4
.=p by A5,A14,A44,FUNCT_1:35;
hence contradiction by A1,A6,A13,A49,TOPREAL1:1;
end;
A50: 0<r by A36,A46,BORSUK_1:40,XXREAL_1:1;
r<1 by A45,A48,XXREAL_0:1;
then consider rc being Real such that
A51: g.rc=r and
A52: 0<rc and
A53: rc <1 by A34,A35,A50,TOPREAL5:6;
the carrier of (TOP-REAL n)|P1 = [#]((TOP-REAL n)|P1)
.=P1 by PRE_TOPC:def 5;
then rng f1 c= dom (f2") by A3,A17;
then dom g=dom f1 by A18,RELAT_1:27
.=[#](I[01]) by A7,TOPS_2:def 5
.=[.0,1.] by BORSUK_1:40;
then rc in dom g by A52,A53,XXREAL_1:1;
hence contradiction by A37,A51,FUNCT_1:def 3;
end;
then P2 c= P1 by XBOOLE_1:37;
hence thesis by A3;
end;
theorem Th47:
for P being Subset of TOP-REAL 2, Q being Subset of (TOP-REAL 2)|P,
p1,p2 being Point of TOP-REAL 2
st P is being_simple_closed_curve & p1 in P & p2 in P & p1<>p2 & Q=P\{p1,p2}
holds not Q is connected
proof
let P be Subset of TOP-REAL 2, Q be Subset of (TOP-REAL 2)|P,
p1,p2 be Point of TOP-REAL 2;
assume that
A1: P is being_simple_closed_curve and
A2: p1 in P and
A3: p2 in P and
A4: p1<>p2 and
A5: Q=P\{p1,p2};
consider P1,P2 being non empty Subset of TOP-REAL 2 such that
A6: P1 is_an_arc_of p1,p2 and
A7: P2 is_an_arc_of p1,p2 and
A8: P = P1 \/ P2 and
A9: P1 /\ P2 = {p1,p2} by A1,A2,A3,A4,TOPREAL2:5;
A10: [#]((TOP-REAL 2)|P)=P by PRE_TOPC:def 5;
reconsider P as Simple_closed_curve by A1;
A11: P1 c= P by A8,XBOOLE_1:7;
P1\{p1,p2} c= P1 by XBOOLE_1:36;
then reconsider P19=P1\{p1,p2} as Subset of (TOP-REAL 2)|P
by A10,A11,XBOOLE_1:1;
A12: P2 c= P by A8,XBOOLE_1:7;
P2\{p1,p2} c= P2 by XBOOLE_1:36;
then reconsider P29=P2\{p1,p2} as Subset of (TOP-REAL 2)|P
by A10,A12,XBOOLE_1:1;
A13: P19 is open by A7,A8,A9,Th39;
A14: P29 is open by A6,A8,A9,Th39;
A15: Q c= P19 \/ P29
proof
let x be object;
assume
A16: x in Q;
then
A17: x in P by A5,XBOOLE_0:def 5;
now per cases by A5,A8,A16,A17,XBOOLE_0:def 3,def 5;
case x in P1 & not x in {p1,p2};
then x in P19 by XBOOLE_0:def 5;
hence thesis by XBOOLE_0:def 3;
end;
case x in P2 & not x in {p1,p2};
then x in P29 by XBOOLE_0:def 5;
hence thesis by XBOOLE_0:def 3;
end;
end;
hence thesis;
end;
consider p3 being Point of TOP-REAL 2 such that
A18: p3 in P1 and
A19: p3<>p1 and
A20: p3<>p2 by A6,Th42;
not p3 in {p1,p2} by A19,A20,TARSKI:def 2;
then
A21: P19<>{} by A18,XBOOLE_0:def 5;
P19 c= Q
proof
let x be object;
assume
A22: x in P19;
then
A23: x in P1 by XBOOLE_0:def 5;
A24: not x in {p1,p2} by A22,XBOOLE_0:def 5;
x in P by A8,A23,XBOOLE_0:def 3;
hence thesis by A5,A24,XBOOLE_0:def 5;
end;
then (P19 /\ Q) <>{} by A21,XBOOLE_1:28;
then
A25: P19 meets Q;
consider p39 being Point of TOP-REAL 2 such that
A26: p39 in P2 and
A27: p39<>p1 and
A28: p39<>p2 by A7,Th42;
not p39 in {p1,p2} by A27,A28,TARSKI:def 2;
then
A29: P29<>{} by A26,XBOOLE_0:def 5;
P29 c= Q
proof
let x be object;
assume
A30: x in P29;
then
A31: x in P2 by XBOOLE_0:def 5;
A32: not x in {p1,p2} by A30,XBOOLE_0:def 5;
x in P1 \/ P2 by A31,XBOOLE_0:def 3;
hence thesis by A5,A8,A32,XBOOLE_0:def 5;
end;
then P29 /\ Q<>{} by A29,XBOOLE_1:28;
then
A33: P29 meets Q;
now
assume P19 meets P29;
then consider p0 being object such that
A34: p0 in P19 and
A35: p0 in P29 by XBOOLE_0:3;
A36: p0 in P1 by A34,XBOOLE_0:def 5;
A37: not p0 in {p1,p2} by A34,XBOOLE_0:def 5;
p0 in P2 by A35,XBOOLE_0:def 5;
hence contradiction by A9,A36,A37,XBOOLE_0:def 4;
end;
hence thesis by A13,A14,A15,A25,A33,TOPREAL5:1;
end;
theorem Th48:
for P,P1,P2,P19,P29 being Subset of TOP-REAL 2,
p1,p2 being Point of TOP-REAL 2 st P is being_simple_closed_curve
& P1 is_an_arc_of p1,p2 & P2 is_an_arc_of p1,p2 & P1 \/ P2=P
& P19 is_an_arc_of p1,p2 & P29 is_an_arc_of p1,p2 & P19 \/ P29=P
holds P1=P19 & P2=P29 or P1=P29 & P2=P19
proof
let P,P1,P2,P19,P29 be Subset of
the carrier of TOP-REAL 2,p1,p2 be Point of TOP-REAL 2;
assume that
A1: P is being_simple_closed_curve and
A2: P1 is_an_arc_of p1,p2 and
A3: P2 is_an_arc_of p1,p2 and
A4: P1 \/ P2=P and
A5: P19 is_an_arc_of p1,p2 and
A6: P29 is_an_arc_of p1,p2 and
A7: P19 \/ P29=P;
reconsider P as Simple_closed_curve by A1;
A8: p1<>p2 by A6,Th37;
A9: p1 in P19 by A5,TOPREAL1:1;
A10: p2 in P19 by A5,TOPREAL1:1;
A11: p1 in P2 by A3,TOPREAL1:1;
A12: p2 in P2 by A3,TOPREAL1:1;
A13: p1 in P1 by A2,TOPREAL1:1;
A14: p2 in P1 by A2,TOPREAL1:1;
A15: P1 c= P by A4,XBOOLE_1:7;
A16: [#]((TOP-REAL 2)|P)=P by PRE_TOPC:def 5;
P1\{p1,p2} c= P1 by XBOOLE_1:36;
then reconsider Q1=P1\{p1,p2} as Subset of (TOP-REAL 2)|P by A15,A16,
XBOOLE_1:1;
A17: P2 c= P by A4,XBOOLE_1:7;
P2\{p1,p2} c= P2 by XBOOLE_1:36;
then reconsider Q2=P2\{p1,p2} as Subset of (TOP-REAL 2)|P by A16,A17,
XBOOLE_1:1;
A18: P19 c= P by A7,XBOOLE_1:7;
P19\{p1,p2} c= P19 by XBOOLE_1:36;
then reconsider Q19=P19\{p1,p2} as Subset of (TOP-REAL 2)|P by A16,A18,
XBOOLE_1:1;
A19: P29 c= P by A7,XBOOLE_1:7;
P29\{p1,p2} c= P29 by XBOOLE_1:36;
then reconsider Q29=P29\{p1,p2} as Subset of (TOP-REAL 2)|P by A16,A19,
XBOOLE_1:1;
A20: Q1 \/ Q2 =P\{p1,p2} by A4,XBOOLE_1:42;
A21: Q19 \/ Q29 =P\{p1,p2} by A7,XBOOLE_1:42;
then
A22: Q19 \/ (Q1 \/ Q2)=Q1 \/ Q2 by A20,XBOOLE_1:7,12;
A23: Q29 \/ (Q1 \/ Q2)=Q1 \/ Q2 by A20,A21,XBOOLE_1:7,12;
A24: Q1 \/ (Q19 \/ Q29)=Q19 \/ Q29 by A20,A21,XBOOLE_1:7,12;
A25: Q2 \/ (Q19 \/ Q29)=Q19 \/ Q29 by A20,A21,XBOOLE_1:7,12;
[#]((TOP-REAL 2)|P1)=P1 by PRE_TOPC:def 5;
then reconsider R1=Q1 as Subset of (TOP-REAL 2)|P1 by XBOOLE_1:36;
R1 is connected by A2,Th40;
then
A26: Q1 is connected by A4,Th41,XBOOLE_1:7;
[#]((TOP-REAL 2)|P2)=P2 by PRE_TOPC:def 5;
then reconsider R2=Q2 as Subset of (TOP-REAL 2)|P2 by XBOOLE_1:36;
R2 is connected by A3,Th40;
then
A27: Q2 is connected by A4,Th41,XBOOLE_1:7;
[#]((TOP-REAL 2)|P19)=P19 by PRE_TOPC:def 5;
then reconsider R19=Q19 as Subset of (TOP-REAL 2)|P19 by XBOOLE_1:36;
R19 is connected by A5,Th40;
then
A28: Q19 is connected by A7,Th41,XBOOLE_1:7;
[#]((TOP-REAL 2)|P29)=P29 by PRE_TOPC:def 5;
then reconsider R29=Q29 as Subset of (TOP-REAL 2)|P29 by XBOOLE_1:36;
R29 is connected by A6,Th40;
then
A29: Q29 is connected by A7,Th41,XBOOLE_1:7;
A30: {p1,p2} c= P1
by A13,A14,TARSKI:def 2;
A31: {p1,p2} c= P2
by A11,A12,TARSKI:def 2;
A32: {p1,p2} c= P19
by A9,A10,TARSKI:def 2;
A33: {p1,p2} c= P29
proof
let x be object;
assume x in {p1,p2};
then x=p1 or x=p2 by TARSKI:def 2;
hence thesis by A6,TOPREAL1:1;
end;
A34: Q1 \/ {p1,p2}=P1 by A30,XBOOLE_1:45;
A35: Q2 \/ {p1,p2}=P2 by A31,XBOOLE_1:45;
A36: Q19 \/ {p1,p2}=P19 by A32,XBOOLE_1:45;
A37: Q29 \/ {p1,p2}=P29 by A33,XBOOLE_1:45;
now
assume
A38: not(P1=P29 & P2=P19);
now per cases by A38;
case
A39: P1<>P29;
A40: now
assume that
A41: Q1\Q29={} and
A42: Q29\Q1={};
A43: Q1 c= Q29 by A41,XBOOLE_1:37;
Q29 c= Q1 by A42,XBOOLE_1:37;
hence contradiction by A34,A37,A39,A43,XBOOLE_0:def 10;
end;
now per cases by A40;
case
A44: Q1\Q29<>{};
set y = the Element of Q1\Q29;
A45: y in Q1 by A44,XBOOLE_0:def 5;
then
A46: y in Q19 \/ Q29 by A20,A21,XBOOLE_0:def 3;
not y in Q29 by A44,XBOOLE_0:def 5;
then y in Q19 by A46,XBOOLE_0:def 3;
then Q1 /\ Q19<>{} by A45,XBOOLE_0:def 4;
then
A47: Q1 meets Q19;
now
assume Q2 meets Q19;
then Q1 \/ Q19 \/ Q2 is connected by A26,A27,A28,A47,JORDAN1:4;
hence contradiction by A8,A13,A14,A15,A20,A22,Th47,XBOOLE_1:4;
end;
then
A48: Q2/\Q19={};
A49: Q2 c= Q29
proof
let x be object;
assume
A50: x in Q2;
then x in Q1 \/ Q2 by XBOOLE_0:def 3;
then x in Q19 or x in Q29 by A20,A21,XBOOLE_0:def 3;
hence thesis by A48,A50,XBOOLE_0:def 4;
end;
Q19 c= Q1
proof
let x be object;
assume
A51: x in Q19;
then x in Q1 \/ Q2 by A20,A21,XBOOLE_0:def 3;
then x in Q1 or x in Q2 by XBOOLE_0:def 3;
hence thesis by A48,A51,XBOOLE_0:def 4;
end;
hence thesis by A2,A3,A5,A6,A34,A35,A36,A37,A49,Th46,XBOOLE_1:9;
end;
case
A52: Q29\Q1<>{};
set y = the Element of Q29\Q1;
A53: y in Q29 by A52,XBOOLE_0:def 5;
then
A54: y in Q2 \/ Q1 by A20,A21,XBOOLE_0:def 3;
not y in Q1 by A52,XBOOLE_0:def 5;
then y in Q2 by A54,XBOOLE_0:def 3;
then Q29 /\ Q2<>{} by A53,XBOOLE_0:def 4;
then
A55: Q29 meets Q2;
now
assume Q19 meets Q2;
then Q29 \/ Q2 \/ Q19 is connected by A27,A28,A29,A55,JORDAN1:4;
hence contradiction by A8,A13,A14,A15,A21,A25,Th47,XBOOLE_1:4;
end;
then
A56: Q19/\Q2={};
A57: Q19 c= Q1
proof
let x be object;
assume
A58: x in Q19;
then x in Q19 \/ Q29 by XBOOLE_0:def 3;
then x in Q1 or x in Q2 by A20,A21,XBOOLE_0:def 3;
hence thesis by A56,A58,XBOOLE_0:def 4;
end;
Q2 c= Q29
proof
let x be object;
assume
A59: x in Q2;
then x in Q2 \/ Q1 by XBOOLE_0:def 3;
then x in Q29 or x in Q19 by A20,A21,XBOOLE_0:def 3;
hence thesis by A56,A59,XBOOLE_0:def 4;
end;
hence thesis by A2,A3,A5,A6,A34,A35,A36,A37,A57,Th46,XBOOLE_1:9;
end;
end;
hence thesis;
end;
case
A60: P2<>P19;
A61: now
assume that
A62: Q2\Q19={} and
A63: Q19\Q2={};
A64: Q2 c= Q19 by A62,XBOOLE_1:37;
Q19 c= Q2 by A63,XBOOLE_1:37;
hence contradiction by A35,A36,A60,A64,XBOOLE_0:def 10;
end;
now per cases by A61;
case
A65: Q2\Q19<>{};
set y = the Element of Q2\Q19;
A66: y in Q2 by A65,XBOOLE_0:def 5;
then
A67: y in Q29 \/ Q19 by A20,A21,XBOOLE_0:def 3;
not y in Q19 by A65,XBOOLE_0:def 5;
then y in Q29 by A67,XBOOLE_0:def 3;
then Q2 /\ Q29<>{} by A66,XBOOLE_0:def 4;
then
A68: Q2 meets Q29;
now
assume Q1 meets Q29;
then Q2 \/ Q29 \/ Q1 is connected by A26,A27,A29,A68,JORDAN1:4;
hence contradiction by A8,A13,A14,A15,A20,A23,Th47,XBOOLE_1:4;
end;
then
A69: Q1/\Q29={};
A70: Q1 c= Q19
proof
let x be object;
assume
A71: x in Q1;
then x in Q2 \/ Q1 by XBOOLE_0:def 3;
then x in Q29 or x in Q19 by A20,A21,XBOOLE_0:def 3;
hence thesis by A69,A71,XBOOLE_0:def 4;
end;
Q29 c= Q2
proof
let x be object;
assume
A72: x in Q29;
then x in Q2 \/ Q1 by A20,A21,XBOOLE_0:def 3;
then x in Q2 or x in Q1 by XBOOLE_0:def 3;
hence thesis by A69,A72,XBOOLE_0:def 4;
end;
hence thesis by A2,A3,A5,A6,A34,A35,A36,A37,A70,Th46,XBOOLE_1:9;
end;
case
A73: Q19\Q2<>{};
set y = the Element of Q19\Q2;
A74: y in Q19 by A73,XBOOLE_0:def 5;
then
A75: y in Q1 \/ Q2 by A20,A21,XBOOLE_0:def 3;
not y in Q2 by A73,XBOOLE_0:def 5;
then y in Q1 by A75,XBOOLE_0:def 3;
then Q19 /\ Q1<>{} by A74,XBOOLE_0:def 4;
then
A76: Q19 meets Q1;
now
assume Q29 meets Q1;
then Q19 \/ Q1 \/ Q29 is connected by A26,A28,A29,A76,JORDAN1:4;
hence contradiction by A8,A13,A14,A15,A21,A24,Th47,XBOOLE_1:4;
end;
then
A77: Q29 /\ Q1 = {};
A78: Q29 c= Q2
proof
let x be object;
assume
A79: x in Q29;
then x in Q29 \/ Q19 by XBOOLE_0:def 3;
then x in Q2 or x in Q1 by A20,A21,XBOOLE_0:def 3;
hence thesis by A77,A79,XBOOLE_0:def 4;
end;
Q1 c= Q19
proof
let x be object;
assume
A80: x in Q1;
then x in Q19 \/ Q29 by A20,A21,XBOOLE_0:def 3;
then x in Q19 or x in Q29 by XBOOLE_0:def 3;
hence thesis by A77,A80,XBOOLE_0:def 4;
end;
hence thesis by A2,A3,A5,A6,A34,A35,A36,A37,A78,Th46,XBOOLE_1:9;
end;
end;
hence thesis;
end;
end;
hence thesis;
end;
hence thesis;
end;
begin ::Lower Arcs and Upper Arcs
Lm1: for g being Function of I[01],R^1,
s1,s2,r being Real st g is continuous &
g.0[01] < r & r < g.1[01]
ex r1 st 0<r1 & r1<1 & g.r1=r
proof
let g be Function of I[01],R^1,s1,s2,r be Real;
assume that
A1: g is continuous and
A2: g.0[01] < r and
A3: r < g.1[01];
ex rc being Real st
g.rc=r & 0<rc & rc <1 by A1,A2,A3,BORSUK_1:def 14,def 15,TOPMETR:20
,TOPREAL5:6;
hence thesis;
end;
theorem Th49:
for P1 being Subset of TOP-REAL 2,
r being Real,p1,p2 being Point of TOP-REAL 2 st
p1`1<=r & r<=p2`1 & P1 is_an_arc_of p1,p2 holds P1 meets Vertical_Line(r) &
P1 /\ Vertical_Line(r) is closed
proof
let P1 be Subset of TOP-REAL 2, r be Real,
p1,p2 be Point of TOP-REAL 2;
assume that
A1: p1`1<=r and
A2: r<=p2`1 and
A3: P1 is_an_arc_of p1,p2;
reconsider P19 = P1 as non empty Subset of TOP-REAL 2 by A3,TOPREAL1:1;
consider f being Function of I[01], (TOP-REAL 2)|P19 such that
A4: f is being_homeomorphism and
A5: f.0 = p1 and
A6: f.1 = p2 by A3,TOPREAL1:def 1;
A7: [#]((TOP-REAL 2)|P1)=P1 by PRE_TOPC:def 5;
then reconsider f1=f as Function of the carrier of I[01],
the carrier of TOP-REAL 2 by FUNCT_2:7;
reconsider f2=f1 as Function of I[01],TOP-REAL 2;
reconsider proj11=proj1 as Function of the carrier of TOP-REAL 2,REAL;
reconsider proj12=proj1 as Function of TOP-REAL 2,R^1 by TOPMETR:17;
reconsider g1=proj11*f1 as Function of the carrier of I[01],REAL;
reconsider g=g1 as Function of I[01],R^1 by TOPMETR:17;
f is continuous by A4,TOPS_2:def 5;
then
A8: f2 is continuous by Th3;
A9: proj12 is continuous by TOPREAL5:10;
A10: dom f=[.0,1.] by BORSUK_1:40,FUNCT_2:def 1;
then
A11: 0 in dom f by XXREAL_1:1;
A12: 1 in dom f by A10,XXREAL_1:1;
A13: g.0=proj1.p1 by A5,A11,FUNCT_1:13
.=p1`1 by PSCOMP_1:def 5;
A14: g.1=proj1.p2 by A6,A12,FUNCT_1:13
.=p2`1 by PSCOMP_1:def 5;
reconsider P19 as non empty Subset of TOP-REAL 2;
A15: P19 is closed by A3,COMPTS_1:7,JORDAN5A:1;
A16: Vertical_Line(r) is closed by Th6;
now per cases by A1,A2,A13,A14,BORSUK_1:def 14,def 15,XXREAL_0:1;
case g.0=g.1;
then
A17: g.0=r by A1,A2,A13,A14,XXREAL_0:1;
A18: f.0 in rng f by A11,FUNCT_1:def 3;
then f.0 in P1 by A7;
then reconsider p=f.0 as Point of TOP-REAL 2;
p`1=proj1.(f.0) by PSCOMP_1:def 5
.=r by A11,A17,FUNCT_1:13;
then f.0 in {q where q is Point of TOP-REAL 2: q`1=r};
hence P1 meets Vertical_Line(r) by A7,A18,XBOOLE_0:3;
end;
case
A19: g.0[01]=r;
A20: f.0 in rng f by A11,FUNCT_1:def 3;
then f.0 in P19 by A7;
then reconsider p=f.0 as Point of TOP-REAL 2;
p`1=proj1.(f.0) by PSCOMP_1:def 5
.=r by A11,A19,BORSUK_1:def 14,FUNCT_1:13;
then f.0 in {q where q is Point of TOP-REAL 2: q`1=r};
hence P1 meets Vertical_Line(r) by A7,A20,XBOOLE_0:3;
end;
case
A21: g.1[01]=r;
A22: f.1 in rng f by A12,FUNCT_1:def 3;
then f.1 in P1 by A7;
then reconsider p=f.1 as Point of TOP-REAL 2;
p`1=proj1.(f.1) by PSCOMP_1:def 5
.=r by A12,A21,BORSUK_1:def 15,FUNCT_1:13;
then f.1 in {q where q is Point of TOP-REAL 2: q`1=r};
hence P1 meets Vertical_Line(r) by A7,A22,XBOOLE_0:3;
end;
case g.0[01]< r & r < g.1[01];
then consider r1 such that
A23: 0<r1 and
A24: r1<1 and
A25: g.r1=r by A8,A9,Lm1;
dom f=[.0,1.] by BORSUK_1:40,FUNCT_2:def 1;
then
A26: r1 in dom f by A23,A24,XXREAL_1:1;
A27: [#]((TOP-REAL 2)|P1)=P1 by PRE_TOPC:def 5;
A28: f.r1 in rng f by A26,FUNCT_1:def 3;
then f.r1 in P19 by A27;
then reconsider p=f.r1 as Point of TOP-REAL 2;
p`1=proj1.(f.r1) by PSCOMP_1:def 5
.=r by A25,A26,FUNCT_1:13;
then f.r1 in {q where q is Point of TOP-REAL 2: q`1=r};
hence P1 meets Vertical_Line(r) by A27,A28,XBOOLE_0:3;
end;
end;
hence thesis by A15,A16,TOPS_1:8;
end;
Lm2: now
let P be Simple_closed_curve;
let P1,P19 be non empty Subset of TOP-REAL 2;
assume that
A1: ex P2 being non empty Subset of TOP-REAL 2 st P1 is_an_arc_of W-min(P)
,E-max(P) & P2 is_an_arc_of E-max(P),W-min(P) & P1 /\ P2={W-min(P),E-max(P)} &
P1 \/ P2=P & First_Point(P1,W-min(P),E-max(P), Vertical_Line((W-bound(P)+
E-bound(P))/2))`2> Last_Point(P2,E-max(P),W-min(P), Vertical_Line((W-bound(P)+
E-bound(P))/2))`2 and
A2: ex P29 being non empty Subset of TOP-REAL 2 st P19 is_an_arc_of
W-min(P),E-max(P) & P29 is_an_arc_of E-max(P),W-min(P) & P19 /\ P29={W-min(P),
E-max(P)} & P19 \/ P29=P & First_Point(P19,W-min(P),E-max(P), Vertical_Line((
W-bound(P)+E-bound(P))/2))`2> Last_Point(P29,E-max(P),W-min(P), Vertical_Line((
W-bound(P)+E-bound(P))/2))`2;
consider P2 being non empty Subset of TOP-REAL 2 such that
A3: P1 is_an_arc_of W-min(P),E-max(P) and
A4: P2 is_an_arc_of E-max(P),W-min(P) and P1 /\ P2={W-min(P),E-max(P)} and
A5: P1 \/ P2=P and
A6: First_Point(P1,W-min(P),E-max(P), Vertical_Line((W-bound(P)+E-bound(
P))/2))`2> Last_Point(P2,E-max(P),W-min(P), Vertical_Line((W-bound(P)+E-bound(P
))/2))`2
by A1;
A7: P2 is_an_arc_of W-min(P),E-max(P) by A4,JORDAN5B:14;
consider P29 being non empty Subset of TOP-REAL 2 such that
A8: P19 is_an_arc_of W-min(P),E-max(P) and
A9: P29 is_an_arc_of E-max(P),W-min(P) and P19 /\ P29={W-min(P),E-max(P)} and
A10: P19 \/ P29=P and
A11: First_Point(P19,W-min(P),E-max(P), Vertical_Line((W-bound(P)+E-bound
(P))/2))`2> Last_Point(P29,E-max(P),W-min(P), Vertical_Line((W-bound(P)+E-bound
(P))/2))`2
by A2;
A12: P29 is_an_arc_of W-min(P),E-max(P) by A9,JORDAN5B:14;
now
assume that
A13: P1=P29 and
A14: P2=P19;
A15: (W-min(P))`1=W-bound(P) by EUCLID:52;
A16: (E-max(P))`1=E-bound(P) by EUCLID:52;
then
A17: (W-min(P))`1<(E-max(P))`1 by A15,TOPREAL5:17;
then
A18: (W-min P)`1<=(W-bound(P)+E-bound(P))/2 by A15,A16,XREAL_1:226;
A19: (W-bound(P)+E-bound(P))/2<=(E-max P)`1 by A15,A16,A17,XREAL_1:226;
then
A20: P2 meets Vertical_Line((W-bound(P)+E-bound(P))/2) by A7,A18,Th49;
P2 /\ Vertical_Line((W-bound(P)+E-bound(P))/2) is closed by A7,A18,A19,Th49
;
then
A21: First_Point(P1,W-min(P),E-max(P),
Vertical_Line((W-bound(P)+E-bound(P))/2))`2>
First_Point(P2,W-min(P),E-max(P),
Vertical_Line((W-bound(P)+E-bound(P))/2))`2 by A4,A6,A20,JORDAN5C:18;
A22: P29 meets Vertical_Line((W-bound(P)+E-bound(P))/2) by A12,A18,A19,Th49;
P29 /\ Vertical_Line((W-bound(P)+E-bound(P))/2) is closed by A12,A18,A19
,Th49;
hence contradiction by A9,A11,A13,A14,A21,A22,JORDAN5C:18;
end;
hence P1=P19 by A3,A5,A7,A8,A10,A12,Th48;
end;
definition
let P be Subset of TOP-REAL 2 such that
A1: P is being_simple_closed_curve;
func Upper_Arc(P) -> non empty Subset of TOP-REAL 2 means
:Def8:
it is_an_arc_of W-min(P),E-max(P) &
ex P2 being non empty Subset of TOP-REAL 2 st
P2 is_an_arc_of E-max(P),W-min(P) & it /\ P2={W-min(P),E-max(P)}
& it \/ P2=P & First_Point(it,W-min(P),E-max(P),
Vertical_Line((W-bound(P)+E-bound(P))/2))`2>
Last_Point(P2,E-max(P),W-min(P),
Vertical_Line((W-bound(P)+E-bound(P))/2))`2;
existence
proof
ex P1,P2 being non empty Subset of TOP-REAL 2 st
P1 is_an_arc_of W-min(P),E-max(P) & P2 is_an_arc_of E-max(P),W-min(P)
& P1 /\ P2={W-min(P),E-max(P)} & P1 \/ P2=P
& First_Point(P1,W-min(P),E-max(P),
Vertical_Line((W-bound(P)+E-bound(P))/2))`2>
Last_Point(P2,E-max(P),W-min(P),
Vertical_Line((W-bound(P)+E-bound(P))/2))`2 by A1,Th33;
hence thesis;
end;
uniqueness by A1,Lm2;
end;
definition
let P be Subset of TOP-REAL 2;
assume
A1: P is being_simple_closed_curve;
then
A2: Upper_Arc(P) is_an_arc_of W-min(P),E-max(P) by Def8;
func Lower_Arc(P) -> non empty Subset of TOP-REAL 2 means
:Def9:
it is_an_arc_of E-max(P),W-min(P) & Upper_Arc(P) /\ it={W-min(P),E-max(P)}
& Upper_Arc(P) \/ it=P & First_Point(Upper_Arc(P),W-min(P),E-max(P),
Vertical_Line((W-bound(P)+E-bound(P))/2))`2>
Last_Point(it,E-max(P),W-min(P),
Vertical_Line((W-bound(P)+E-bound(P))/2))`2;
existence by A1,Def8;
uniqueness
proof
let P1,P19 be non empty Subset of TOP-REAL 2;
assume that
A3: P1 is_an_arc_of E-max(P),W-min(P)
and Upper_Arc(P) /\ P1={W-min(P),E-max(P)} and
A4: Upper_Arc(P) \/ P1=P
and First_Point(Upper_Arc(P),W-min(P),E-max(P), Vertical_Line((W-bound(P
)+E-bound(P))/2))`2> Last_Point(P1,E-max(P),W-min(P), Vertical_Line((W-bound(P)
+E-bound(P))/2))`2 and
A5: P19 is_an_arc_of E-max(P),W-min(P)
and Upper_Arc(P) /\ P19={W-min(P),E-max(P)} and
A6: Upper_Arc(P) \/ P19=P
and First_Point(Upper_Arc(P),W-min(P),E-max(P), Vertical_Line((W-bound(P
)+E-bound(P))/2))`2> Last_Point(P19,E-max(P),W-min(P), Vertical_Line((W-bound(P
)+E-bound(P))/2))`2;
A7: P1 is_an_arc_of W-min(P),E-max(P) by A3,JORDAN5B:14;
P19 is_an_arc_of W-min(P),E-max(P) by A5,JORDAN5B:14;
then P1=P19 or Upper_Arc(P)=P19 & P1=Upper_Arc(P) by A1,A2,A4,A6,A7,Th48;
hence thesis;
end;
end;
theorem Th50:
for P being Subset of TOP-REAL 2 st P is being_simple_closed_curve holds
Upper_Arc(P) is_an_arc_of W-min(P),E-max(P) &
Upper_Arc(P) is_an_arc_of E-max(P),W-min(P) &
Lower_Arc(P) is_an_arc_of E-max(P),W-min(P) &
Lower_Arc(P) is_an_arc_of W-min(P),E-max(P) &
Upper_Arc(P) /\ Lower_Arc(P)={W-min(P),E-max(P)}
& Upper_Arc(P) \/ Lower_Arc(P)=P
& First_Point(Upper_Arc(P),W-min(P),E-max(P),
Vertical_Line((W-bound(P)+E-bound(P))/2))`2>
Last_Point(Lower_Arc(P),E-max(P),W-min(P),
Vertical_Line((W-bound(P)+E-bound(P))/2))`2
proof
let P be Subset of TOP-REAL 2;
assume
A1: P is being_simple_closed_curve;
then
A2: Upper_Arc(P) is_an_arc_of W-min(P),E-max(P) by Def8;
Lower_Arc(P) is_an_arc_of E-max(P),W-min(P) by A1,Def9;
hence thesis by A1,A2,Def9,JORDAN5B:14;
end;
theorem Th51:
for P being Subset of TOP-REAL 2 st P is being_simple_closed_curve
holds Lower_Arc(P)=(P\Upper_Arc(P)) \/ {W-min(P),E-max(P)} &
Upper_Arc(P)=(P\Lower_Arc(P)) \/ {W-min(P),E-max(P)}
proof
let P be Subset of TOP-REAL 2;
assume
A1: P is being_simple_closed_curve;
then
A2: Upper_Arc(P) /\ Lower_Arc(P)={W-min(P),E-max(P)} by Def9;
set B=Upper_Arc(P),A=Lower_Arc(P);
A3: (B \/ A \B)\/ (B /\ A) =(A \ B) \/ (A/\B) by XBOOLE_1:40
.=A by XBOOLE_1:51;
(B \/ A \A)\/ (B /\ A) =(B \ A) \/ (B/\A) by XBOOLE_1:40
.=B by XBOOLE_1:51;
hence thesis by A1,A2,A3,Def9;
end;
theorem
for P being Subset of TOP-REAL 2, P1 being Subset of (TOP-REAL 2)|P
st P is being_simple_closed_curve
& Upper_Arc(P) /\ P1={W-min(P),E-max(P)} & Upper_Arc(P) \/ P1=P
holds P1=Lower_Arc(P)
proof
let P be Subset of TOP-REAL 2, P1 be Subset of (TOP-REAL 2)|P;
assume that
A1: P is being_simple_closed_curve and
A2: Upper_Arc(P) /\ P1={W-min(P),E-max(P)} and
A3: Upper_Arc(P) \/ P1=P;
set B=Upper_Arc(P);
(B \/ P1 \B)\/ (B /\ P1) =(P1 \ B) \/ (P1/\B) by XBOOLE_1:40
.=P1 by XBOOLE_1:51;
hence thesis by A1,A2,A3,Th51;
end;
theorem
for P being Subset of TOP-REAL 2, P1 being Subset of (TOP-REAL 2)|P
st P is being_simple_closed_curve
& P1 /\ Lower_Arc(P)={W-min(P),E-max(P)} & P1 \/ Lower_Arc(P)=P
holds P1=Upper_Arc(P)
proof
let P be Subset of TOP-REAL 2, P1 be Subset of (TOP-REAL 2)|P;
assume that
A1: P is being_simple_closed_curve and
A2: P1 /\ Lower_Arc(P)={W-min(P),E-max(P)} and
A3: P1 \/ Lower_Arc(P)=P;
set B=Lower_Arc(P);
(P1 \/ B\B) \/ (P1 /\ B) =P1 /\B \/ (P1\B) by XBOOLE_1:40
.=P1 by XBOOLE_1:51;
hence thesis by A1,A2,A3,Th51;
end;
begin ::An Order of Points in a Simple Closed Curve
theorem Th54:
for P being Subset of TOP-REAL 2,
p1, p2, q being Point of TOP-REAL 2 st P is_an_arc_of p1,p2 &
LE q,p1,P,p1,p2 holds q=p1
proof
let P be Subset of TOP-REAL 2, p1, p2, q be Point of TOP-REAL 2;
assume that
A1: P is_an_arc_of p1,p2 and
A2: LE q,p1,P,p1,p2;
q in P by A2;
then LE p1,q,P,p1,p2 by A1,JORDAN5C:10;
hence thesis by A1,A2,JORDAN5C:12;
end;
theorem Th55:
for P being Subset of TOP-REAL 2,
p1, p2, q being Point of TOP-REAL 2 st P is_an_arc_of p1,p2 &
LE p2,q,P,p1,p2 holds q=p2
proof
let P be Subset of TOP-REAL 2, p1, p2, q be Point of TOP-REAL 2;
assume that
A1: P is_an_arc_of p1,p2 and
A2: LE p2,q,P,p1,p2;
q in P by A2;
then LE q,p2,P,p1,p2 by A1,JORDAN5C:10;
hence thesis by A1,A2,JORDAN5C:12;
end;
definition
let P be Subset of TOP-REAL 2, q1,q2 be Point of TOP-REAL 2;
pred LE q1,q2,P means
q1 in Upper_Arc(P) & q2 in Lower_Arc(P)& not q2=W-min(P) or
q1 in Upper_Arc(P) & q2 in Upper_Arc(P) &
LE q1,q2,Upper_Arc(P),W-min(P),E-max(P) or
q1 in Lower_Arc(P) & q2 in Lower_Arc(P)& not q2=W-min(P) &
LE q1,q2,Lower_Arc(P),E-max(P),W-min(P);
end;
theorem
for P being Subset of TOP-REAL 2, q being Point of TOP-REAL 2
st P is being_simple_closed_curve & q in P holds LE q,q,P
proof
let P be Subset of TOP-REAL 2, q be Point of TOP-REAL 2;
assume that
A1: P is being_simple_closed_curve and
A2: q in P;
A3: Upper_Arc(P) \/ Lower_Arc(P)=P by A1,Def9;
A4: Upper_Arc(P) is_an_arc_of W-min(P),E-max(P) by A1,Th50;
now per cases by A2,A3,XBOOLE_0:def 3;
case
q in Upper_Arc(P);
then LE q,q,Upper_Arc(P),W-min(P),E-max(P) by JORDAN5C:9;
hence thesis;
end;
case
A5: q in Lower_Arc(P) & not q in Upper_Arc(P);
then
A6: LE q,q,Lower_Arc(P),E-max(P),W-min(P) by JORDAN5C:9;
q <> W-min P by A4,A5,TOPREAL1:1;
hence thesis by A6;
end;
end;
hence thesis;
end;
theorem
for P being Subset of TOP-REAL 2, q1,q2 being Point of TOP-REAL 2
st P is being_simple_closed_curve & LE q1,q2,P & LE q2,q1,P holds q1=q2
proof
let P be Subset of TOP-REAL 2, q1,q2 be Point of TOP-REAL 2;
assume that
A1: P is being_simple_closed_curve and
A2: LE q1,q2,P and
A3: LE q2,q1,P;
A4: Lower_Arc(P) is_an_arc_of E-max(P),W-min(P) by A1,Def9;
A5: Upper_Arc(P) /\ Lower_Arc(P)={W-min(P),E-max(P)} by A1,Def9;
A6: Upper_Arc(P) is_an_arc_of W-min(P),E-max(P) by A1,Th50;
now per cases by A2;
case
A7: q1 in Upper_Arc(P) & q2 in Lower_Arc(P)& not q2=W-min(P);
now per cases by A3;
case
A8: q2 in Upper_Arc(P) & q1 in Lower_Arc(P)& not q1=W-min(P);
then q1 in Upper_Arc(P) /\ Lower_Arc(P) by A7,XBOOLE_0:def 4;
then
A9: q1=E-max(P) by A5,A8,TARSKI:def 2;
q2 in Upper_Arc(P) /\ Lower_Arc(P) by A7,A8,XBOOLE_0:def 4;
hence thesis by A5,A7,A9,TARSKI:def 2;
end;
case
A10: q2 in Upper_Arc(P) & q1 in Upper_Arc(P) &
LE q2,q1,Upper_Arc(P),W-min(P),E-max(P);
then q2 in Upper_Arc(P) /\ Lower_Arc(P) by A7,XBOOLE_0:def 4;
then q2=E-max(P) by A5,A7,TARSKI:def 2;
hence thesis by A6,A10,Th55;
end;
case
A11: q2 in Lower_Arc(P) & q1 in Lower_Arc(P)& not q1=W-min(P) &
LE q2,q1,Lower_Arc(P),E-max(P),W-min(P);
then q1 in Upper_Arc(P) /\ Lower_Arc(P) by A7,XBOOLE_0:def 4;
then q1=E-max(P) by A5,A11,TARSKI:def 2;
hence thesis by A4,A11,Th54;
end;
end;
hence thesis;
end;
case
A12: q1 in Upper_Arc(P) & q2 in Upper_Arc(P)
& LE q1,q2,Upper_Arc(P),W-min(P),E-max(P);
now per cases by A3;
case
A13: q2 in Upper_Arc(P) & q1 in Lower_Arc(P)& not q1=W-min(P);
then q1 in Upper_Arc(P) /\ Lower_Arc(P) by A12,XBOOLE_0:def 4;
then q1=E-max(P) by A5,A13,TARSKI:def 2;
hence thesis by A6,A12,Th55;
end;
case q2 in Upper_Arc(P) & q1 in Upper_Arc(P) &
LE q2,q1,Upper_Arc(P),W-min(P),E-max(P);
hence thesis by A6,A12,JORDAN5C:12;
end;
case
A14: q2 in Lower_Arc(P) & q1 in Lower_Arc(P)& not q1=W-min(P) &
LE q2,q1,Lower_Arc(P),E-max(P),W-min(P);
then q1 in Upper_Arc(P) /\ Lower_Arc(P) by A12,XBOOLE_0:def 4;
then q1=E-max(P) by A5,A14,TARSKI:def 2;
hence thesis by A4,A14,Th54;
end;
end;
hence thesis;
end;
case
A15: q1 in Lower_Arc(P) & q2 in Lower_Arc(P)& not q2=W-min(P) &
LE q1,q2,Lower_Arc(P),E-max(P),W-min(P);
now per cases by A3;
case q2 in Upper_Arc(P) & q1 in Lower_Arc(P)& not q1=W-min(P);
then q2 in Upper_Arc(P) /\ Lower_Arc(P) by A15,XBOOLE_0:def 4;
then q2=E-max(P) by A5,A15,TARSKI:def 2;
hence thesis by A4,A15,Th54;
end;
case
A16: q2 in Upper_Arc(P) & q1 in Upper_Arc(P) &
LE q2,q1,Upper_Arc(P),W-min(P),E-max(P);
then q2 in Upper_Arc(P) /\ Lower_Arc(P) by A15,XBOOLE_0:def 4;
then q2=E-max(P) by A5,A15,TARSKI:def 2;
hence thesis by A6,A16,Th55;
end;
case q2 in Lower_Arc(P) & q1 in Lower_Arc(P)& not q1=W-min(P) &
LE q2,q1,Lower_Arc(P),E-max(P),W-min(P);
hence thesis by A4,A15,JORDAN5C:12;
end;
end;
hence thesis;
end;
end;
hence thesis;
end;
theorem
for P being Subset of TOP-REAL 2, q1,q2,q3 being Point of TOP-REAL 2
st P is being_simple_closed_curve & LE q1,q2,P & LE q2,q3,P holds LE q1,q3,P
proof
let P be Subset of TOP-REAL 2, q1,q2,q3 be Point of TOP-REAL 2;
assume that
A1: P is being_simple_closed_curve and
A2: LE q1,q2,P and
A3: LE q2,q3,P;
A4: Lower_Arc(P) is_an_arc_of E-max(P),W-min(P) by A1,Def9;
A5: Upper_Arc(P) /\ Lower_Arc(P)={W-min(P),E-max(P)} by A1,Def9;
A6: Upper_Arc(P) is_an_arc_of W-min(P),E-max(P) by A1,Th50;
now per cases by A2;
case
A7: q1 in Upper_Arc(P) & q2 in Lower_Arc(P)& not q2=W-min(P);
now per cases by A3;
case q2 in Upper_Arc(P) & q3 in Lower_Arc(P)& not q3=W-min(P);
hence thesis by A7;
end;
case
A8: q2 in Upper_Arc(P) & q3 in Upper_Arc(P) &
LE q2,q3,Upper_Arc(P),W-min(P),E-max(P);
then q2 in Upper_Arc(P) /\ Lower_Arc(P) by A7,XBOOLE_0:def 4;
then q2=E-max(P) by A5,A7,TARSKI:def 2;
hence thesis by A2,A6,A8,Th55;
end;
case q2 in Lower_Arc(P) & q3 in Lower_Arc(P)& not q3=W-min(P) &
LE q2,q3,Lower_Arc(P),E-max(P),W-min(P);
hence thesis by A7;
end;
end;
hence thesis;
end;
case
A9: q1 in Upper_Arc(P) & q2 in Upper_Arc(P)
& LE q1,q2,Upper_Arc(P),W-min(P),E-max(P);
now per cases by A3;
case q2 in Upper_Arc(P) & q3 in Lower_Arc(P)& not q3=W-min(P);
hence thesis by A9;
end;
case
q2 in Upper_Arc(P) & q3 in Upper_Arc(P) &
LE q2,q3,Upper_Arc(P),W-min(P),E-max(P);
then LE q1,q3,Upper_Arc(P),W-min(P),E-max(P) by A9,JORDAN5C:13;
hence thesis;
end;
case q2 in Lower_Arc(P) & q3 in Lower_Arc(P)& not q3=W-min(P) &
LE q2,q3,Lower_Arc(P),E-max(P),W-min(P);
hence thesis by A9;
end;
end;
hence thesis;
end;
case
A10: q1 in Lower_Arc(P) & q2 in Lower_Arc(P)& not q2=W-min(P) &
LE q1,q2,Lower_Arc(P),E-max(P),W-min(P);
now per cases by A3;
case
A11: q2 in Upper_Arc(P) & q3 in Lower_Arc(P)& not q3=W-min(P);
then q2 in Upper_Arc(P) /\ Lower_Arc(P) by A10,XBOOLE_0:def 4;
then q2=E-max(P) by A5,A10,TARSKI:def 2;
then LE q2,q3,Lower_Arc(P),E-max(P),W-min(P) by A4,A11,JORDAN5C:10;
then LE q1,q3,Lower_Arc(P),E-max(P),W-min(P) by A10,JORDAN5C:13;
hence thesis by A11;
end;
case
A12: q2 in Upper_Arc(P) & q3 in Upper_Arc(P) &
LE q2,q3,Upper_Arc(P),W-min(P),E-max(P);
then q2 in Upper_Arc(P) /\ Lower_Arc(P) by A10,XBOOLE_0:def 4;
then q2=E-max(P) by A5,A10,TARSKI:def 2;
hence thesis by A2,A6,A12,Th55;
end;
case
A13: q2 in Lower_Arc(P) & q3 in Lower_Arc(P)& not q3=W-min(P) &
LE q2,q3,Lower_Arc(P),E-max(P),W-min(P);
then LE q1,q3,Lower_Arc(P),E-max(P),W-min(P) by A10,JORDAN5C:13;
hence thesis by A13;
end;
end;
hence thesis;
end;
end;
hence thesis;
end;
theorem
for P being Subset of TOP-REAL 2, p1,p2,q being Point of TOP-REAL 2
st P is_an_arc_of p1,p2 & q <> p2 holds not p2 in L_Segment(P,p1,p2,q)
proof
let P be Subset of TOP-REAL 2, p1,p2,q be Point of TOP-REAL 2 such that
A1: P is_an_arc_of p1,p2 and
A2: q <> p2;
assume p2 in L_Segment(P,p1,p2,q);
then ex w being Point of TOP-REAL 2 st p2 = w & LE w,q,P,p1,p2;
hence contradiction by A1,A2,Th55;
end;
theorem
for P being Subset of TOP-REAL 2, p1,p2,q being Point of TOP-REAL 2
st P is_an_arc_of p1,p2 & q <> p1 holds not p1 in R_Segment(P,p1,p2,q)
proof
let P be Subset of TOP-REAL 2, p1,p2,q be Point of TOP-REAL 2 such that
A1: P is_an_arc_of p1,p2 and
A2: q <> p1;
assume p1 in R_Segment(P,p1,p2,q);
then ex w being Point of TOP-REAL 2 st p1 = w & LE q,w,P,p1,p2;
hence contradiction by A1,A2,Th54;
end;
registration
let S be non empty being_simple_closed_curve Subset of TOP-REAL 2;
cluster Lower_Arc S -> non empty compact;
coherence
proof
Lower_Arc S is_an_arc_of E-max S, W-min S by Def9;
hence thesis by JORDAN5A:1;
end;
cluster Upper_Arc S -> non empty compact;
coherence
proof
Upper_Arc S is_an_arc_of W-min S, E-max S by Def8;
hence thesis by JORDAN5A:1;
end;
end;
theorem Th61:
for S being being_simple_closed_curve non empty Subset of TOP-REAL 2
holds Lower_Arc S c= S & Upper_Arc S c= S
proof
let S be being_simple_closed_curve non empty Subset of TOP-REAL 2;
S = Lower_Arc S \/ Upper_Arc S by Th50;
hence thesis by XBOOLE_1:7;
end;
reserve C for Simple_closed_curve;
definition
let C be Simple_closed_curve;
func Lower_Middle_Point C -> Point of TOP-REAL 2 equals
First_Point(Lower_Arc C,W-min C,E-max C,
Vertical_Line((W-bound C+E-bound C)/2));
coherence;
func Upper_Middle_Point C -> Point of TOP-REAL 2 equals
First_Point(Upper_Arc C,W-min C,E-max C,
Vertical_Line((W-bound C+E-bound C)/2));
coherence;
end;
theorem Th62:
Lower_Arc C meets Vertical_Line((W-bound C+E-bound C)/2)
proof
A1: W-bound C <= E-bound C by SPRECT_1:21;
(W-min C)`1 = W-bound C by EUCLID:52;
then
A2: (W-min C)`1<=(W-bound C +E-bound C)/2 by A1,Th1;
(E-max C)`1 = E-bound C by EUCLID:52;
then
A3: (W-bound C +E-bound C)/2<=(E-max C)`1 by A1,Th1;
Lower_Arc C is_an_arc_of W-min C,E-max C by Th50;
hence thesis by A2,A3,Th49;
end;
theorem Th63:
Upper_Arc C meets Vertical_Line((W-bound C+E-bound C)/2)
proof
A1: W-bound C <= E-bound C by SPRECT_1:21;
(W-min C)`1 = W-bound C by EUCLID:52;
then
A2: (W-min C)`1<=(W-bound C +E-bound C)/2 by A1,Th1;
(E-max C)`1 = E-bound C by EUCLID:52;
then
A3: (W-bound C +E-bound C)/2<=(E-max C)`1 by A1,Th1;
Upper_Arc C is_an_arc_of W-min C,E-max C by Th50;
hence thesis by A2,A3,Th49;
end;
theorem
(Lower_Middle_Point C)`1 = (W-bound C+E-bound C)/2
proof
set L = Vertical_Line((W-bound C+E-bound C)/2),
p = First_Point(Lower_Arc C,W-min C,E-max C,L);
A1: Lower_Arc C meets L by Th62;
L is closed by Th6;
then
A2: Lower_Arc C /\ L is closed by TOPS_1:8;
Lower_Arc C is_an_arc_of W-min C, E-max C by Th50;
then p in Lower_Arc C /\ L by A1,A2,JORDAN5C:def 1;
then p in L by XBOOLE_0:def 4;
hence thesis by Th31;
end;
theorem
(Upper_Middle_Point C)`1 = (W-bound C+E-bound C)/2
proof
set L = Vertical_Line((W-bound C+E-bound C)/2),
p = First_Point(Upper_Arc C,W-min C,E-max C,L);
A1: Upper_Arc C meets L by Th63;
L is closed by Th6;
then
A2: Upper_Arc C /\ L is closed by TOPS_1:8;
Upper_Arc C is_an_arc_of W-min C, E-max C by Th50;
then p in Upper_Arc C /\ L by A1,A2,JORDAN5C:def 1;
then p in L by XBOOLE_0:def 4;
hence thesis by Th31;
end;
theorem
Lower_Middle_Point C in Lower_Arc C
proof
set L = Vertical_Line((W-bound C+E-bound C)/2),
p = First_Point(Lower_Arc C,W-min C,E-max C,L);
A1: Lower_Arc C meets L by Th62;
L is closed by Th6;
then
A2: Lower_Arc C /\ L is closed by TOPS_1:8;
Lower_Arc C is_an_arc_of W-min C, E-max C by Th50;
then p in L /\ Lower_Arc C by A1,A2,JORDAN5C:def 1;
hence thesis by XBOOLE_0:def 4;
end;
theorem Th67:
Upper_Middle_Point C in Upper_Arc C
proof
set L = Vertical_Line((W-bound C+E-bound C)/2),
p = First_Point(Upper_Arc C,W-min C,E-max C,L);
A1: Upper_Arc C meets L by Th63;
L is closed by Th6;
then
A2: Upper_Arc C /\ L is closed by TOPS_1:8;
A3: Upper_Arc C is_an_arc_of E-max C, W-min C by Th50;
then p = Last_Point(Upper_Arc C,E-max C,W-min C,L) by A1,A2,JORDAN5C:18;
then p in L /\ Upper_Arc C by A1,A2,A3,JORDAN5C:def 2;
hence thesis by XBOOLE_0:def 4;
end;
theorem
Upper_Middle_Point C in C
proof
A1: Upper_Middle_Point C in Upper_Arc C by Th67;
Upper_Arc C c= C by Th61;
hence thesis by A1;
end;
theorem :: JORDAN1B:26: AK, 20.02.2006
for C be Simple_closed_curve
for r be Real st W-bound C <= r & r <= E-bound C holds
LSeg(|[r,S-bound C]|,|[r,N-bound C]|) meets Upper_Arc C
proof
let C be Simple_closed_curve;
let r be Real;
A1: (W-min C)`1 = W-bound C by EUCLID:52;
A2: (E-max C)`1 = E-bound C by EUCLID:52;
assume that
A3: W-bound C <= r and
A4: r <= E-bound C;
Upper_Arc C is_an_arc_of W-min(C),E-max(C) by Def8;
then Upper_Arc C meets Vertical_Line(r) by A1,A2,A3,A4,Th49;
then consider x be object such that
A5: x in Upper_Arc C /\ Vertical_Line(r) by XBOOLE_0:4;
A6: x in Upper_Arc C by A5,XBOOLE_0:def 4;
A7: x in Vertical_Line(r) by A5,XBOOLE_0:def 4;
reconsider fs = x as Point of TOP-REAL 2 by A5;
A8: Upper_Arc C c= C by Th61;
then
A9: S-bound C <= fs`2 by A6,PSCOMP_1:24;
A10: fs`2 <= N-bound C by A6,A8,PSCOMP_1:24;
A11: |[r,S-bound C]|`1 = r by EUCLID:52
.= fs`1 by A7,Th31;
A12: |[r,N-bound C]|`1 = r by EUCLID:52
.= fs`1 by A7,Th31;
A13: |[r,S-bound C]|`2 = S-bound C by EUCLID:52;
|[r,N-bound C]|`2 = N-bound C by EUCLID:52;
then x in LSeg(|[r,S-bound C]|,|[r,N-bound C]|) by A9,A10,A11,A12,A13,
GOBOARD7:7;
hence thesis by A6,XBOOLE_0:3;
end;
theorem :: JORDAN1B:27: AK, 20.02.2006
for C be Simple_closed_curve
for r be Real st W-bound C <= r & r <= E-bound C holds
LSeg(|[r,S-bound C]|,|[r,N-bound C]|) meets Lower_Arc C
proof
let C be Simple_closed_curve;
let r be Real;
A1: (W-min C)`1 = W-bound C by EUCLID:52;
A2: (E-max C)`1 = E-bound C by EUCLID:52;
assume that
A3: W-bound C <= r and
A4: r <= E-bound C;
Lower_Arc C is_an_arc_of E-max(C),W-min(C) by Def9;
then Lower_Arc C is_an_arc_of W-min(C),E-max(C) by JORDAN5B:14;
then Lower_Arc C meets Vertical_Line(r) by A1,A2,A3,A4,Th49;
then consider x be object such that
A5: x in Lower_Arc C /\ Vertical_Line(r) by XBOOLE_0:4;
A6: x in Lower_Arc C by A5,XBOOLE_0:def 4;
A7: x in Vertical_Line(r) by A5,XBOOLE_0:def 4;
reconsider fs = x as Point of TOP-REAL 2 by A5;
A8: Lower_Arc C c= C by Th61;
then
A9: S-bound C <= fs`2 by A6,PSCOMP_1:24;
A10: fs`2 <= N-bound C by A6,A8,PSCOMP_1:24;
A11: |[r,S-bound C]|`1 = r by EUCLID:52
.= fs`1 by A7,Th31;
A12: |[r,N-bound C]|`1 = r by EUCLID:52
.= fs`1 by A7,Th31;
A13: |[r,S-bound C]|`2 = S-bound C by EUCLID:52;
|[r,N-bound C]|`2 = N-bound C by EUCLID:52;
then x in LSeg(|[r,S-bound C]|,|[r,N-bound C]|) by A9,A10,A11,A12,A13,
GOBOARD7:7;
hence thesis by A6,XBOOLE_0:3;
end;