:: On the Decomposition of a Simple Closed Curve into Two Arcs
:: by Andrzej Trybulec and Yatsuka Nakamura
::
:: Received September 16, 2002
:: Copyright (c) 2002-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, TOPREAL2, SUBSET_1, EUCLID, PRE_TOPC, TARSKI, XBOOLE_0,
JORDAN6, PSCOMP_1, TOPREAL1, JORDAN3, FUNCT_1, ORDINAL2, CONNSP_2,
RCOMP_1, RELAT_1, TOPS_2, FUNCT_2, STRUCT_0, BORSUK_1, CARD_1, REAL_1,
ARYTM_3, XXREAL_0, XXREAL_1, PCOMPS_1, JGRAPH_2, ARYTM_1, TOPMETR;
notations TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, XXREAL_0, XCMPLX_0,
XREAL_0, REAL_1, RELAT_1, FUNCT_1, RELSET_1, PARTFUN1, FUNCT_2, FCONT_1,
STRUCT_0, PRE_TOPC, TOPS_2, COMPTS_1, CONNSP_2, PCOMPS_1, RCOMP_1,
TMAP_1, EUCLID, PSCOMP_1, TOPMETR, JORDAN6, TOPREAL1, JORDAN5C, TOPREAL2,
JORDAN7;
constructors REAL_1, RCOMP_1, FCONT_1, TOPS_2, TMAP_1, TOPMETR, PCOMPS_1,
TOPREAL1, PSCOMP_1, JORDAN5C, JORDAN6, JORDAN7, COMPLEX1, NUMBERS;
registrations XBOOLE_0, FUNCT_1, RELSET_1, FUNCT_2, NUMBERS, XXREAL_0,
XREAL_0, MEMBERED, STRUCT_0, PRE_TOPC, BORSUK_1, EUCLID, TOPMETR,
TOPREAL2, TMAP_1, ORDINAL1;
requirements NUMERALS, REAL, BOOLE, SUBSET, ARITHM;
definitions TARSKI, TOPS_2, TOPREAL1, BORSUK_1;
equalities STRUCT_0;
expansions TARSKI, TOPS_2, TOPREAL1, BORSUK_1;
theorems PRE_TOPC, TOPMETR, XBOOLE_0, FUNCT_1, XBOOLE_1, FUNCT_2, TOPREAL5,
TREAL_1, BORSUK_1, JORDAN6, TOPREAL1, TOPS_2, TARSKI, RELAT_1, TOPREAL3,
JORDAN5B, TOPMETR3, TOPREAL2, ZFMISC_1, JORDAN5A, JORDAN5C, FCONT_1,
FUNCT_3, CONNSP_2, TMAP_1, RFUNCT_2, RELSET_1, FUNCT_4, JORDAN7,
SPRECT_1, XCMPLX_1, XREAL_1, XXREAL_0, XXREAL_1, EUCLID, XREAL_0;
begin
reserve C for Simple_closed_curve,
A,A1,A2 for Subset of TOP-REAL 2,
p,p1,p2,q ,q1,q2 for Point of TOP-REAL 2,
n for Element of NAT;
theorem
Lower_Arc C <> Upper_Arc C
proof
assume Lower_Arc C = Upper_Arc C;
then
A1: Lower_Arc C =(C\Lower_Arc C) \/ {W-min C, E-max C} by JORDAN6:51;
Lower_Arc C is_an_arc_of W-min C, E-max C by JORDAN6:50;
then
A2: ex p3 being Point of TOP-REAL 2 st p3 in Lower_Arc C & p3<>W-min C & p3
<>E-max C by JORDAN6:42;
Lower_Arc C misses C\Lower_Arc C by XBOOLE_1:79;
then Lower_Arc C c= {W-min C, E-max C} by A1,XBOOLE_1:73;
hence contradiction by A2,TARSKI:def 2;
end;
theorem Th2:
Segment(A,p1,p2,q1,q2) c= A
proof
Segment(A,p1,p2,q1,q2) = R_Segment(A,p1,p2,q1) /\ L_Segment(A,p1,p2,q2)
by JORDAN6:def 5;
then
R_Segment(A,p1,p2,q1) c= A & Segment(A,p1,p2,q1,q2) c= R_Segment(A,p1,p2
,q1) by JORDAN6:20,XBOOLE_1:17;
hence thesis;
end;
theorem Th3:
q in A implies q in L_Segment(A,p1,p2,q)
proof
assume q in A;
then
A1: LE q,q,A,p1,p2 by JORDAN5C:9;
L_Segment(A,p1,p2,q) = {q1 : LE q1,q,A,p1,p2} by JORDAN6:def 3;
hence thesis by A1;
end;
theorem Th4:
q in A implies q in R_Segment(A,p1,p2,q)
proof
assume q in A;
then
A1: LE q,q,A,p1,p2 by JORDAN5C:9;
R_Segment(A,p1,p2,q) = {q1 : LE q,q1,A,p1,p2} by JORDAN6:def 4;
hence thesis by A1;
end;
theorem Th5:
LE q1, q2, A, p1, p2 implies q1 in Segment(A,p1,p2,q1,q2) & q2 in
Segment(A,p1,p2,q1,q2)
proof
A1: Segment(A,p1,p2,q1,q2) = R_Segment(A,p1,p2,q1) /\ L_Segment(A,p1,p2,q2)
by JORDAN6:def 5;
assume
A2: LE q1, q2, A, p1, p2;
L_Segment(A,p1,p2,q2) = {q : LE q,q2,A,p1,p2} by JORDAN6:def 3;
then
A3: q1 in L_Segment(A,p1,p2,q2) by A2;
q1 in A by A2,JORDAN5C:def 3;
then q1 in R_Segment(A,p1,p2,q1) by Th4;
hence q1 in Segment(A,p1,p2,q1,q2) by A1,A3,XBOOLE_0:def 4;
R_Segment(A,p1,p2,q1) = {q : LE q1,q,A,p1,p2} by JORDAN6:def 4;
then
A4: q2 in R_Segment(A,p1,p2,q1) by A2;
q2 in A by A2,JORDAN5C:def 3;
then q2 in L_Segment(A,p1,p2,q2) by Th3;
hence thesis by A1,A4,XBOOLE_0:def 4;
end;
theorem
Segment(p,q,C) c= C
proof
set S =Segment(p,q,C);
let e be object such that
A1: e in S;
Upper_Arc C \/ Lower_Arc C = C by JORDAN6:50;
then
A2: Upper_Arc C c= C & Lower_Arc C c= C by XBOOLE_1:7;
per cases;
suppose
q = W-min C;
then S = {p1: LE p,p1,C or p in C & p1=W-min C} by JORDAN7:def 1;
then consider p1 such that
A3: e = p1 &( LE p,p1,C or p in C & p1=W-min C) by A1;
now
assume LE p,p1,C;
then p1 in Upper_Arc C or p1 in Lower_Arc C by JORDAN6:def 10;
hence p1 in C by A2;
end;
hence thesis by A3,SPRECT_1:13;
end;
suppose
q <> W-min C;
then S = {p1: LE p,p1,C & LE p1,q,C} by JORDAN7:def 1;
then consider p1 such that
A4: e = p1 and
A5: LE p,p1,C and
LE p1,q,C by A1;
p1 in Upper_Arc C or p1 in Lower_Arc C by A5,JORDAN6:def 10;
hence thesis by A2,A4;
end;
end;
theorem
p in C & q in C implies LE p,q,C or LE q,p,C
proof
assume that
A1: p in C and
A2: q in C;
A3: C = Lower_Arc C \/ Upper_Arc C by JORDAN6:50;
per cases by A1,A2,A3,JORDAN7:1,XBOOLE_0:def 3;
suppose
p = q;
hence thesis by A1,JORDAN6:56;
end;
suppose that
A4: p in Lower_Arc C & p <> W-min C & q in Lower_Arc C & q <> W-min C and
A5: p <> q;
Lower_Arc C is_an_arc_of E-max C,W-min C by JORDAN6:50;
then LE p,q,Lower_Arc C, E-max C,W-min C or LE q,p,Lower_Arc C, E-max C,
W-min C by A4,A5,JORDAN5C:14;
hence thesis by A4,JORDAN6:def 10;
end;
suppose
p in Lower_Arc C & p <> W-min C & q in Upper_Arc C;
hence thesis by JORDAN6:def 10;
end;
suppose
p in Upper_Arc C & q in Lower_Arc C & q <> W-min C;
hence thesis by JORDAN6:def 10;
end;
suppose that
A6: p in Upper_Arc C & q in Upper_Arc C and
A7: p <> q;
Upper_Arc C is_an_arc_of W-min C, E-max C by JORDAN6:50;
then LE p,q,Upper_Arc C,W-min C, E-max C or LE q,p,Upper_Arc C,W-min C,
E-max C by A6,A7,JORDAN5C:14;
hence thesis by A6,JORDAN6:def 10;
end;
end;
theorem Th8:
for X,Y being non empty TopSpace, Y0 being non empty SubSpace of
Y, f being Function of X,Y, g being Function of X,Y0 st f = g & f is continuous
holds g is continuous
proof
let X,Y be non empty TopSpace, Y0 being non empty SubSpace of Y;
let f be Function of X,Y, g be Function of X,Y0 such that
A1: f = g and
A2: f is continuous;
let W being Point of X, G being a_neighborhood of g.W;
consider V being Subset of Y0 such that
A3: V is open and
A4: V c= G and
A5: g.W in V by CONNSP_2:6;
g.W in [#]Y0 & [#]Y0 c= [#]Y by PRE_TOPC:def 4;
then reconsider p = g.W as Point of Y;
consider C being Subset of Y such that
A6: C is open and
A7: C /\ [#]Y0 = V by A3,TOPS_2:24;
p in C by A5,A7,XBOOLE_0:def 4;
then C is a_neighborhood of p by A6,CONNSP_2:3;
then consider H being a_neighborhood of W such that
A8: f.:H c= C by A1,A2;
take H;
g.:H c= V by A1,A7,A8,XBOOLE_1:19;
hence thesis by A4;
end;
theorem Th9:
for S,T being non empty TopSpace, S0 being non empty SubSpace of
S, T0 being non empty SubSpace of T, f being Function of S,T st f is
being_homeomorphism for g being Function of S0,T0 st g = f|S0 & g is onto holds
g is being_homeomorphism
proof
let S,T be non empty TopSpace, S0 be non empty SubSpace of S, T0 be non
empty SubSpace of T, f be Function of S,T such that
A1: f is being_homeomorphism;
A2: rng f = [#]T by A1;
A3: f" is continuous by A1;
let g be Function of S0,T0 such that
A4: g = f|S0 and
A5: g is onto;
A6: g = f|the carrier of S0 by A4,TMAP_1:def 4;
then
A7: f.:the carrier of S0 = rng g by RELAT_1:115
.= the carrier of T0 by A5,FUNCT_2:def 3;
thus dom g = [#]S0 by FUNCT_2:def 1;
thus
rng g = [#]T0 by A5,FUNCT_2:def 3;
A8: f is one-to-one by A1;
hence
A9: g is one-to-one by A6,FUNCT_1:52;
A10: f is onto by A2,FUNCT_2:def 3;
f is continuous by A1;
then g is continuous Function of S0,T by A4;
hence g is continuous by Th8;
g" = (f qua Function|the carrier of S0)" by A5,A6,A9,TOPS_2:def 4
.= (f qua Function)"|(f.:the carrier of S0) by A8,RFUNCT_2:17
.= f"|(the carrier of T0) by A10,A8,A7,TOPS_2:def 4
.= f"|T0 by TMAP_1:def 4;
then g" is continuous Function of T0,S by A3;
hence thesis by Th8;
end;
theorem Th10:
for P1,P2,P3 being Subset of TOP-REAL 2 for p1,p2 being Point of
TOP-REAL 2 st P1 is_an_arc_of p1,p2 & P2 is_an_arc_of p1,p2 & P3 is_an_arc_of
p1,p2 & P2 /\ P3={p1,p2} & P1 c= P2 \/ P3 holds P1=P2 or P1=P3
proof
let P1,P2,P3 be Subset of TOP-REAL 2;
set P = P2 \/ P3;
A1: the carrier of (TOP-REAL 2)|P=[#]((TOP-REAL 2)|P) .=P by PRE_TOPC:def 5;
then reconsider U2=P2 as Subset of (TOP-REAL 2)|P by XBOOLE_1:7;
reconsider U3=P3 as Subset of (TOP-REAL 2)|P by A1,XBOOLE_1:7;
let p1,p2 be Point of TOP-REAL 2;
assume that
A2: P1 is_an_arc_of p1,p2 and
A3: P2 is_an_arc_of p1,p2 and
A4: P3 is_an_arc_of p1,p2;
consider f being Function of I[01], (TOP-REAL 2)|P1 such that
A5: f is being_homeomorphism and
A6: f.0 = p1 & f.1 = p2 by A2;
A7: f is one-to-one by A5;
U2=P2 /\ P by XBOOLE_1:7,28;
then
A8: U2 is closed by A3,JORDAN6:2,11;
A9: rng f=[#]((TOP-REAL 2)|P1) by A5
.=P1 by PRE_TOPC:def 5;
p1 in P2 by A3,TOPREAL1:1;
then reconsider Q=P as non empty Subset of Euclid 2 by TOPREAL3:8;
assume that
A10: P2 /\ P3={p1,p2} and
A11: P1 c= P2 \/ P3;
A12: p2 in P2 /\ P3 & p1 in P2 /\ P3 by A10,TARSKI:def 2;
U3=P3 /\ P by XBOOLE_1:7,28;
then
A13: U3 is closed by A4,JORDAN6:2,11;
A14: f is continuous by A5;
A15: dom f=[#](I[01]) by A5;
per cases;
suppose
A16: for r being Real st 0<r & r<1 holds f.r in P3;
P1 c= P3
proof
let y be object;
assume y in P1;
then consider x being object such that
A17: x in dom f and
A18: y=f.x by A9,FUNCT_1:def 3;
reconsider r=x as Real by A17;
r<=1 by A17,BORSUK_1:40,XXREAL_1:1;
then r = 0 or r = 1 or 0<r & r <1 by A17,BORSUK_1:40,XXREAL_0:1
,XXREAL_1:1;
hence thesis by A12,A6,A16,A18,XBOOLE_0:def 4;
end;
hence thesis by A2,A4,JORDAN6:46;
end;
suppose
A19: ex r being Real st 0<r & r<1 & not f.r in P3;
now
per cases;
case
A20: for r being Real st 0<r & r<1 holds f.r in P2;
P1 c= P2
proof
let y be object;
assume y in P1;
then consider x being object such that
A21: x in dom f and
A22: y=f.x by A9,FUNCT_1:def 3;
reconsider r=x as Real by A21;
r<=1 by A21,BORSUK_1:40,XXREAL_1:1;
then 0<r & r<1 or r=0 or r=1 by A21,BORSUK_1:40,XXREAL_0:1,XXREAL_1:1
;
hence thesis by A12,A6,A20,A22,XBOOLE_0:def 4;
end;
hence thesis by A2,A3,JORDAN6:46;
end;
case
ex r being Real st 0<r & r<1 & not f.r in P2;
then consider r2 being Real such that
A23: 0<r2 and
A24: r2<1 and
A25: not f.r2 in P2;
r2 in [.0,1.] by A23,A24,XXREAL_1:1;
then f.r2 in rng f by A15,BORSUK_1:40,FUNCT_1:def 3;
then
A26: f.r2 in P3 by A11,A9,A25,XBOOLE_0:def 3;
consider r1 being Real such that
A27: 0<r1 and
A28: r1<1 and
A29: not f.r1 in P3 by A19;
r1 in [.0,1.] by A27,A28,XXREAL_1:1;
then
A30: f.r1 in rng f by A15,BORSUK_1:40,FUNCT_1:def 3;
then
A31: f.r1 in P2 by A11,A9,A29,XBOOLE_0:def 3;
now
per cases;
suppose
A32: r1<=r2;
now
per cases by A32,XXREAL_0:1;
suppose
r1=r2;
hence contradiction by A11,A9,A25,A29,A30,XBOOLE_0:def 3;
end;
suppose
A33: r1<r2;
A34: the carrier of (TOP-REAL 2)|P1=[#]((TOP-REAL 2)|P1)
.=P1 by PRE_TOPC:def 5;
the carrier of (TOP-REAL 2)|P=[#]((TOP-REAL 2)|P)
.=P by PRE_TOPC:def 5;
then rng f c= the carrier of (TOP-REAL 2)|P by A11,A34;
then reconsider
g=f as Function of I[01],(TOP-REAL 2)|P by A15,FUNCT_2:2;
P=P1 \/ P by A11,XBOOLE_1:12;
then
A35: (TOP-REAL 2)|P1 is SubSpace of (TOP-REAL 2)|P by TOPMETR:4;
U2 \/ U3 =the carrier of ((Euclid 2)|Q) & (TOP-REAL 2)|P=
TopSpaceMetr(( Euclid 2)|Q) by EUCLID:63,TOPMETR:def 2;
then consider r0 being Real such that
A36: r1<=r0 and
A37: r0<=r2 and
A38: g.r0 in U2 /\ U3 by A14,A8,A13,A24,A27,A26,A31,A33,A35,
PRE_TOPC:26,TOPMETR3:13;
r0<1 by A24,A37,XXREAL_0:2;
then
A39: r0 in dom f by A15,A27,A36,BORSUK_1:40,XXREAL_1:1;
A40: 0 in dom f & 1 in dom f by A15,BORSUK_1:40,XXREAL_1:1;
g.r0=p1 or g.r0=p2 by A10,A38,TARSKI:def 2;
hence contradiction by A6,A7,A24,A27,A36,A37,A39,A40,
FUNCT_1:def 4;
end;
end;
hence contradiction;
end;
suppose
A41: r1>r2;
A42: the carrier of (TOP-REAL 2)|P1=[#]((TOP-REAL 2)|P1)
.=P1 by PRE_TOPC:def 5;
the carrier of (TOP-REAL 2)|P=[#]((TOP-REAL 2)|P)
.=P by PRE_TOPC:def 5;
then rng f c= the carrier of (TOP-REAL 2)|P by A11,A42;
then reconsider g=f as Function of I[01],(TOP-REAL 2)|P by A15,
FUNCT_2:2;
P=P1 \/ P by A11,XBOOLE_1:12;
then
A43: (TOP-REAL 2)|P1 is SubSpace of (TOP-REAL 2)|P by TOPMETR:4;
U2 \/ U3 =the carrier of ((Euclid 2)|Q) & (TOP-REAL 2)|P=
TopSpaceMetr(( Euclid 2)|Q) by EUCLID:63,TOPMETR:def 2;
then consider r0 being Real such that
A44: r2<=r0 and
A45: r0<=r1 and
A46: g.r0 in U2 /\ U3 by A14,A8,A13,A23,A28,A26,A31,A41,A43,PRE_TOPC:26
,TOPMETR3:13;
r0<1 by A28,A45,XXREAL_0:2;
then
A47: r0 in dom f by A15,A23,A44,BORSUK_1:40,XXREAL_1:1;
A48: 0 in dom f & 1 in dom f by A15,BORSUK_1:40,XXREAL_1:1;
g.r0=p1 or g.r0=p2 by A10,A46,TARSKI:def 2;
hence contradiction by A6,A7,A23,A28,A44,A45,A47,A48,FUNCT_1:def 4;
end;
end;
hence contradiction;
end;
end;
hence thesis;
end;
end;
theorem Th11:
for C being Simple_closed_curve, A1,A2 being Subset of TOP-REAL
2, p1,p2 being Point of TOP-REAL 2 st A1 is_an_arc_of p1,p2 & A2 is_an_arc_of
p1,p2 & A1 c= C & A2 c= C & A1 <> A2 holds A1 \/ A2 = C & A1 /\ A2 = {p1,p2}
proof
let C be Simple_closed_curve, A1,A2 be Subset of TOP-REAL 2, p1,p2 be Point
of TOP-REAL 2 such that
A1: A1 is_an_arc_of p1,p2 and
A2: A2 is_an_arc_of p1,p2 and
A3: A1 c= C and
A4: A2 c= C & A1 <> A2;
A5: p2 in A1 by A1,TOPREAL1:1;
p1 <> p2 & p1 in A1 by A1,JORDAN6:37,TOPREAL1:1;
then consider P1,P2 being non empty Subset of TOP-REAL 2 such that
A6: P1 is_an_arc_of p1,p2 & P2 is_an_arc_of p1,p2 & C = P1 \/ P2 & P1 /\
P2 = {p1,p2} by A3,A5,TOPREAL2:5;
reconsider P1,P2 as non empty Subset of TOP-REAL 2;
A1=P1 or A1=P2 by A1,A3,A6,Th10;
hence thesis by A2,A4,A6,Th10;
end;
theorem Th12:
for A1,A2 being Subset of TOP-REAL 2, p1,p2,q1,q2 being Point of
TOP-REAL 2 st A1 is_an_arc_of p1,p2 & A1 /\ A2 = {q1,q2} holds A1 <> A2
proof
let A1,A2 be Subset of TOP-REAL 2, p1,p2,q1,q2 be Point of TOP-REAL 2 such
that
A1: A1 is_an_arc_of p1,p2 and
A2: A1 /\ A2 = {q1,q2} & A1 = A2;
p1 in A1 by A1,TOPREAL1:1;
then
A3: p1= q1 or p1 = q2 by A2,TARSKI:def 2;
p2 in A1 by A1,TOPREAL1:1;
then
A4: p2= q1 or p2 = q2 by A2,TARSKI:def 2;
ex p3 being Point of TOP-REAL 2 st p3 in A1 & p3<>p1 & p3<>p2 by A1,
JORDAN6:42;
hence contradiction by A1,A2,A3,A4,JORDAN6:37,TARSKI:def 2;
end;
theorem
for C being Simple_closed_curve, A1,A2 being Subset of TOP-REAL 2, p1,
p2 being Point of TOP-REAL 2 st A1 is_an_arc_of p1,p2 & A2 is_an_arc_of p1,p2 &
A1 c= C & A2 c= C & A1 /\ A2 = {p1,p2} holds A1 \/ A2 = C
proof
let C be Simple_closed_curve, A1,A2 be Subset of TOP-REAL 2, p1,p2 be Point
of TOP-REAL 2 such that
A1: A1 is_an_arc_of p1,p2 and
A2: A2 is_an_arc_of p1,p2 and
A3: A1 c= C & A2 c= C and
A4: A1 /\ A2 = {p1,p2};
A1 <> A2 by A2,A4,Th12;
hence thesis by A1,A2,A3,Th11;
end;
theorem
A1 c= C & A2 c= C & A1 <> A2 & A1 is_an_arc_of p1,p2 & A2 is_an_arc_of
p1,p2 implies for A st A is_an_arc_of p1,p2 & A c= C holds A = A1 or A = A2
proof
assume that
A1: A1 c= C & A2 c= C & A1 <> A2 and
A2: A1 is_an_arc_of p1,p2 & A2 is_an_arc_of p1,p2;
A3: A1 \/ A2 = C & A1 /\ A2 = {p1,p2} by A1,A2,Th11;
let A;
assume A is_an_arc_of p1,p2 & A c= C;
hence thesis by A2,A3,Th10;
end;
theorem Th15:
for C being Simple_closed_curve, A being non empty Subset of
TOP-REAL 2 st A is_an_arc_of W-min C, E-max C & A c= C holds A = Lower_Arc C or
A = Upper_Arc C
proof
let C be Simple_closed_curve, A be non empty Subset of TOP-REAL 2 such that
A1: A is_an_arc_of W-min C, E-max C and
A2: A c= C;
A is compact by A1,JORDAN5A:1;
hence thesis by A1,A2,TOPMETR3:15;
end;
theorem Th16:
A is_an_arc_of p1,p2 & LE q1, q2, A, p1, p2 implies ex g being
Function of I[01], (TOP-REAL 2)|A, s1, s2 being Real st g is
being_homeomorphism & g.0 = p1 & g.1 = p2 & g.s1 = q1 & g.s2 = q2 & 0 <= s1 &
s1 <= s2 & s2 <= 1
proof
given f being Function of I[01], (TOP-REAL 2)|A such that
A1: f is being_homeomorphism and
A2: f.0 = p1 & f.1 = p2;
A3: rng f = [#]((TOP-REAL 2)|A) by A1
.= A by PRE_TOPC:def 5;
assume
A4: LE q1, q2, A, p1, p2;
then q1 in A by JORDAN5C:def 3;
then consider u being object such that
A5: u in dom f and
A6: q1 = f.u by A3,FUNCT_1:def 3;
take f;
A7: dom f = [#]I[01] by A1
.= [.0,1.] by BORSUK_1:40;
then reconsider s1 = u as Element of REAL by A5;
A8: s1 <= 1 by A7,A5,XXREAL_1:1;
q2 in A by A4,JORDAN5C:def 3;
then consider u being object such that
A9: u in dom f and
A10: q2 = f.u by A3,FUNCT_1:def 3;
reconsider s2 = u as Element of REAL by A7,A9;
take s1,s2;
thus f is being_homeomorphism & f.0 = p1 & f.1 = p2 by A1,A2;
thus q1 = f.s1 & q2 = f.s2 by A6,A10;
thus 0 <= s1 by A7,A5,XXREAL_1:1;
0 <= s2 & s2 <= 1 by A7,A9,XXREAL_1:1;
hence s1 <= s2 by A1,A2,A4,A6,A10,A8,JORDAN5C:def 3;
thus thesis by A7,A9,XXREAL_1:1;
end;
theorem Th17:
A is_an_arc_of p1,p2 & LE q1, q2, A, p1, p2 & q1 <> q2 implies
ex g being Function of I[01], (TOP-REAL 2)|A, s1, s2 being Real st g is
being_homeomorphism & g.0 = p1 & g.1 = p2 & g.s1 = q1 & g.s2 = q2 & 0 <= s1 &
s1 < s2 & s2 <= 1
proof
assume that
A1: A is_an_arc_of p1,p2 & LE q1, q2, A, p1, p2 and
A2: q1 <> q2;
consider g being Function of I[01], (TOP-REAL 2)|A, s1, s2 being Real such
that
A3: g is being_homeomorphism & g.0 = p1 & g.1 = p2 and
A4: g.s1 = q1 & g.s2 = q2 and
A5: 0 <= s1 and
A6: s1 <= s2 and
A7: s2 <= 1 by A1,Th16;
take g,s1,s2;
thus g is being_homeomorphism & g.0 = p1 & g.1 = p2 & g.s1 = q1 & g.s2 = q2
& 0 <= s1 by A3,A4,A5;
thus s1 < s2 by A2,A4,A6,XXREAL_0:1;
thus thesis by A7;
end;
theorem
LE q1, q2, A, p1, p2 implies Segment(A,p1,p2,q1,q2) is non empty
proof
A1: Segment(A,p1,p2,q1,q2)={q:LE q1,q,A,p1,p2 & LE q,q2,A,p1,p2} by JORDAN6:26;
assume
A2: LE q1, q2, A, p1, p2;
then q2 in A by JORDAN5C:def 3;
then LE q2,q2,A,p1,p2 by JORDAN5C:9;
then q2 in Segment(A,p1,p2,q1,q2) by A2,A1;
hence thesis;
end;
theorem
p in C implies p in Segment(p,W-min C,C) & W-min C in Segment(p,W-min C,C)
proof
A1: Segment(p,W-min C,C) = {p1: LE p,p1,C or p in C & p1=W-min C} by
JORDAN7:def 1;
assume
A2: p in C;
then LE p,p,C by JORDAN6:56;
hence p in Segment(p,W-min C, C) by A1;
thus thesis by A2,A1;
end;
theorem Th20:
for f being Function of R^1, R^1 for a,b being Real st a <> 0 &
f = AffineMap(a,b) holds f is being_homeomorphism
proof
let f be Function of R^1, R^1;
let a,b be Real such that
A1: a <> 0 and
A2: f = AffineMap(a,b);
thus dom f = [#]R^1 by FUNCT_2:def 1;
thus
A3: rng f = [#]R^1 by A1,A2,FCONT_1:55,TOPMETR:17;
thus
A4: f is one-to-one by A1,A2,FCONT_1:50;
for x being Real holds f.x = a*x + b by A2,FCONT_1:def 4;
hence f is continuous by TOPMETR:21;
f is onto by A3,FUNCT_2:def 3;
then f" = (f qua Function)" by A4,TOPS_2:def 4
.= AffineMap(a",-b/a) by A1,A2,FCONT_1:56;
then for x being Real holds f".x = a"*x + -b/a by FCONT_1:def 4;
hence thesis by TOPMETR:21;
end;
theorem Th21:
A is_an_arc_of p1,p2 & LE q1, q2, A, p1, p2 & q1 <> q2 implies
Segment(A,p1,p2,q1,q2) is_an_arc_of q1,q2
proof
assume that
A1: A is_an_arc_of p1,p2 and
A2: LE q1, q2, A, p1, p2 & q1 <> q2;
consider g being Function of I[01], (TOP-REAL 2)|A, s1, s2 being Real such
that
A3: g is being_homeomorphism and
A4: g.0 = p1 & g.1 = p2 and
A5: g.s1 = q1 and
A6: g.s2 = q2 and
A7: 0 <= s1 and
A8: s1 < s2 and
A9: s2 <= 1 by A1,A2,Th17;
reconsider A9 = A as non empty Subset of TOP-REAL 2 by A1,TOPREAL1:1;
set S = Segment(A,p1,p2,q1,q2);
A10: S={q:LE q1,q,A,p1,p2 & LE q,q2,A,p1,p2} by JORDAN6:26;
A11: 0 < s2 - s1 by A8,XREAL_1:50;
set f = (g*AffineMap(s2-s1,s1))| [.0,1.];
reconsider g as Function of I[01], (TOP-REAL 2)|A9;
reconsider m = AffineMap(s2-s1,s1) as Function of R^1,R^1 by TOPMETR:17;
for x being Real holds m.x = (s2-s1)*x + s1 by FCONT_1:def 4;
then reconsider m as continuous Function of R^1, R^1 by TOPMETR:21;
set h = m | I[01];
A12: h = m | [. 0,1 .] by BORSUK_1:40,TMAP_1:def 4;
then
A13: rng h = m.:[. 0,1 .] by RELAT_1:115
.= [.s1,s2-s1+s1.] by A8,FCONT_1:57,XREAL_1:50
.= [.s1,s2.];
then
A14: rng h c= [. 0,1 .] by A7,A9,XXREAL_1:34;
A15: dom m = REAL by FUNCT_2:def 1;
then
A16: dom h = [.0,1.] by A12,RELAT_1:62;
then reconsider h as Function of I[01],I[01] by A14,BORSUK_1:40,RELSET_1:4;
A17: f = g*h by A12,RELAT_1:83;
A18: [.0,1.] = dom g by BORSUK_1:40,FUNCT_2:def 1;
m.: [.0,1.] c= dom g
proof
let e be object;
assume e in m.: [.0,1.];
then
A19: e in [.s1,s2-s1+s1.] by A8,FCONT_1:57,XREAL_1:50;
[.s1,s2.] c= [.0,1.] by A7,A9,XXREAL_1:34;
hence thesis by A18,A19;
end;
then
A20: [.0,1.] c= dom(g*m) by A15,FUNCT_3:3;
then
A21: dom f = [#]I[01] by BORSUK_1:40,RELAT_1:62;
reconsider CIT = Closed-Interval-TSpace(s1,s2) as non empty SubSpace of
I[01] by A7,A8,A9,TOPMETR:20,TREAL_1:3;
[.s1,s2.] c= [.0,1.] by A7,A9,XXREAL_1:34;
then
A22: the carrier of CIT c= dom g by A8,A18,TOPMETR:18;
A23: rng h = the carrier of CIT by A8,A13,TOPMETR:18;
A24: dom f = the carrier of I[01] by A20,BORSUK_1:40,RELAT_1:62;
A25: s1 < 1 by A8,A9,XXREAL_0:2;
for y being object holds y in [#]((TOP-REAL 2)|S)
iff ex x being object st x
in dom f & y = f.x
proof
let y be object;
thus y in [#]((TOP-REAL 2)|S) implies
ex x being object st x in dom f & y = f.x
proof
assume y in [#]((TOP-REAL 2)|S);
then y in S by PRE_TOPC:def 5;
then consider q0 being Point of TOP-REAL 2 such that
A26: y = q0 and
A27: LE q1,q0,A,p1,p2 and
A28: LE q0,q2,A,p1,p2 by A10;
q0 in A by A27,JORDAN5C:def 3;
then q0 in [#]((TOP-REAL 2)|A) by PRE_TOPC:def 5;
then q0 in rng g by A3;
then consider s being object such that
A29: s in dom g and
A30: q0 = g.s by FUNCT_1:def 3;
reconsider s as Real by A29;
take x = (s-s1)/(s2-s1);
A31: s <= 1 by A29,BORSUK_1:40,XXREAL_1:1;
then s <= s2 by A3,A4,A6,A7,A8,A9,A28,A30,JORDAN5C:def 3;
then s-s1 <= s2 - s1 by XREAL_1:9;
then x <= (s2 - s1)/(s2 - s1) by A11,XREAL_1:72;
then
A32: x <= 1 by A11,XCMPLX_1:60;
0 <= s by A29,BORSUK_1:40,XXREAL_1:1;
then s1+0 <= s by A3,A4,A5,A25,A27,A30,A31,JORDAN5C:def 3;
then 0 <= s - s1 by XREAL_1:19;
hence
A33: x in dom f by A11,A21,A32,BORSUK_1:40,XXREAL_1:1;
A34: x in REAL by XREAL_0:def 1;
m.x = (s2-s1)*x + s1 by FCONT_1:def 4
.= s - s1 + s1 by A11,XCMPLX_1:87
.= s;
hence y = (g*m).x by A15,A26,A30,FUNCT_1:13,A34
.= f.x by A33,FUNCT_1:47;
end;
given x be object such that
A35: x in dom f and
A36: y = f.x;
reconsider x as Element of REAL by A35;
AffineMap(s2-s1,s1).x in REAL;
then reconsider s = m.x as Element of REAL;
h.x = m.x by A12,A16,A21,A35,BORSUK_1:40,FUNCT_1:47;
then
A37: s in rng h by A16,A21,A35,BORSUK_1:40,FUNCT_1:def 3;
then
A38: s1 <= s by A13,XXREAL_1:1;
y in rng f by A35,A36,FUNCT_1:def 3;
then y in [#]((TOP-REAL 2)|A);
then y in A by PRE_TOPC:def 5;
then reconsider q = y as Point of TOP-REAL 2;
A39: s <= s2 by A13,A37,XXREAL_1:1;
then
A40: s <= 1 by A9,XXREAL_0:2;
A41: q = (g*m).x by A35,A36,FUNCT_1:47
.= g.s by A15,FUNCT_1:13;
then
A42: LE q1,q,A,p1,p2 by A1,A3,A4,A5,A7,A25,A38,A40,JORDAN5C:8;
LE q,q2,A,p1,p2 by A1,A3,A4,A6,A7,A9,A41,A38,A39,A40,JORDAN5C:8;
then q in S by A10,A42;
hence thesis by PRE_TOPC:def 5;
end;
then
A43: rng f = [#]((TOP-REAL 2)|S) by FUNCT_1:def 3;
then
A44: [#]((TOP-REAL 2)|S) <> {} by A21,RELAT_1:42;
then reconsider f as Function of I[01], (TOP-REAL 2)|S by A24,A43,
FUNCT_2:def 1,RELSET_1:4;
reconsider TS = (TOP-REAL 2)|S as non empty SubSpace of (TOP-REAL 2)|A9 by
A44,Th2,TOPMETR:22;
take f;
A45: AffineMap(s2-s1,s1).0 = s1 by FCONT_1:48;
set o = g | CIT;
A46: dom o = dom(g|the carrier of CIT) by TMAP_1:def 4
.= dom g /\ the carrier of CIT by RELAT_1:61
.= the carrier of CIT by A22,XBOOLE_1:28;
reconsider h as Function of I[01], CIT by A16,A23,RELSET_1:4;
h is onto by A23,FUNCT_2:def 3;
then
A47: h is being_homeomorphism by A11,Th9,Th20;
A48: the carrier of CIT = [.s1,s2.] by A8,TOPMETR:18;
then o = g|rng h by A13,TMAP_1:def 4;
then
A49: f = o*h by A17,FUNCT_4:2;
then
A50: rng o = rng f by A13,A46,A48,RELAT_1:28;
then reconsider o as Function of CIT, TS by A46,RELSET_1:4;
o is onto by A43,A50,FUNCT_2:def 3;
then o is being_homeomorphism by A3,Th9;
hence f is being_homeomorphism by A49,A47,TOPS_2:57;
A51: dom AffineMap(s2-s1,s1) = REAL by FUNCT_2:def 1;
A52: 0 in REAL by XREAL_0:def 1;
0 in [.0,1.] by XXREAL_1:1;
hence f.0 = (g*m).0 by FUNCT_1:49
.=q1 by A5,A45,A51,FUNCT_1:13,A52;
A53: AffineMap(s2-s1,s1).1 = s2-s1+s1 by FCONT_1:49
.= s2;
A54: 1 in REAL by XREAL_0:def 1;
1 in [.0,1.] by XXREAL_1:1;
hence f.1 = (g*m).1 by FUNCT_1:49
.= q2 by A6,A53,A51,FUNCT_1:13,A54;
end;
theorem
for p1,p2 being Point of TOP-REAL 2 for P being Subset of TOP-REAL 2
st P c= C & P is_an_arc_of p1,p2 & W-min C in P & E-max C in P holds Upper_Arc
C c= P or Lower_Arc C c= P
proof
let p1,p2 be Point of TOP-REAL 2;
let P being Subset of TOP-REAL 2 such that
A1: P c= C and
A2: P is_an_arc_of p1,p2 and
A3: W-min C in P and
A4: E-max C in P;
reconsider P9 = P as non empty Subset of TOP-REAL 2 by A3;
A5: W-min C <> E-max C by TOPREAL5:19;
per cases by A2,A3,A4,A5,JORDAN5C:14;
suppose
A6: LE W-min C, E-max C, P,p1,p2;
set S = Segment(P9,p1,p2,W-min C, E-max C);
reconsider S9 = S as non empty Subset of TOP-REAL 2 by A6,Th5;
S c= P by Th2;
then S c= C by A1;
then S9 = Lower_Arc C or S9 = Upper_Arc C by A2,A5,A6,Th15,Th21;
hence thesis by Th2;
end;
suppose
A7: LE E-max C, W-min C, P,p1,p2;
set S = Segment(P9,p1,p2,E-max C, W-min C);
reconsider S9 = S as non empty Subset of TOP-REAL 2 by A7,Th5;
S is_an_arc_of E-max C, W-min C by A2,A5,A7,Th21;
then
A8: S9 is_an_arc_of W-min C, E-max C by JORDAN5B:14;
S c= P by Th2;
hence thesis by A1,A8,Th15,XBOOLE_1:1;
end;
end;
:: Moved from JORDAN18, AK, 23.02.2006
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 & q1 in P & q2 in P & q1 <> p1 & q1 <> p2 & q2 <> p1
& q2 <> p2 & q1 <> q2 ex Q being non empty Subset of TOP-REAL 2 st Q
is_an_arc_of q1,q2 & Q c= P & Q misses {p1,p2}
proof
let P be Subset of TOP-REAL 2, p1,p2,q1,q2 be Point of TOP-REAL 2 such that
A1: P is_an_arc_of p1,p2 and
A2: q1 in P & q2 in P and
A3: q1 <> p1 and
A4: q1 <> p2 and
A5: q2 <> p1 and
A6: q2 <> p2 and
A7: q1 <> q2;
per cases by A1,A2,A7,JORDAN5C:14;
suppose
A8: LE q1,q2,P,p1,p2;
set S = Segment(P,p1,p2,q1,q2);
S is_an_arc_of q1,q2 by A1,A7,A8,Th21;
then reconsider S as non empty Subset of TOP-REAL 2 by TOPREAL1:1;
take S;
thus S is_an_arc_of q1,q2 by A1,A7,A8,Th21;
thus S c= P by Th2;
now
A9: S = {q where q is Point of TOP-REAL 2 : LE q1,q,P,p1,p2 & LE q,q2,P
,p1,p2} by JORDAN6:26;
assume
A10: S meets {p1,p2};
per cases by A10,ZFMISC_1:51;
suppose
p1 in S;
then
ex q being Point of TOP-REAL 2 st q = p1 & LE q1,q,P,p1,p2 & LE q
,q2,P,p1,p2 by A9;
hence contradiction by A1,A3,JORDAN6:54;
end;
suppose
p2 in S;
then
ex q being Point of TOP-REAL 2 st q = p2 & LE q1,q,P,p1,p2 & LE q
,q2,P,p1,p2 by A9;
hence contradiction by A1,A6,JORDAN6:55;
end;
end;
hence thesis;
end;
suppose
A11: LE q2,q1,P,p1,p2;
set S = Segment(P,p1,p2,q2,q1);
S is_an_arc_of q2,q1 by A1,A7,A11,Th21;
then reconsider S as non empty Subset of TOP-REAL 2 by TOPREAL1:1;
take S;
S is_an_arc_of q2,q1 by A1,A7,A11,Th21;
hence S is_an_arc_of q1,q2 by JORDAN5B:14;
thus S c= P by Th2;
now
A12: S = {q where q is Point of TOP-REAL 2 : LE q2,q,P,p1,p2 & LE q,q1,P
,p1,p2} by JORDAN6:26;
assume
A13: S meets {p1,p2};
per cases by A13,ZFMISC_1:51;
suppose
p1 in S;
then
ex q being Point of TOP-REAL 2 st q = p1 & LE q2,q,P,p1,p2 & LE q
,q1,P,p1,p2 by A12;
hence contradiction by A1,A5,JORDAN6:54;
end;
suppose
p2 in S;
then
ex q being Point of TOP-REAL 2 st q = p2 & LE q2,q,P,p1,p2 & LE q
,q1,P,p1,p2 by A12;
hence contradiction by A1,A4,JORDAN6:55;
end;
end;
hence thesis;
end;
end;
:: moved from JORDAN20, AG 1.04.2006
theorem
for P being non empty Subset of TOP-REAL 2, p1,p2,q1 being Point of
TOP-REAL 2 st P is_an_arc_of p1,p2 & q1 in P & p1<>q1 holds Segment(P,p1,p2,p1,
q1) is_an_arc_of p1,q1
proof
let P be non empty Subset of TOP-REAL 2, p1,p2,q1 be Point of TOP-REAL 2;
assume that
A1: P is_an_arc_of p1,p2 and
A2: q1 in P and
A3: p1<>q1;
LE p1,q1,P,p1,p2 by A1,A2,JORDAN5C:10;
hence thesis by A1,A3,Th21;
end;