:: 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-2021 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies NUMBERS, 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;
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 :: JORDAN6:1
r<=s implies r <= (r+s)/2 & (r+s)/2 <= s;
theorem :: JORDAN6:2
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;
theorem :: JORDAN6:3
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;
theorem :: JORDAN6:4
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;
theorem :: JORDAN6:5
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;
theorem :: JORDAN6:6
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;
theorem :: JORDAN6:7
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;
theorem :: JORDAN6:8
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;
theorem :: JORDAN6:9
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;
theorem :: JORDAN6:10
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;
theorem :: JORDAN6:11
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;
theorem :: JORDAN6:12
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;
theorem :: JORDAN6:13
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;
theorem :: JORDAN6:14
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;
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
:: JORDAN6:def 1
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);
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
:: JORDAN6:def 2
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);
end;
theorem :: JORDAN6:15
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;
theorem :: JORDAN6:16
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;
theorem :: JORDAN6:17
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;
begin ::Segments of Arcs
theorem :: JORDAN6:18
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;
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
:: JORDAN6:def 3
{q : LE q,q1,P,p1,p2};
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
:: JORDAN6:def 4
{q: LE q1,q,P,p1,p2};
end;
theorem :: JORDAN6:19
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;
theorem :: JORDAN6:20
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;
theorem :: JORDAN6:21
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};
theorem :: JORDAN6:22
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;
theorem :: JORDAN6:23
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};
theorem :: JORDAN6:24
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;
theorem :: JORDAN6:25
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);
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
:: JORDAN6:def 5
R_Segment(P,p1,p2,q1) /\ L_Segment(P,p1,p2,q2);
end;
theorem :: JORDAN6:26
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};
theorem :: JORDAN6:27
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;
theorem :: JORDAN6:28
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);
theorem :: JORDAN6:29
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);
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
:: JORDAN6:def 6
{p where p is Point of TOP-REAL 2: p`1=s};
func Horizontal_Line(s) -> Subset of TOP-REAL 2 equals
:: JORDAN6:def 7
{p: p`2=s};
end;
theorem :: JORDAN6:30
for r being Real holds
Vertical_Line(r) is closed & Horizontal_Line(r) is closed;
theorem :: JORDAN6:31
for r being Real,p being Point of TOP-REAL 2 holds
p in Vertical_Line(r) iff p`1=r;
theorem :: JORDAN6:32
for r being Real,p being Point of TOP-REAL 2 holds
p in Horizontal_Line(r) iff p`2=r;
theorem :: JORDAN6:33
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;
begin ::Uniqueness of Decomposition of a Simple Closed Curve
theorem :: JORDAN6:34
for P being Subset of I[01] st
P=(the carrier of I[01]) \{0,1} holds P is open;
theorem :: JORDAN6:35
for P being Subset of R^1, r,s being Real st P=].r,s.[ holds P is open;
theorem :: JORDAN6:36
for P7 being Subset of I[01] st
P7=(the carrier of I[01]) \{0,1} holds P7<>{} & P7 is connected;
theorem :: JORDAN6:37
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;
theorem :: JORDAN6:38
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;
::A proof of the following is almost same as JORDAN5A:1.
theorem :: JORDAN6:39
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;
theorem :: JORDAN6:40
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;
theorem :: JORDAN6:41
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;
theorem :: JORDAN6:42
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;
theorem :: JORDAN6:43
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}<>{};
theorem :: JORDAN6:44
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;
theorem :: JORDAN6:45
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;
theorem :: JORDAN6:46
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;
theorem :: JORDAN6:47
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;
theorem :: JORDAN6:48
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;
begin
theorem :: JORDAN6:49
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;
definition
let P be Subset of TOP-REAL 2 such that
P is being_simple_closed_curve;
func Upper_Arc(P) -> non empty Subset of TOP-REAL 2 means
:: JORDAN6:def 8
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;
end;
definition
let P be Subset of TOP-REAL 2;
assume
P is being_simple_closed_curve;
func Lower_Arc(P) -> non empty Subset of TOP-REAL 2 means
:: JORDAN6:def 9
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;
end;
theorem :: JORDAN6:50
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;
theorem :: JORDAN6:51
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)};
theorem :: JORDAN6:52
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);
theorem :: JORDAN6:53
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);
begin ::An Order of Points in a Simple Closed Curve
theorem :: JORDAN6:54
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;
theorem :: JORDAN6:55
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;
definition
let P be Subset of TOP-REAL 2, q1,q2 be Point of TOP-REAL 2;
pred LE q1,q2,P means
:: JORDAN6:def 10
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 :: JORDAN6:56
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;
theorem :: JORDAN6:57
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;
theorem :: JORDAN6:58
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;
theorem :: JORDAN6:59
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);
theorem :: JORDAN6:60
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);
registration
let S be non empty being_simple_closed_curve Subset of TOP-REAL 2;
cluster Lower_Arc S -> non empty compact;
cluster Upper_Arc S -> non empty compact;
end;
theorem :: JORDAN6:61
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;
reserve C for Simple_closed_curve;
definition
let C be Simple_closed_curve;
func Lower_Middle_Point C -> Point of TOP-REAL 2 equals
:: JORDAN6:def 11
First_Point(Lower_Arc C,W-min C,E-max C,
Vertical_Line((W-bound C+E-bound C)/2));
func Upper_Middle_Point C -> Point of TOP-REAL 2 equals
:: JORDAN6:def 12
First_Point(Upper_Arc C,W-min C,E-max C,
Vertical_Line((W-bound C+E-bound C)/2));
end;
theorem :: JORDAN6:62
Lower_Arc C meets Vertical_Line((W-bound C+E-bound C)/2);
theorem :: JORDAN6:63
Upper_Arc C meets Vertical_Line((W-bound C+E-bound C)/2);
theorem :: JORDAN6:64
(Lower_Middle_Point C)`1 = (W-bound C+E-bound C)/2;
theorem :: JORDAN6:65
(Upper_Middle_Point C)`1 = (W-bound C+E-bound C)/2;
theorem :: JORDAN6:66
Lower_Middle_Point C in Lower_Arc C;
theorem :: JORDAN6:67
Upper_Middle_Point C in Upper_Arc C;
theorem :: JORDAN6:68
Upper_Middle_Point C in C;
theorem :: JORDAN6:69 :: 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;
theorem :: JORDAN6:70 :: 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;