:: On the Segmentation of a Simple Closed Curve
:: by Andrzej Trybulec
::
:: Received August 18, 2003
:: Copyright (c) 2003-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, PRE_TOPC, EUCLID, SUBSET_1, XBOOLE_0,
ORDINAL2, PSCOMP_1, RCOMP_1, RELAT_1, FUNCT_1, TOPMETR, TARSKI, XXREAL_2,
ZFMISC_1, XXREAL_0, STRUCT_0, CARD_1, ARYTM_3, SEQ_4, JORDAN6, JORDAN3,
COMPLEX1, ARYTM_1, CONNSP_2, SETFAM_1, XXREAL_1, PCOMPS_1, METRIC_1,
REAL_1, WEIERSTR, TOPREAL1, FINSEQ_1, PARTFUN1, GOBRD10, MEASURE5,
FINSET_1, JORDAN_A, NAT_1, CHORD, FUNCT_7;
notations TARSKI, XBOOLE_0, SUBSET_1, ZFMISC_1, ORDINAL1, NUMBERS, XCMPLX_0,
XREAL_0, REAL_1, NAT_1, FINSET_1, FUNCT_1, RELSET_1, PARTFUN1, FUNCT_2,
BINOP_1, FINSEQ_1, NAT_D, XXREAL_2, SEQ_4, RCOMP_1, TOPMETR, CONNSP_2,
STRUCT_0, PRE_TOPC, TBSP_1, COMPTS_1, METRIC_1, RLVECT_1, EUCLID,
TOPREAL1, TOPREAL2, GOBRD10, WEIERSTR, PCOMPS_1, JORDAN5C, JORDAN6,
JORDAN7, MEASURE6, PSCOMP_1, JORDAN1K, XXREAL_0, BORSUK_1;
constructors REAL_1, RCOMP_1, NAT_D, TOPS_2, TBSP_1, TOPREAL1, MEASURE6,
GOBRD10, JORDAN5C, JORDAN6, JORDAN7, JORDAN1K, SEQ_4, FUNCSDOM, BINOP_2,
RVSUM_1, PSCOMP_1;
registrations XBOOLE_0, SUBSET_1, ORDINAL1, RELSET_1, FINSET_1, NUMBERS,
XREAL_0, MEMBERED, FINSEQ_1, RCOMP_1, STRUCT_0, COMPTS_1, BORSUK_1,
EUCLID, TOPMETR, TOPREAL1, TOPREAL2, PSCOMP_1, WAYBEL_2, TOPREAL6,
XXREAL_2, PCOMPS_1, PRE_TOPC, MEASURE6, ZFMISC_1, FUNCT_1, JORDAN5A;
requirements NUMERALS, SUBSET, BOOLE, REAL, ARITHM;
definitions XBOOLE_0, TARSKI, PSCOMP_1;
equalities EUCLID, BINOP_1;
expansions XBOOLE_0, TARSKI, PSCOMP_1;
theorems EUCLID, PCOMPS_1, FINSEQ_3, NAT_1, FINSEQ_5, JGRAPH_1, SPPOL_1,
ZFMISC_1, JORDAN7, SPRECT_1, JORDAN6, XBOOLE_1, REVROT_1, JORDAN5A,
JORDAN5C, SEQ_4, PARTFUN2, WEIERSTR, SUBSET_1, METRIC_1, TOPREAL3,
TARSKI, XBOOLE_0, TOPRNS_1, BORSUK_1, JORDAN16, JORDAN1K, RCOMP_1,
BORSUK_3, TOPREAL6, TOPMETR, FUNCT_2, BINOP_1, TOPS_1, CONNSP_2, FUNCT_1,
RELAT_1, TOPREAL5, JORDAN17, TOPREAL1, TOPREAL8, GOBRD10, ORDINAL1,
XREAL_0, XREAL_1, XXREAL_0, GOBOARD6, PARTFUN1, CARD_1, XXREAL_2,
XXREAL_1, NAT_D, COMPTS_1, MEASURE6, RLVECT_1, FINSEQ_6;
schemes DOMAIN_1, FRAENKEL, FUNCT_7, TOPREAL1;
begin :: Preliminaries
reserve C for Simple_closed_curve,
p,q,p1 for Point of TOP-REAL 2,
i,j,k,n for Nat,
r,s for Real;
theorem Th1:
for T being non empty TopSpace, f being continuous RealMap of T,
A being compact Subset of T holds f.:A is compact
proof
let T be non empty TopSpace, f be continuous RealMap of T,
A be compact Subset of T;
reconsider g = f as continuous Function of T,R^1 by JORDAN5A:27,TOPMETR:17;
[#](g.:A) is compact by WEIERSTR:9,13;
hence thesis by WEIERSTR:def 1;
end;
theorem Th2:
for A being compact Subset of REAL, B being non empty Subset of REAL st B c= A
holds lower_bound B in A
proof
let A be compact Subset of REAL, B be non empty Subset of REAL such that
A1: B c= A;
A2: A is real-bounded by RCOMP_1:10;
then
A3: B is bounded_below by A1,XXREAL_2:44;
A4: Cl B c= A by A1,MEASURE6:57;
Cl B is bounded_below by A1,A2,MEASURE6:57,XXREAL_2:44;
then lower_bound Cl B in Cl B by RCOMP_1:13;
then lower_bound Cl B in A by A4;
hence thesis by A3,TOPREAL6:68;
end;
theorem
for A,B being compact non empty Subset of TOP-REAL n,
f being continuous RealMap of [:TOP-REAL n, TOP-REAL n:],
g being RealMap of TOP-REAL n st for p being Point of TOP-REAL n
ex G being Subset of REAL
st G = { f.(p,q) where q is Point of TOP-REAL n : q in B } &
g.p = lower_bound G
holds lower_bound(f.:[:A,B:]) = lower_bound(g.:A)
proof
let A,B be compact non empty Subset of TOP-REAL n;
let f be continuous RealMap of [:TOP-REAL n, TOP-REAL n:];
let g being RealMap of TOP-REAL n such that
A1: for p being Point of TOP-REAL n ex G being Subset of REAL st
G = { f.(p,q) where q is Point of TOP-REAL n : q in B } &
g.p = lower_bound G;
A2: [:A,B:] is compact by BORSUK_3:23;
then
A3: f.:[:A,B:] is compact by Th1;
A4: f.:[:A,B:] is real-bounded by A2,Th1,RCOMP_1:10;
A5: g.:A c= f.:[:A,B:]
proof
let u be object;
assume u in g.:A;
then consider p being Point of TOP-REAL n such that
A6: p in A and
A7: u = g.p by FUNCT_2:65;
consider q being Point of TOP-REAL n such that
A8: q in B by SUBSET_1:4;
consider G being Subset of REAL such that
A9: G = { f.(p,q1) where q1 is Point of TOP-REAL n : q1 in B } and
A10: u = lower_bound G by A1,A7;
A11: f.(p,q) in G by A8,A9;
G c= f.:[:A,B:]
proof
let u be object;
assume u in G;
then consider q1 being Point of TOP-REAL n such that
A12: u = f.(p,q1) and
A13: q1 in B by A9;
[p,q1] in [:A,B:] by A6,A13,ZFMISC_1:87;
hence thesis by A12,FUNCT_2:35;
end;
hence thesis by A3,A10,A11,Th2;
end;
then
A14: g.:A is bounded_below by A4,XXREAL_2:44;
A15: for r st r in f.:[:A,B:] holds lower_bound(g.:A)<=r
proof
let r;
assume r in f.:[:A,B:];
then consider pq being Point of [:TOP-REAL n, TOP-REAL n:] such that
A16: pq in [:A,B:] and
A17: r = f.pq by FUNCT_2:65;
pq in the carrier of [:TOP-REAL n, TOP-REAL n:];
then pq in [:the carrier of TOP-REAL n, the carrier of TOP-REAL n:]
by BORSUK_1:def 2;
then consider p,q being object such that
A18: p in the carrier of TOP-REAL n and
A19: q in the carrier of TOP-REAL n and
A20: pq = [p,q] by ZFMISC_1:84;
A21: q in B by A16,A20,ZFMISC_1:87;
reconsider p,q as Point of TOP-REAL n by A18,A19;
consider G being Subset of REAL such that
A22: G = { f.(p,q1) where q1 is Point of TOP-REAL n : q1 in B } and
A23: g.p = lower_bound G by A1;
A24: p in A by A16,A20,ZFMISC_1:87;
G c= f.:[:A,B:]
proof
let u be object;
assume u in G;
then consider q1 being Point of TOP-REAL n such that
A25: u = f.(p,q1) and
A26: q1 in B by A22;
[p,q1] in [:A,B:] by A24,A26,ZFMISC_1:87;
hence thesis by A25,FUNCT_2:35;
end;
then
A27: G is bounded_below by A4,XXREAL_2:44;
r = f.(p,q) by A17,A20;
then r in G by A21,A22;
then
A28: g.p <= r by A23,A27,SEQ_4:def 2;
g.p in g.:A by A24,FUNCT_2:35;
then lower_bound(g.:A)<=g.p by A14,SEQ_4:def 2;
hence thesis by A28,XXREAL_0:2;
end;
for s st 0<s ex r st r in f.:[:A,B:] & r<lower_bound(g.:A)+s
proof
let s;
assume 0<s;
then consider r such that
A29: r in g.:A and
A30: r<lower_bound(g.:A)+s by A14,SEQ_4:def 2;
take r;
thus r in f.:[:A,B:] by A5,A29;
thus thesis by A30;
end;
hence thesis by A4,A15,SEQ_4:def 2;
end;
theorem
for A,B being compact non empty Subset of TOP-REAL n,
f being continuous RealMap of [:TOP-REAL n, TOP-REAL n:],
g being RealMap of TOP-REAL n st for q being Point of TOP-REAL n
ex G being Subset of REAL
st G = { f.(p,q) where p is Point of TOP-REAL n : p in A } &
g.q = lower_bound G
holds lower_bound(f.:[:A,B:]) = lower_bound(g.:B )
proof
let A,B be compact non empty Subset of TOP-REAL n;
let f be continuous RealMap of [:TOP-REAL n, TOP-REAL n:];
let g being RealMap of TOP-REAL n such that
A1: for q being Point of TOP-REAL n ex G being Subset of REAL st
G = { f.(p,q) where p is Point of TOP-REAL n : p in A } &
g.q = lower_bound G;
A2: [:A,B:] is compact by BORSUK_3:23;
then
A3: f.:[:A,B:] is compact by Th1;
A4: f.:[:A,B:] is real-bounded by A2,Th1,RCOMP_1:10;
A5: g.:B c= f.:[:A,B:]
proof
let u be object;
assume u in g.:B;
then consider q being Point of TOP-REAL n such that
A6: q in B and
A7: u = g.q by FUNCT_2:65;
consider p being Point of TOP-REAL n such that
A8: p in A by SUBSET_1:4;
consider G being Subset of REAL such that
A9: G = { f.(p1,q) where p1 is Point of TOP-REAL n : p1 in A } and
A10: u = lower_bound G by A1,A7;
A11: f.(p,q) in G by A8,A9;
G c= f.:[:A,B:]
proof
let u be object;
assume u in G;
then consider p1 being Point of TOP-REAL n such that
A12: u = f.(p1,q) and
A13: p1 in A by A9;
[p1,q] in [:A,B:] by A6,A13,ZFMISC_1:87;
hence thesis by A12,FUNCT_2:35;
end;
hence thesis by A3,A10,A11,Th2;
end;
then
A14: g.:B is bounded_below by A4,XXREAL_2:44;
A15: for r st r in f.:[:A,B:] holds lower_bound(g.:B)<=r
proof
let r;
assume r in f.:[:A,B:];
then consider pq being Point of [:TOP-REAL n, TOP-REAL n:] such that
A16: pq in [:A,B:] and
A17: r = f.pq by FUNCT_2:65;
pq in the carrier of [:TOP-REAL n, TOP-REAL n:];
then pq in [:the carrier of TOP-REAL n, the carrier of TOP-REAL n:]
by BORSUK_1:def 2;
then consider p,q being object such that
A18: p in the carrier of TOP-REAL n and
A19: q in the carrier of TOP-REAL n and
A20: pq = [p,q] by ZFMISC_1:84;
A21: p in A by A16,A20,ZFMISC_1:87;
reconsider p,q as Point of TOP-REAL n by A18,A19;
consider G being Subset of REAL such that
A22: G = { f.(p1,q) where p1 is Point of TOP-REAL n : p1 in A } and
A23: g.q = lower_bound G by A1;
A24: q in B by A16,A20,ZFMISC_1:87;
G c= f.:[:A,B:]
proof
let u be object;
assume u in G;
then consider p1 being Point of TOP-REAL n such that
A25: u = f.(p1,q) and
A26: p1 in A by A22;
[p1,q] in [:A,B:] by A24,A26,ZFMISC_1:87;
hence thesis by A25,FUNCT_2:35;
end;
then
A27: G is bounded_below by A4,XXREAL_2:44;
r = f.(p,q) by A17,A20;
then r in G by A21,A22;
then
A28: g.q <= r by A23,A27,SEQ_4:def 2;
g.q in g.:B by A24,FUNCT_2:35;
then lower_bound(g.:B)<=g.q by A14,SEQ_4:def 2;
hence thesis by A28,XXREAL_0:2;
end;
for s st 0<s ex r st r in f.:[:A,B:] & r<lower_bound(g.:B)+s
proof
let s;
assume 0<s;
then consider r such that
A29: r in g.:B and
A30: r<lower_bound(g.:B)+s by A14,SEQ_4:def 2;
take r;
thus r in f.:[:A,B:] by A5,A29;
thus thesis by A30;
end;
hence thesis by A4,A15,SEQ_4:def 2;
end;
theorem Th5:
q in Lower_Arc C & q <> W-min C implies LE E-max C, q, C
proof
E-max C in Upper_Arc C by JORDAN7:1;
hence thesis by JORDAN6:def 10;
end;
theorem Th6:
q in Upper_Arc C implies LE q, E-max C, C
proof
A1: E-max C in Lower_Arc C by JORDAN7:1;
E-max C <> W-min C by TOPREAL5:19;
hence thesis by A1,JORDAN6:def 10;
end;
begin :: The Euclidean distance
definition
let n;
A1: [:the carrier of TOP-REAL n, the carrier of TOP-REAL n:]
= the carrier of [:TOP-REAL n, TOP-REAL n:] by BORSUK_1:def 2;
func Eucl_dist n -> RealMap of [:TOP-REAL n, TOP-REAL n:] means
:Def1:
for p,q being Point of TOP-REAL n holds it.(p,q) =|.p - q.|;
existence
proof
deffunc F(Point of TOP-REAL n,Point of TOP-REAL n) = |.$1 - $2.|;
A2: for p,q being Point of TOP-REAL n holds F(p,q) in REAL by XREAL_0:def 1;
consider f
being Function of [:the carrier of TOP-REAL n, the carrier of TOP-REAL n:],
REAL such that
A3: for p,q being Point of TOP-REAL n holds f.(p,q) = F(p,q)
from FUNCT_7:sch 1(A2);
reconsider f as RealMap of [:TOP-REAL n, TOP-REAL n:] by A1;
take f;
let p,q being Point of TOP-REAL n;
thus thesis by A3;
end;
uniqueness
proof
let IT1,IT2 be RealMap of [:TOP-REAL n, TOP-REAL n:] such that
A4: for p,q being Point of TOP-REAL n holds IT1.(p,q) =|.p - q.| and
A5: for p,q being Point of TOP-REAL n holds IT2.(p,q) =|.p - q.|;
now
let p,q be Point of TOP-REAL n;
thus IT1.(p,q) = |.p - q.| by A4
.= IT2.(p,q) by A5;
end;
hence thesis by A1,BINOP_1:2;
end;
end;
definition
let T be non empty TopSpace, f be RealMap of T;
redefine attr f is continuous means :: redefines continuous (PSCOMP_1, definition)
for p being Point of T, N being Neighbourhood of f.p
ex V being a_neighborhood of p st f.:V c= N;
compatibility
proof
thus f is continuous implies
for p being Point of T, N being Neighbourhood of f.p
ex V being a_neighborhood of p st f.:V c= N
proof
assume
A1: f is continuous;
let p be Point of T, N be Neighbourhood of f.p;
A2: f"(N`) = (f"N)` by FUNCT_2:100;
N` is closed by RCOMP_1:def 5;
then f"(N`) is closed by A1;
then
A3: f"N is open by A2,TOPS_1:4;
f.p in N by RCOMP_1:16;
then p in f"N by FUNCT_2:38;
then reconsider V = f"N as a_neighborhood of p by A3,CONNSP_2:3;
take V;
thus thesis by FUNCT_1:75;
end;
assume
A4: for p being Point of T, N being Neighbourhood of f.p
ex V being a_neighborhood of p st f.:V c= N;
let Y be Subset of REAL;
assume Y is closed;
then Y`` is closed;
then
A5: Y` is open by RCOMP_1:def 5;
for p being Point of T st p in (f"Y)` ex A being Subset of T st
A is a_neighborhood of p & A c= (f"Y)`
proof
let p be Point of T;
assume p in (f"Y)`;
then p in f"Y` by FUNCT_2:100;
then f.p in Y` by FUNCT_2:38;
then consider N being Neighbourhood of f.p such that
A6: N c= Y` by A5,RCOMP_1:18;
consider V being a_neighborhood of p such that
A7: f.:V c= N by A4;
take V;
thus V is a_neighborhood of p;
f.:V c= Y` by A6,A7;
then
A8: f"(f.:V) c= f"Y` by RELAT_1:143;
V c= f"(f.:V) by FUNCT_2:42;
then V c= f"Y` by A8;
hence thesis by FUNCT_2:100;
end;
then (f"Y)` is open by CONNSP_2:7;
then (f"Y)`` is closed by TOPS_1:4;
hence thesis;
end;
end;
Lm1: for X,Y being TopSpace holds
the TopStruct of [:X,Y:] = [: the TopStruct of X, the TopStruct of Y:]
proof
let X,Y be TopSpace;
set T = [: the TopStruct of X, the TopStruct of Y:];
A1: the carrier of T = [: the carrier of the TopStruct of X,
the carrier of the TopStruct of Y:] by BORSUK_1:def 2
.= the carrier of [:X,Y:] by BORSUK_1:def 2;
set tau1 = { union A where A is Subset-Family of T:
A c= { [:X1,Y1:]
where X1 is Subset of the TopStruct of X,
Y1 is Subset of the TopStruct of Y :
X1 in the topology of the TopStruct of X &
Y1 in the topology of the TopStruct of Y}};
set tau2 =
{ union A where A is Subset-Family of T:
A c= { [:X1,Y1:]
where X1 is Subset of X,
Y1 is Subset of Y :
X1 in the topology of X &
Y1 in the topology of Y}};
the topology of T = tau1 by BORSUK_1:def 2
.= tau2
.= the topology of [:X,Y:] by A1,BORSUK_1:def 2;
hence thesis by A1;
end;
registration
let n;
cluster Eucl_dist n -> continuous;
coherence
proof
set f = Eucl_dist n;
let p being Point of [:TOP-REAL n, TOP-REAL n:],
N being Neighbourhood of f.p;
consider r such that
A1: 0<r and
A2: N = ].f.p-r,f.p+r.[ by RCOMP_1:def 6;
p in the carrier of [:TOP-REAL n, TOP-REAL n:];
then p in [:the carrier of TOP-REAL n, the carrier of TOP-REAL n:]
by BORSUK_1:def 2;
then consider p1,p2 being object such that
A3: p1 in the carrier of TOP-REAL n and
A4: p2 in the carrier of TOP-REAL n and
A5: p = [p1,p2] by ZFMISC_1:84;
reconsider p1,p2 as Point of TOP-REAL n by A3,A4;
reconsider p19=p1, p29=p2 as Element of Euclid n by TOPREAL3:8;
A6: the TopStruct of TOP-REAL n = TopSpaceMetr Euclid n by EUCLID:def 8;
then reconsider q1=p1, q2=p2 as Point of TopSpaceMetr Euclid n;
reconsider U = Ball(p19,r/2) as a_neighborhood of q1 by A1,GOBOARD6:91
,XREAL_1:215;
reconsider W = Ball(p29,r/2) as a_neighborhood of q2 by A1,GOBOARD6:91
,XREAL_1:215;
reconsider V = [:U,W:]
as a_neighborhood of p by A5,A6,Lm1;
take V;
let s be object;
assume
A7: s in f.:V;
then reconsider s as Real;
consider q being Point of [:TOP-REAL n, TOP-REAL n:] such that
A8: q in V and
A9: f.q = s by A7,FUNCT_2:65;
q in the carrier of [:TOP-REAL n, TOP-REAL n:];
then q in [:the carrier of TOP-REAL n, the carrier of TOP-REAL n:]
by BORSUK_1:def 2;
then consider q1,q2 being object such that
A10: q1 in the carrier of TOP-REAL n and
A11: q2 in the carrier of TOP-REAL n and
A12: q = [q1,q2] by ZFMISC_1:84;
reconsider q1,q2 as Point of TOP-REAL n by A10,A11;
reconsider q19=q1, q29=q2 as Element of Euclid n by TOPREAL3:8;
reconsider q199=q19, q299=q29, p199=p19, p299=p29 as Element of REAL n;
A13: q19 in Ball(p19,r/2) by A8,A12,ZFMISC_1:87;
A14: q29 in Ball(p29,r/2) by A8,A12,ZFMISC_1:87;
A15: dist(q19,p19) < r/2 by A13,METRIC_1:11;
A16: dist(q29,p29) < r/2 by A14,METRIC_1:11;
A17: |.q1-p1.| < r/2 by A15,SPPOL_1:5;
|.q2-p2.| < r/2 by A16,SPPOL_1:5;
then
A18: |.q1-p1.|+|.q2-p2.| < r/2+r/2 by A17,XREAL_1:8;
A19: for p,q being Point of TOP-REAL n holds f. [p,q] =|.p - q.|
proof
let p,q be Point of TOP-REAL n;
thus f. [p,q] = f.(p,q) .=|.p - q.| by Def1;
end;
then
A20: f.p = |.p1-p2.| by A5;
A21: s = |.q1-q2.| by A9,A12,A19;
A22: q1-q2-(p1-p2) = q1-q2-p1+p2 by RLVECT_1:29
.= q1-(q2+p1)+p2 by RLVECT_1:27
.= q1-p1-q2+p2 by RLVECT_1:27
.= (q1-p1)-(q2-p2) by RLVECT_1:29;
A23: |.(q1-p1)-(q2-p2).| <= |.q1-p1.| + |.q2-p2.| by TOPRNS_1:30;
A24: s - f.p <= |.(q1-q2)-(p1-p2).| by A20,A21,TOPRNS_1:32;
f.p - s <= |.(p1-p2)-(q1-q2).| by A20,A21,TOPRNS_1:32;
then f.p - s <= |.(q1-q2)-(p1-p2).| by TOPRNS_1:27;
then f.p - s <= |.q1-p1.| + |.q2-p2.| by A22,A23,XXREAL_0:2;
then f.p - s < r by A18,XXREAL_0:2;
then
A25: f.p-r < s by XREAL_1:11;
s - f.p <= |.q1-p1.| + |.q2-p2.| by A22,A23,A24,XXREAL_0:2;
then s - f.p < r by A18,XXREAL_0:2;
then s < f.p+r by XREAL_1:19;
hence thesis by A2,A25,XXREAL_1:4;
end;
end;
begin :: On the distance between subsets of a Euclidean space
theorem Th7:
:: JORDAN1K:39, JGRAPH_1:55
for A,B being non empty compact Subset of TOP-REAL n st A misses B
holds dist_min(A,B) > 0
proof
let A,B be non empty compact Subset of TOP-REAL n such that
A1: A misses B;
A2: the TopStruct of TOP-REAL n = TopSpaceMetr Euclid n by EUCLID:def 8;
consider A9,B9 being Subset of TopSpaceMetr Euclid n such that
A3: A = A9 and
A4: B = B9 and
A5: dist_min(A,B) = min_dist_min(A9,B9) by JORDAN1K:def 1;
A6: A9 is compact by A2,A3,COMPTS_1:23;
B9 is compact by A2,A4,COMPTS_1:23;
hence thesis by A1,A3,A4,A5,A6,JGRAPH_1:38;
end;
begin :: On the segments
theorem Th8:
LE p,q,C & LE q, E-max C, C & p <> q implies
Segment(p,q,C) = Segment(Upper_Arc C,W-min C,E-max C,p,q)
proof
assume that
A1: LE p,q,C and
A2: LE q, E-max C, C and
A3: p <> q;
A4: Upper_Arc C is_an_arc_of W-min C,E-max C by JORDAN6:50;
A5: LE p, E-max C, C by A1,A2,JORDAN6:58;
A6: p in Upper_Arc C by A1,A2,JORDAN17:3,JORDAN6:58;
A7: q in Upper_Arc C by A2,JORDAN17:3;
A8: Upper_Arc C c= C by JORDAN6:61;
A9: now
assume q = W-min C;
then LE q,p,C by A6,A8,JORDAN7:3;
hence contradiction by A1,A3,JORDAN6:57;
end;
defpred P[Point of TOP-REAL 2] means LE p,$1,C & LE $1,q,C;
defpred Q[Point of TOP-REAL 2] means LE p,$1,Upper_Arc C,W-min C,E-max C &
LE $1,q,Upper_Arc C,W-min C,E-max C;
A10: P[p1] iff Q[p1]
proof
hereby
assume that
A11: LE p,p1,C and
A12: LE p1,q,C;
hereby per cases;
suppose p1 = E-max C;
hence LE p,p1,Upper_Arc C,W-min C,E-max C by A4,A6,JORDAN5C:10;
end;
suppose p1 = W-min C;
then LE p1,p,C by A6,A8,JORDAN7:3;
then p = p1 by A11,JORDAN6:57;
hence LE p,p1,Upper_Arc C,W-min C,E-max C by A5,JORDAN17:3,JORDAN5C:9;
end;
suppose that
A13: p1 <> E-max C and
A14: p1 <> W-min C;
now
assume
A15: p1 in Lower_Arc C;
p1 in Upper_Arc C by A2,A12,JORDAN17:3,JORDAN6:58;
then p1 in Upper_Arc C /\ Lower_Arc C by A15,XBOOLE_0:def 4;
then p1 in {W-min C,E-max C} by JORDAN6:50;
hence contradiction by A13,A14,TARSKI:def 2;
end;
hence LE p,p1,Upper_Arc C,W-min C,E-max C by A11,JORDAN6:def 10;
end;
end;
per cases;
suppose
A16: q = E-max C;
then p1 in Upper_Arc C by A12,JORDAN17:3;
hence LE p1,q,Upper_Arc C,W-min C,E-max C by A4,A16,JORDAN5C:10;
end;
suppose
A17: q <> E-max C;
now
assume q in Lower_Arc C;
then q in Upper_Arc C /\ Lower_Arc C by A7,XBOOLE_0:def 4;
then q in {W-min C,E-max C} by JORDAN6:50;
hence contradiction by A9,A17,TARSKI:def 2;
end;
hence LE p1,q,Upper_Arc C,W-min C,E-max C by A12,JORDAN6:def 10;
end;
end;
assume that
A18: LE p,p1,Upper_Arc C,W-min C,E-max C and
A19: LE p1,q,Upper_Arc C,W-min C,E-max C;
A20: p1 in Upper_Arc C by A18,JORDAN5C:def 3;
hence LE p,p1,C by A6,A18,JORDAN6:def 10;
thus thesis by A7,A19,A20,JORDAN6:def 10;
end;
deffunc F(set) = $1;
set X = {F(p1): P[p1]}, Y = {F(p1): Q[p1]};
A21: X = Y from FRAENKEL:sch 3(A10);
Segment(p,q,C) = X by A9,JORDAN7:def 1;
hence thesis by A21,JORDAN6:26;
end;
theorem Th9:
LE E-max C, q, C implies
Segment(E-max C,q,C) = Segment(Lower_Arc C,E-max C,W-min C,E-max C,q)
proof
set p = E-max C;
assume
A1: LE E-max C, q, C;
A2: Lower_Arc C is_an_arc_of E-max C,W-min C by JORDAN6:50;
A3: p in Lower_Arc C by JORDAN7:1;
A4: q in Lower_Arc C by A1,JORDAN17:4;
A5: Lower_Arc C c= C by JORDAN6:61;
A6: now
assume
A7: q = W-min C;
then p = q by A1,JORDAN7:2;
hence contradiction by A7,TOPREAL5:19;
end;
defpred P[Point of TOP-REAL 2] means LE p,$1,C & LE $1,q,C;
defpred Q[Point of TOP-REAL 2] means LE p,$1,Lower_Arc C,E-max C,W-min C &
LE $1,q,Lower_Arc C,E-max C, W-min C;
A8: P[p1] iff Q[p1]
proof
hereby
assume that
A9: LE p,p1,C and
A10: LE p1,q,C;
A11: p1 in Lower_Arc C by A9,JORDAN17:4;
hence LE p,p1,Lower_Arc C,E-max C,W-min C by A2,JORDAN5C:10;
per cases;
suppose
A12: p1 = E-max C;
then q in Lower_Arc C by A10,JORDAN17:4;
hence LE p1,q,Lower_Arc C,E-max C,W-min C by A2,A12,JORDAN5C:10;
end;
suppose
A13: p1 <> E-max C;
A14: now
assume
A15: p1 = W-min C;
then LE p1,p, C by A3,A5,JORDAN7:3;
hence contradiction by A9,A15,JORDAN6:57,TOPREAL5:19;
end;
now
assume p1 in Upper_Arc C;
then p1 in Upper_Arc C /\ Lower_Arc C by A11,XBOOLE_0:def 4;
then p1 in {W-min C,E-max C} by JORDAN6:50;
hence contradiction by A13,A14,TARSKI:def 2;
end;
hence LE p1,q,Lower_Arc C,E-max C,W-min C by A10,JORDAN6:def 10;
end;
end;
assume that
A16: LE p,p1,Lower_Arc C,E-max C,W-min C and
A17: LE p1,q,Lower_Arc C,E-max C,W-min C;
A18: p1 in Lower_Arc C by A16,JORDAN5C:def 3;
p1 <> W-min C by A2,A6,A17,JORDAN6:55;
hence LE p,p1,C by A3,A16,A18,JORDAN6:def 10;
thus thesis by A4,A6,A17,A18,JORDAN6:def 10;
end;
deffunc F(set) = $1;
set X = {F(p1): P[p1]}, Y = {F(p1): Q[p1]};
A19: X = Y from FRAENKEL:sch 3(A8);
Segment(p,q,C) = X by A6,JORDAN7:def 1;
hence thesis by A19,JORDAN6:26;
end;
theorem Th10:
LE E-max C, q, C implies
Segment(q,W-min C,C) = Segment(Lower_Arc C,E-max C,W-min C,q,W-min C)
proof
set p = W-min C;
assume
A1: LE E-max C, q, C;
A2: Lower_Arc C is_an_arc_of E-max C,W-min C by JORDAN6:50;
A3: p in Lower_Arc C by JORDAN7:1;
A4: q in Lower_Arc C by A1,JORDAN17:4;
A5: Lower_Arc C c= C by JORDAN6:61;
defpred P[Point of TOP-REAL 2] means LE q,$1,C or q in C & $1=W-min C;
defpred Q[Point of TOP-REAL 2] means LE q,$1,Lower_Arc C,E-max C,W-min C &
LE $1,p,Lower_Arc C,E-max C, W-min C;
A6: P[p1] iff Q[p1]
proof
hereby
assume
A7: LE q,p1,C or q in C & p1=W-min C;
per cases by A7;
suppose that
A8: q = E-max C and
A9: LE q,p1,C;
A10: p1 in Lower_Arc C by A8,A9,JORDAN17:4;
hence LE q,p1,Lower_Arc C,E-max C,W-min C by A2,A8,JORDAN5C:10;
thus LE p1,p,Lower_Arc C,E-max C,W-min C by A2,A10,JORDAN5C:10;
end;
suppose that
A11: q <> E-max C and
A12: LE q,p1,C;
A13: p1 in Lower_Arc C by A1,A12,JORDAN17:4,JORDAN6:58;
A14: now
assume
A15: q = W-min C;
then LE q, E-max C, C by JORDAN7:3,SPRECT_1:14;
hence contradiction by A1,A15,JORDAN6:57,TOPREAL5:19;
end;
now
assume q in Upper_Arc C;
then q in Upper_Arc C /\ Lower_Arc C by A4,XBOOLE_0:def 4;
then q in {E-max C, W-min C} by JORDAN6:def 9;
hence contradiction by A11,A14,TARSKI:def 2;
end;
hence LE q,p1,Lower_Arc C,E-max C,W-min C by A12,JORDAN6:def 10;
thus LE p1,p,Lower_Arc C,E-max C,W-min C by A2,A13,JORDAN5C:10;
end;
suppose that q in C and
A16: p1 = W-min C;
thus LE q,p1,Lower_Arc C,E-max C,W-min C by A2,A4,A16,JORDAN5C:10;
thus LE p1,p,Lower_Arc C,E-max C,W-min C by A3,A16,JORDAN5C:9;
end;
end;
assume that
A17: LE q,p1,Lower_Arc C,E-max C,W-min C and
LE p1,p,Lower_Arc C,E-max C,W-min C;
A18: p1 in Lower_Arc C by A17,JORDAN5C:def 3;
A19: q in Lower_Arc C by A17,JORDAN5C:def 3;
per cases;
suppose p1 <> W-min C;
hence thesis by A17,A18,A19,JORDAN6:def 10;
end;
suppose p1 = W-min C;
hence thesis by A4,A5;
end;
end;
deffunc F(set) = $1;
set X = {F(p1): P[p1]}, Y = {F(p1): Q[p1]};
A20: X = Y from FRAENKEL:sch 3(A6);
Segment(q,p,C) = X by JORDAN7:def 1;
hence thesis by A20,JORDAN6:26;
end;
theorem Th11:
LE p,q,C & LE E-max C, p, C implies
Segment(p,q,C) = Segment(Lower_Arc C,E-max C,W-min C,p,q)
proof
assume that
A1: LE p,q,C and
A2: LE E-max C, p, C;
per cases;
suppose p = E-max C;
hence thesis by A1,Th9;
end;
suppose
A3: p <> E-max C;
A4: Lower_Arc C is_an_arc_of E-max C,W-min C by JORDAN6:50;
A5: q in Lower_Arc C by A1,A2,JORDAN17:4,JORDAN6:58;
A6: p in Lower_Arc C by A2,JORDAN17:4;
A7: Lower_Arc C c= C by JORDAN6:61;
A8: now
assume
A9: p = W-min C;
then LE p, E-max C, C by JORDAN17:2;
hence contradiction by A2,A9,JORDAN6:57,TOPREAL5:19;
end;
A10: now
assume
A11: q = W-min C;
then LE q,p,C by A6,A7,JORDAN7:3;
hence contradiction by A1,A8,A11,JORDAN6:57;
end;
defpred P[Point of TOP-REAL 2] means LE p,$1,C & LE $1,q,C;
defpred Q[Point of TOP-REAL 2] means LE p,$1,Lower_Arc C,E-max C,W-min C &
LE $1,q,Lower_Arc C,E-max C,W-min C;
A12: P[p1] iff Q[p1]
proof
hereby
assume that
A13: LE p,p1,C and
A14: LE p1,q,C;
A15: now
assume
A16: p1 = W-min C;
then LE p1,p,C by A6,A7,JORDAN7:3;
hence contradiction by A8,A13,A16,JORDAN6:57;
end;
A17: now
assume
A18: p in Upper_Arc C;
p in Lower_Arc C by A2,JORDAN17:4;
then p in Lower_Arc C /\ Upper_Arc C by A18,XBOOLE_0:def 4;
then p in {W-min C,E-max C} by JORDAN6:50;
hence contradiction by A3,A8,TARSKI:def 2;
end;
hence LE p,p1,Lower_Arc C,E-max C,W-min C by A13,JORDAN6:def 10;
A19: p1 in Lower_Arc C by A13,A17,JORDAN6:def 10;
per cases;
suppose q = E-max C;
hence LE p1,q,Lower_Arc C,E-max C,W-min C by A1,A2,A3,JORDAN6:57;
end;
suppose p1 = E-max C;
hence LE p1,q,Lower_Arc C,E-max C,W-min C by A4,A5,JORDAN5C:10;
end;
suppose that
A20: p1 <> E-max C;
now
assume p1 in Upper_Arc C;
then p1 in Lower_Arc C /\ Upper_Arc C by A19,XBOOLE_0:def 4;
then p1 in {W-min C,E-max C} by JORDAN6:50;
hence contradiction by A15,A20,TARSKI:def 2;
end;
hence LE p1,q,Lower_Arc C,E-max C,W-min C by A14,JORDAN6:def 10;
end;
end;
assume that
A21: LE p,p1,Lower_Arc C,E-max C,W-min C and
A22: LE p1,q,Lower_Arc C,E-max C,W-min C;
A23: p1 <> W-min C by A4,A10,A22,JORDAN6:55;
A24: p1 in Lower_Arc C by A21,JORDAN5C:def 3;
hence LE p,p1,C by A6,A21,A23,JORDAN6:def 10;
thus thesis by A5,A10,A22,A24,JORDAN6:def 10;
end;
deffunc F(set) = $1;
set X = {F(p1): P[p1]}, Y = {F(p1): Q[p1]};
A25: X = Y from FRAENKEL:sch 3(A12);
Segment(p,q,C) = X by A10,JORDAN7:def 1;
hence thesis by A25,JORDAN6:26;
end;
end;
theorem Th12:
LE p,E-max C,C & LE E-max C, q, C implies
Segment(p,q,C) = R_Segment(Upper_Arc C,W-min C,E-max C,p)
\/ L_Segment(Lower_Arc C,E-max C,W-min C,q)
proof
assume that
A1: LE p,E-max C,C and
A2: LE E-max C, q, C;
A3: p in Upper_Arc C by A1,JORDAN17:3;
A4: q in Lower_Arc C by A2,JORDAN17:4;
A5: now
assume q = W-min C;
then W-min C = E-max C by A2,JORDAN7:2;
hence contradiction by TOPREAL5:19;
end;
A6: Lower_Arc C is_an_arc_of E-max C,W-min C by JORDAN6:50;
defpred P[Point of TOP-REAL 2] means LE p,$1,C & LE $1,q,C;
defpred Q1[Point of TOP-REAL 2] means LE p,$1,Upper_Arc C,W-min C,E-max C;
defpred Q2[Point of TOP-REAL 2] means LE $1,q,Lower_Arc C,E-max C,W-min C;
defpred Q[Point of TOP-REAL 2] means Q1[$1] or Q2[$1];
A7: P[p1] iff Q[p1]
proof
thus
LE p,p1,C & LE p1,q,C implies LE p,p1,Upper_Arc C,W-min C,E-max C or
LE p1,q,Lower_Arc C,E-max C,W-min C
proof
assume that
A8: LE p,p1,C and
A9: LE p1,q,C;
A10: now
assume that
A11: p1 in Lower_Arc C and
A12: p1 in Upper_Arc C;
p1 in Lower_Arc C /\ Upper_Arc C by A11,A12,XBOOLE_0:def 4;
then p1 in {W-min C,E-max C} by JORDAN6:def 9;
hence p1 = W-min C or p1 = E-max C by TARSKI:def 2;
end;
per cases by A10;
suppose
A13: p1 = W-min C;
then p = W-min C by A8,JORDAN7:2;
hence thesis by A1,A13,JORDAN17:3,JORDAN5C:9;
end;
suppose p1 = E-max C;
hence thesis by A4,A6,JORDAN5C:10;
end;
suppose not p1 in Lower_Arc C;
hence thesis by A8,JORDAN6:def 10;
end;
suppose not p1 in Upper_Arc C;
hence thesis by A9,JORDAN6:def 10;
end;
end;
assume that
A14: LE p,p1,Upper_Arc C,W-min C,E-max C or
LE p1,q,Lower_Arc C,E-max C,W-min C;
per cases by A14;
suppose
A15: LE p,p1,Upper_Arc C,W-min C,E-max C;
then
A16: p1 in Upper_Arc C by JORDAN5C:def 3;
hence LE p,p1,C by A3,A15,JORDAN6:def 10;
thus thesis by A4,A5,A16,JORDAN6:def 10;
end;
suppose that
A17: LE p1,q,Lower_Arc C,E-max C,W-min C and
A18: p1 <> W-min C;
A19: p1 in Lower_Arc C by A17,JORDAN5C:def 3;
hence LE p,p1,C by A3,A18,JORDAN6:def 10;
thus thesis by A4,A5,A17,A19,JORDAN6:def 10;
end;
suppose LE p1,q,Lower_Arc C,E-max C,W-min C & p1 = W-min C;
hence thesis by A5,A6,JORDAN6:55;
end;
end;
set Y1 = {p1: Q1[p1]}, Y2 = {p1: Q2[p1]};
deffunc F(set) = $1;
set X = {F(p1): P[p1]}, Y = {F(p1): Q[p1]}, Y9 = {p1: Q1[p1] or Q2[p1]};
A20: X = Y from FRAENKEL:sch 3(A7);
A21: Segment(p,q,C) = X by A5,JORDAN7:def 1;
A22: L_Segment(Lower_Arc C,E-max C,W-min C,q) = Y2 by JORDAN6:def 3;
Y9 = Y1 \/ Y2 from TOPREAL1:sch 1;
hence thesis by A20,A21,A22,JORDAN6:def 4;
end;
theorem Th13:
LE p,E-max C,C implies
Segment(p,W-min C,C) = R_Segment(Upper_Arc C,W-min C,E-max C,p)
\/ L_Segment(Lower_Arc C,E-max C,W-min C,W-min C)
proof
set q = W-min C;
assume LE p,E-max C,C;
then
A1: p in Upper_Arc C by JORDAN17:3;
A2: q in Lower_Arc C by JORDAN7:1;
A3: Lower_Arc C is_an_arc_of E-max C,W-min C by JORDAN6:50;
defpred P[Point of TOP-REAL 2] means LE p,$1,C or p in C & $1 = W-min C;
defpred Q1[Point of TOP-REAL 2] means LE p,$1,Upper_Arc C,W-min C,E-max C;
defpred Q2[Point of TOP-REAL 2] means LE $1,q,Lower_Arc C,E-max C,W-min C;
defpred Q[Point of TOP-REAL 2] means Q1[$1] or Q2[$1];
A4: P[p1] iff Q[p1]
proof
thus LE p,p1,C or p in C & p1=W-min C implies
LE p,p1,Upper_Arc C,W-min C,E-max C or LE p1,q,Lower_Arc C,E-max C,W-min C
proof
assume
A5: LE p,p1,C or p in C & p1=W-min C;
A6: now
assume that
A7: p1 in Lower_Arc C and
A8: p1 in Upper_Arc C;
p1 in Lower_Arc C /\ Upper_Arc C by A7,A8,XBOOLE_0:def 4;
then p1 in {W-min C,E-max C} by JORDAN6:def 9;
hence p1 = W-min C or p1 = E-max C by TARSKI:def 2;
end;
per cases by A6;
suppose p1 = W-min C;
hence thesis by A2,JORDAN5C:9;
end;
suppose p1 = E-max C;
hence thesis by A2,A3,JORDAN5C:10;
end;
suppose not p1 in Lower_Arc C & p1 <> W-min C;
hence thesis by A5,JORDAN6:def 10;
end;
suppose that
A9: not p1 in Upper_Arc C and
A10: p1 <> W-min C;
A11: p1 in C by A5,A10,JORDAN7:5;
C = Lower_Arc C \/ Upper_Arc C by JORDAN6:def 9;
then p1 in Lower_Arc C by A9,A11,XBOOLE_0:def 3;
hence thesis by A3,JORDAN5C:10;
end;
end;
assume that
A12: LE p,p1,Upper_Arc C,W-min C,E-max C or
LE p1,q,Lower_Arc C,E-max C,W-min C;
A13: Upper_Arc C c= C by JORDAN6:61;
per cases by A12;
suppose
A14: LE p,p1,Upper_Arc C,W-min C,E-max C;
then p1 in Upper_Arc C by JORDAN5C:def 3;
hence thesis by A1,A14,JORDAN6:def 10;
end;
suppose
LE p1,q,Lower_Arc C,E-max C,W-min C;
then
A15: p1 in Lower_Arc C by JORDAN5C:def 3;
now per cases;
suppose p1 = W-min C;
hence thesis by A1,A13;
end;
suppose p1 <> W-min C;
hence thesis by A1,A15,JORDAN6:def 10;
end;
end;
hence thesis;
end;
end;
set Y1 = {p1: Q1[p1]}, Y2 = {p1: Q2[p1]};
deffunc F(set) = $1;
set X = {F(p1): P[p1]}, Y = {F(p1): Q[p1]}, Y9 = {p1: Q1[p1] or Q2[p1]};
A16: X = Y from FRAENKEL:sch 3(A4);
A17: Segment(p,q,C) = X by JORDAN7:def 1;
A18: L_Segment(Lower_Arc C,E-max C,W-min C,q) = Y2 by JORDAN6:def 3;
Y9 = Y1 \/ Y2 from TOPREAL1:sch 1;
hence thesis by A16,A17,A18,JORDAN6:def 4;
end;
theorem Th14:
R_Segment(Upper_Arc C,W-min C,E-max C,p) =
Segment(Upper_Arc C,W-min C,E-max C,p,E-max C)
proof
Upper_Arc C is_an_arc_of W-min C,E-max C by JORDAN6:50;
then L_Segment(Upper_Arc C,W-min C,E-max C,E-max C) = Upper_Arc C
by JORDAN6:22;
hence Segment(Upper_Arc C,W-min C,E-max C,p,E-max C) =
R_Segment(Upper_Arc C,W-min C,E-max C,p) /\ Upper_Arc C by JORDAN6:def 5
.= R_Segment(Upper_Arc C,W-min C,E-max C,p) by JORDAN6:20,XBOOLE_1:28;
end;
theorem Th15:
L_Segment(Lower_Arc C,E-max C,W-min C,p) =
Segment(Lower_Arc C,E-max C,W-min C,E-max C,p)
proof
Lower_Arc C is_an_arc_of E-max C,W-min C by JORDAN6:50;
then R_Segment(Lower_Arc C,E-max C,W-min C,E-max C) = Lower_Arc C
by JORDAN6:24;
hence Segment(Lower_Arc C,E-max C,W-min C,E-max C,p) =
Lower_Arc C /\ L_Segment(Lower_Arc C,E-max C,W-min C,p) by JORDAN6:def 5
.= L_Segment(Lower_Arc C,E-max C,W-min C,p) by JORDAN6:19,XBOOLE_1:28;
end;
theorem Th16:
for p being Point of TOP-REAL 2 st p in C & p <> W-min C
holds Segment(p,W-min C,C) is_an_arc_of p,W-min C
proof
set q = W-min C;
let p be Point of TOP-REAL 2 such that
A1: p in C and
A2: p <> W-min C;
A3: E-max C in C by SPRECT_1:14;
A4: Upper_Arc C is_an_arc_of W-min C, E-max C by JORDAN6:50;
A5: Lower_Arc C is_an_arc_of E-max C, W-min C by JORDAN6:50;
A6: q <> E-max C by TOPREAL5:19;
per cases by A1,A3,JORDAN16:7;
suppose that
A7: p <> E-max C and
A8: LE p, E-max C, C;
A9: now
assume W-min C in R_Segment(Upper_Arc C,W-min C,E-max C,p)
/\ L_Segment(Lower_Arc C,E-max C,W-min C,q);
then W-min C in R_Segment(Upper_Arc C,W-min C,E-max C,p) by
XBOOLE_0:def 4;
hence contradiction by A2,A4,JORDAN6:60;
end;
p in Upper_Arc C by A8,JORDAN17:3;
then
A10: LE p,E-max C,Upper_Arc C,W-min C,E-max C by A4,JORDAN5C:10;
A11: R_Segment(Upper_Arc C,W-min C,E-max C,p) =
Segment(Upper_Arc C,W-min C,E-max C,p,E-max C) by Th14;
then
A12: E-max C in R_Segment(Upper_Arc C,W-min C,E-max C,p) by A10,JORDAN16:5;
q in Lower_Arc C by JORDAN7:1;
then
A13: LE E-max C,q,Lower_Arc C,E-max C,W-min C by A5,JORDAN5C:10;
A14: L_Segment(Lower_Arc C,E-max C,W-min C,q) =
Segment(Lower_Arc C,E-max C,W-min C,E-max C,q) by Th15;
then E-max C in L_Segment(Lower_Arc C,E-max C,W-min C,q) by A13,JORDAN16:5;
then
A15: E-max C in R_Segment(Upper_Arc C,W-min C,E-max C,p)
/\ L_Segment(Lower_Arc C,E-max C,W-min C,q) by A12,XBOOLE_0:def 4;
A16: R_Segment(Upper_Arc C,W-min C,E-max C,p) c= Upper_Arc C by JORDAN6:20;
A17: L_Segment(Lower_Arc C,E-max C,W-min C,q) c= Lower_Arc C by JORDAN6:19;
Upper_Arc C /\ Lower_Arc C = {W-min C, E-max C} by JORDAN6:def 9;
then
A18: R_Segment(Upper_Arc C,W-min C,E-max C,p)
/\ L_Segment(Lower_Arc C,E-max C,W-min C,q) = {E-max C}
by A9,A15,A16,A17,TOPREAL8:1,XBOOLE_1:27;
A19: R_Segment(Upper_Arc C,W-min C,E-max C,p) is_an_arc_of p, E-max C
by A4,A7,A10,A11,JORDAN16:21;
A20: L_Segment(Lower_Arc C,E-max C,W-min C,q) is_an_arc_of E-max C,q
by A5,A6,A13,A14,JORDAN16:21;
Segment(p,W-min C,C) = R_Segment(Upper_Arc C,W-min C,E-max C,p)
\/ L_Segment(Lower_Arc C,E-max C,W-min C,W-min C) by A8,Th13;
hence thesis by A18,A19,A20,TOPREAL1:2;
end;
suppose
A21: p = E-max C;
then Segment(p,q,C) = Lower_Arc C by JORDAN7:4;
hence thesis by A21,JORDAN6:50;
end;
suppose that p <> E-max C and
A22: LE E-max C,p, C;
A23: Segment(p,q,C) = Segment(Lower_Arc C,E-max C,W-min C,p,q) by A22,Th10;
p in Lower_Arc C by A22,JORDAN17:4;
then LE p, q, Lower_Arc C, E-max C, W-min C by A5,JORDAN5C:10;
hence thesis by A2,A5,A23,JORDAN16:21;
end;
end;
theorem Th17:
for p,q being Point of TOP-REAL 2 st p<> q & LE p,q,C
holds Segment(p,q,C) is_an_arc_of p,q
proof
let p,q be Point of TOP-REAL 2 such that
A1: p <> q and
A2: LE p,q,C;
A3: E-max C in C by SPRECT_1:14;
A4: p in C by A2,JORDAN7:5;
A5: q in C by A2,JORDAN7:5;
A6: Upper_Arc C is_an_arc_of W-min C, E-max C by JORDAN6:50;
A7: Lower_Arc C is_an_arc_of E-max C, W-min C by JORDAN6:50;
per cases by A3,A4,A5,JORDAN16:7;
suppose q = W-min C;
hence thesis by A1,A4,Th16;
end;
suppose that
A8: LE q, E-max C, C and
A9: not LE E-max C, q, C and
A10: q <> W-min C;
A11: Segment(p,q,C) = Segment(Upper_Arc C,W-min C,E-max C,p,q) by A1,A2,A8,Th8;
not q in Lower_Arc C by A9,A10,Th5;
then LE p, q, Upper_Arc C, W-min C, E-max C by A2,JORDAN6:def 10;
hence thesis by A1,A6,A11,JORDAN16:21;
end;
suppose that
A12: p <> E-max C and
A13: LE p, E-max C, C and
A14: LE E-max C,q, C and
A15: q <> E-max C;
A16: now
assume
A17: W-min C in R_Segment(Upper_Arc C,W-min C,E-max C,p)
/\ L_Segment(Lower_Arc C,E-max C,W-min C,q);
then W-min C in R_Segment(Upper_Arc C,W-min C,E-max C,p) by
XBOOLE_0:def 4;
then
A18: p = W-min C by A6,JORDAN6:60;
W-min C in L_Segment(Lower_Arc C,E-max C,W-min C,q) by A17,XBOOLE_0:def 4;
hence contradiction by A1,A7,A18,JORDAN6:59;
end;
p in Upper_Arc C by A13,JORDAN17:3;
then
A19: LE p,E-max C,Upper_Arc C,W-min C,E-max C by A6,JORDAN5C:10;
A20: R_Segment(Upper_Arc C,W-min C,E-max C,p) =
Segment(Upper_Arc C,W-min C,E-max C,p,E-max C) by Th14;
then
A21: E-max C in R_Segment(Upper_Arc C,W-min C,E-max C,p) by A19,JORDAN16:5;
q in Lower_Arc C by A14,JORDAN17:4;
then
A22: LE E-max C,q,Lower_Arc C,E-max C,W-min C by A7,JORDAN5C:10;
A23: L_Segment(Lower_Arc C,E-max C,W-min C,q) =
Segment(Lower_Arc C,E-max C,W-min C,E-max C,q) by Th15;
then E-max C in L_Segment(Lower_Arc C,E-max C,W-min C,q) by A22,JORDAN16:5;
then
A24: E-max C in R_Segment(Upper_Arc C,W-min C,E-max C,p)
/\ L_Segment(Lower_Arc C,E-max C,W-min C,q) by A21,XBOOLE_0:def 4;
A25: R_Segment(Upper_Arc C,W-min C,E-max C,p) c= Upper_Arc C by JORDAN6:20;
A26: L_Segment(Lower_Arc C,E-max C,W-min C,q) c= Lower_Arc C by JORDAN6:19;
Upper_Arc C /\ Lower_Arc C = {W-min C, E-max C} by JORDAN6:def 9;
then
A27: R_Segment(Upper_Arc C,W-min C,E-max C,p)
/\ L_Segment(Lower_Arc C,E-max C,W-min C,q) = {E-max C}
by A16,A24,A25,A26,TOPREAL8:1,XBOOLE_1:27;
A28: R_Segment(Upper_Arc C,W-min C,E-max C,p) is_an_arc_of p, E-max C
by A6,A12,A19,A20,JORDAN16:21;
A29: L_Segment(Lower_Arc C,E-max C,W-min C,q) is_an_arc_of E-max C,q
by A7,A15,A22,A23,JORDAN16:21;
Segment(p,q,C) = R_Segment(Upper_Arc C,W-min C,E-max C,p)
\/ L_Segment(Lower_Arc C,E-max C,W-min C,q) by A13,A14,Th12;
hence thesis by A27,A28,A29,TOPREAL1:2;
end;
suppose that
A30: q = E-max C and
A31: LE p, E-max C, C and
A32: LE E-max C,q, C;
p in Upper_Arc C by A31,JORDAN17:3;
then
A33: LE p,E-max C,Upper_Arc C,W-min C,E-max C by A6,JORDAN5C:10;
A34: R_Segment(Upper_Arc C,W-min C,E-max C,p) =
Segment(Upper_Arc C,W-min C,E-max C,p,E-max C) by Th14;
then
A35: E-max C in R_Segment(Upper_Arc C,W-min C,E-max C,p) by A33,JORDAN16:5;
A36: L_Segment(Lower_Arc C,E-max C,W-min C,q) = {E-max C} by A7,A30,JORDAN6:21;
Segment(p,q,C) = R_Segment(Upper_Arc C,W-min C,E-max C,p)
\/ L_Segment(Lower_Arc C,E-max C,W-min C,q) by A31,A32,Th12
.= R_Segment(Upper_Arc C,W-min C,E-max C,p) by A35,A36,ZFMISC_1:40;
hence thesis by A1,A6,A30,A33,A34,JORDAN16:21;
end;
suppose that
A37: p = E-max C and
A38: LE p, E-max C, C and
A39: LE E-max C,q, C;
q in Lower_Arc C by A39,JORDAN17:4;
then
A40: LE E-max C,q,Lower_Arc C,E-max C,W-min C by A7,JORDAN5C:10;
A41: L_Segment(Lower_Arc C,E-max C,W-min C,q) =
Segment(Lower_Arc C,E-max C,W-min C,E-max C,q) by Th15;
then
A42: E-max C in L_Segment(Lower_Arc C,E-max C,W-min C,q) by A40,JORDAN16:5;
A43: R_Segment(Upper_Arc C,W-min C,E-max C,p) = {E-max C} by A6,A37,JORDAN6:23;
Segment(p,q,C) = R_Segment(Upper_Arc C,W-min C,E-max C,p)
\/ L_Segment(Lower_Arc C,E-max C,W-min C,q) by A38,A39,Th12
.= L_Segment(Lower_Arc C,E-max C,W-min C,q) by A42,A43,ZFMISC_1:40;
hence thesis by A1,A7,A37,A40,A41,JORDAN16:21;
end;
suppose that
A44: LE E-max C,p, C and
A45: not LE p, E-max C, C;
A46: Segment(p,q,C) = Segment(Lower_Arc C,E-max C,W-min C,p,q) by A2,A44,Th11;
not p in Upper_Arc C by A45,Th6;
then LE p, q, Lower_Arc C, E-max C, W-min C by A2,JORDAN6:def 10;
hence thesis by A1,A7,A46,JORDAN16:21;
end;
end;
theorem Th18: :: poprawic JORDAN7:7
C = Segment(W-min C,W-min C,C)
proof
set X = {p: LE W-min C,p,C or W-min C in C & p=W-min C};
A1: Segment(W-min C,W-min C,C) = X by JORDAN7:def 1;
thus C c= Segment(W-min C,W-min C,C)
proof
let e be object;
assume
A2: e in C;
then reconsider p = e as Point of TOP-REAL 2;
LE W-min C,p,C by A2,JORDAN7:3;
hence thesis by A1;
end;
thus thesis by JORDAN16:6;
end;
theorem Th19:
for q being Point of TOP-REAL 2 st q in C
holds Segment(q,W-min C,C) is compact
proof
let q be Point of TOP-REAL 2 such that
A1: q in C;
per cases;
suppose q = W-min C;
hence thesis by Th18;
end;
suppose q <> W-min C;
hence thesis by A1,Th16,JORDAN5A:1;
end;
end;
theorem Th20:
for q1,q2 being Point of TOP-REAL 2 st LE q1,q2,C
holds Segment(q1,q2,C) is compact
proof
let q1,q2 be Point of TOP-REAL 2 such that
A1: LE q1,q2,C;
A2: q1 in C by A1,JORDAN7:5;
per cases;
suppose q2 = W-min C;
hence thesis by A2,Th19;
end;
suppose q1 = q2 & q2 <> W-min C;
then Segment(q1,q2,C) = {q1} by A2,JORDAN7:8;
hence thesis;
end;
suppose q1 <> q2 & q2 <> W-min C;
hence thesis by A1,Th17,JORDAN5A:1;
end;
end;
begin :: The concept of a segmentation
definition
let C;
mode Segmentation of C -> FinSequence of TOP-REAL 2 means
:Def3:
it/.1=W-min C & it is one-to-one & 8<=len it & rng it c= C &
(for i being Nat st 1<=i & i<len it holds LE it/.i,it/.(i+1),C) &
(for i being Nat st 1<=i & i+1<len it holds
Segment(it/.i,it/.(i+1),C) /\ Segment(it/.(i+1),it/.(i+2),C)={it/.(i+1)}) &
Segment(it/.len it,it/.1,C) /\ Segment(it/.1,it/.2,C)={it/.1} &
Segment(it/.(len it-' 1),it/.len it,C)/\ Segment(it/.len it,it/.1,C)
={it/.len it} &
Segment(it/.(len it-'1),it/.len it,C) misses Segment(it/.1,it/.2,C) &
(for i,j being Nat st 1<=i & i < j & j < len it &
i,j aren't_adjacent
holds Segment(it/.i,it/.(i+1),C) misses Segment(it/.j,it/.(j+1),C)) &
for i being Nat st 1 < i & i+1 < len it holds
Segment(it/.len it,it/.1,C) misses Segment(it/.i,it/.(i+1),C);
existence
proof
consider h being FinSequence of the carrier of TOP-REAL 2 such that
A1: h.1=W-min C and
A2: h is one-to-one and
A3: 8<=len h and
A4: rng h c= C and
A5: for i being Nat st 1<=i & i<len h holds LE h/.i,h/.(i+1),C and
for i being Nat,W being Subset of Euclid 2 st 1<=i & i<len h
& W=Segment(h/.i,h/.(i+1),C) holds diameter(W)<1
and for W being Subset of Euclid 2 st W=Segment(h/.len h,h/.1,C) holds
diameter(W)<1 and
A6: for i being Nat st 1<=i & i+1<len h holds
Segment(h/.i,h/.(i+1),C)/\ Segment(h/.(i+1),h/.(i+2),C)={h/.(i+1)} and
A7: Segment(h/.len h,h/.1,C)/\ Segment(h/.1,h/.2,C)={h/.1} and
A8: Segment(h/.(len h-' 1),h/.len h,C)/\ Segment(h/.len h,h/.1,C)={h/.len h}
and
A9: Segment(h/.(len h-'1),h/.len h,C) misses Segment(h/.1,h/.2,C) and
A10: for i,j being Nat st 1<=i & i < j & j < len h &
i,j aren't_adjacent
holds Segment(h/.i,h/.(i+1),C) misses Segment(h/.j,h/.(j+1),C) and
A11: for i being Nat st 1 < i & i+1 < len h holds
Segment(h/.len h,h/.1,C) misses Segment(h/.i,h/.(i+1),C) by JORDAN7:20;
reconsider h as non empty FinSequence of the carrier of TOP-REAL 2
by A3,CARD_1:27;
take h;
1 in dom h by FINSEQ_5:6;
hence h/.1=W-min C by A1,PARTFUN1:def 6;
thus h is one-to-one by A2;
thus 8<=len h by A3;
thus rng h c= C by A4;
thus
for i being Nat st 1<=i & i<len h holds LE h/.i,h/.(i+1),C
by A5;
thus for i being Nat st 1<=i & i+1<len h holds
Segment(h/.i,h/.(i+1),C) /\ Segment(h/.(i+1),h/.(i+2),C)={h/.(i+1)} by A6;
thus Segment(h/.len h,h/.1,C) /\ Segment(h/.1,h/.2,C)={h/.1} by A7;
thus Segment(h/.(len h-' 1),h/.len h,C)/\ Segment(h/.len h,h/.1,C)
={h/.len h} by A8;
thus
Segment(h/.(len h-'1),h/.len h,C) misses Segment(h/.1,h/.2,C) by A9;
thus for i,j being Nat
st 1<=i & i < j & j < len h & i,j aren't_adjacent
holds Segment(h/.i,h/.(i+1),C) misses Segment(h/.j,h/.(j+1),C) by A10;
thus thesis by A11;
end;
end;
registration
let C;
cluster -> non trivial for Segmentation of C;
coherence
proof
let S be Segmentation of C;
len S >= 8 by Def3;
then len S >= 2 by XXREAL_0:2;
hence thesis by NAT_D:60;
end;
end;
theorem Th21:
for S being Segmentation of C, i st 1<=i & i <= len S holds S/.i in C
proof
let S be Segmentation of C, i;
assume that
A1: 1<=i and
A2: i <= len S;
i in dom S by A1,A2,FINSEQ_3:25;
then
A3: S/.i in rng S by PARTFUN2:2;
rng S c= C by Def3;
hence thesis by A3;
end;
begin :: The segments of a segmentation
definition
let C;
let i be Nat;
let S be Segmentation of C;
func Segm(S,i) -> Subset of TOP-REAL 2 equals
:Def4:
Segment(S/.i,S/.(i+1),C) if 1<=i & i<len S
otherwise Segment(S/.len S,S/.1,C);
correctness;
end;
theorem
for S being Segmentation of C st i in dom S holds Segm(S,i) c= C
proof
let S be Segmentation of C;
assume i in dom S;
then
A1: 1 <= i by FINSEQ_3:25;
i < len S or i >= len S;
then Segm(S,i) = Segment(S/.i,S/.(i+1),C) or
Segm(S,i) = Segment(S/.len S,S/.1,C) by A1,Def4;
hence thesis by JORDAN16:6;
end;
registration
let C;
let S be Segmentation of C, i;
cluster Segm(S,i) -> non empty compact;
coherence
proof
per cases;
suppose
A1: 1<=i & i<len S;
then
A2: Segm(S,i) = Segment(S/.i,S/.(i+1),C) by Def4;
LE S/.i,S/.(i+1),C by A1,Def3;
hence thesis by A2,Th20,JORDAN7:6;
end;
suppose not(1<=i & i<len S);
then
A3: Segm(S,i) = Segment(S/.len S,S/.1,C) by Def4;
8 <= len S by Def3;
then 1 <= len S by XXREAL_0:2;
then
A4: S/.len S in C by Th21;
S/.1 = W-min C by Def3;
hence thesis by A3,A4,Th19,JORDAN16:19;
end;
end;
end;
theorem
for S being Segmentation of C, p st p in C
ex i being Nat st i in dom S & p in Segm(S,i)
proof
let S be Segmentation of C, p such that
A1: p in C;
set X = { i : i in dom S & LE S/.i, p, C };
A2: X c= dom S
proof
let e be object;
assume e in X;
then ex i st e = i & i in dom S & LE S/.i, p, C;
hence thesis;
end;
A3: 1 in dom S by FINSEQ_5:6;
A4: W-min C = S/.1 by Def3;
then LE S/.1, p, C by A1,JORDAN7:3;
then 1 in X by A3;
then reconsider X as finite non empty Subset of NAT by A2,XBOOLE_1:1;
reconsider mX = max X as Nat by TARSKI:1;
take mX;
A5: max X in X by XXREAL_2:def 8;
hence mX in dom S by A2;
A6: 1 <= max X by A2,A5,FINSEQ_3:25;
A7: max X <= len S by A2,A5,FINSEQ_3:25;
A8: ex i st max X = i & i in dom S & LE S/.i, p, C by A5;
per cases by A7,XXREAL_0:1;
suppose
A9: max X < len S;
A10: 1 <= max X + 1 by NAT_1:11;
max X +1 <= len S by A9,NAT_1:13;
then
A11: mX + 1 in dom S by A10,FINSEQ_3:25;
A12: S is one-to-one by Def3;
max X +1 >= 1+1 by A6,XREAL_1:6;
then max X + 1 <> 1;
then
A13: S/.(max X+1) <> S/.1 by A3,A11,A12,PARTFUN2:10;
A14: S/.(max X+1) in rng S by A11,PARTFUN2:2;
A15: rng S c= C by Def3;
now
assume LE S/.(max X+1),p,C;
then max X +1 in X by A11;
then max X +1 <= max X by XXREAL_2:def 8;
hence contradiction by XREAL_1:29;
end;
then LE p,S/.(max X+1),C by A1,A14,A15,JORDAN16:7;
then p in {p1: LE S/.(max X),p1,C & LE p1,S/.(max X+1),C} by A8;
then p in Segment(S/.max X,S/.(max X+1),C) by A4,A13,JORDAN7:def 1;
hence thesis by A6,A9,Def4;
end;
suppose
A16: max X = len S;
now per cases;
case p<>W-min C;
thus LE S/.len S,p,C by A8,A16;
end;
case p=W-min C;
A17: S/.len S in rng S by FINSEQ_6:168;
rng S c= C by Def3;
hence S/.len S in C by A17;
end;
end;
then p in {p1: LE S/.len S,p1,C or S/.len S in C & p1=W-min C};
then p in Segment(S/.len S,S/.1,C) by A4,JORDAN7:def 1;
hence thesis by A16,Def4;
end;
end;
theorem Th24:
for S being Segmentation of C
for i,j st 1<=i & i< j & j<len S & i,j aren't_adjacent
holds Segm(S,i) misses Segm(S,j)
proof
let S be Segmentation of C;
let i,j such that
A1: 1<=i and
A2: i < j and
A3: j<len S and
A4: i,j aren't_adjacent;
i < len S by A2,A3,XXREAL_0:2;
then
A5: Segm(S,i) = Segment(S/.i,S/.(i+1),C) by A1,Def4;
1 < j by A1,A2,XXREAL_0:2;
then Segm(S,j) = Segment(S/.j,S/.(j+1),C) by A3,Def4;
hence thesis by A1,A2,A3,A4,A5,Def3;
end;
theorem Th25:
for S being Segmentation of C for j st 1<j & j<len S -' 1
holds Segm(S,len S) misses Segm(S,j)
proof
let S be Segmentation of C;
let j such that
A1: 1<j and
A2: j<len S -' 1;
A3: Segm(S,len S) = Segment(S/.len S,S/.1,C) by Def4;
A4: j+1 < len S by A2,NAT_D:53;
j < len S by A2,NAT_D:44;
then Segm(S,j) = Segment(S/.j,S/.(j+1),C) by A1,Def4;
hence thesis by A1,A3,A4,Def3;
end;
theorem Th26:
for S being Segmentation of C
for i,j st 1<=i & i< j & j<len S & i,j are_adjacent
holds Segm(S,i) /\ Segm(S,j)={S/.(i+1)}
proof
let S be Segmentation of C;
let i,j such that
A1: 1<=i and
A2: i< j and
A3: j<len S and
A4: i,j are_adjacent;
i < len S by A2,A3,XXREAL_0:2;
then
A5: Segm(S,i) = Segment(S/.i,S/.(i+1),C) by A1,Def4;
1 < j by A1,A2,XXREAL_0:2;
then
A6: Segm(S,j) = Segment(S/.j,S/.(j+1),C) by A3,Def4;
j+1 > i by A2,NAT_1:13;
then j = i+1 by A4,GOBRD10:def 1;
then j+1 = i+(1+1);
hence thesis by A1,A3,A5,A6,Def3;
end;
theorem Th27:
for S being Segmentation of C
for i,j st 1<=i & i< j & j<len S & i,j are_adjacent
holds Segm(S,i) meets Segm(S,j)
proof
let S be Segmentation of C;
let i,j;
assume that
A1: 1<=i and
A2: i< j and
A3: j<len S and
A4: i,j are_adjacent;
Segm(S,i) /\ Segm(S,j)={S/.(i+1)} by A1,A2,A3,A4,Th26;
hence thesis;
end;
theorem Th28:
for S being Segmentation of C holds Segm(S,len S) /\ Segm(S,1) = {S/.1}
proof
let S be Segmentation of C;
A1: Segm(S,len S) = Segment(S/.len S,S/.1,C) by Def4;
len S >= 8 by Def3;
then 1 < len S by XXREAL_0:2;
then Segm(S,1) = Segment(S/.1,S/.(1+1),C) by Def4;
hence thesis by A1,Def3;
end;
theorem Th29:
for S being Segmentation of C holds Segm(S,len S) meets Segm(S,1)
proof
let S be Segmentation of C;
Segm(S,len S) /\ Segm(S,1) = {S/.1} by Th28;
hence thesis;
end;
theorem Th30:
for S being Segmentation of C
holds Segm(S,len S) /\ Segm(S,len S -' 1) = {S/.len S}
proof
let S be Segmentation of C;
A1: Segm(S,len S) = Segment(S/.len S,S/.1,C) by Def4;
A2: len S >= 8 by Def3;
then len S >= 1+1 by XXREAL_0:2;
then
A3: 1 <= len S -' 1 by NAT_D:55;
A4: len S -' 1 + 1 = len S by A2,XREAL_1:235,XXREAL_0:2;
then len S -' 1 < len S by NAT_1:13;
then Segm(S,len S -' 1) = Segment(S/.(len S -' 1),S/.len S,C) by A3,A4,Def4;
hence thesis by A1,Def3;
end;
theorem Th31:
for S being Segmentation of C holds Segm(S,len S) meets Segm(S,len S -' 1)
proof
let S be Segmentation of C;
Segm(S,len S) /\ Segm(S,len S -' 1) = {S/.len S} by Th30;
hence thesis;
end;
begin :: The diameter of a segmentation
definition
let n;
let C be Subset of TOP-REAL n;
func diameter C -> Real means
:Def5:
ex W being Subset of Euclid n st W = C & it = diameter W;
existence
proof
the TopStruct of TOP-REAL n =TopSpaceMetr Euclid n by EUCLID:def 8
.= TopStruct (#the carrier of Euclid n,Family_open_set Euclid n #)
by PCOMPS_1:def 5;
then reconsider W = C as Subset of Euclid n;
take diameter W, W;
thus thesis;
end;
correctness;
end;
definition
let C;
let S be Segmentation of C;
func diameter S -> Real means
:Def6:
ex S1 being non empty finite Subset of REAL st
S1 = { diameter Segm(S,i) where i is Element of NAT: i in dom S} &
it = max S1;
existence
proof
deffunc F(Nat) = In(diameter Segm(S,$1),REAL);
defpred P[set] means $1 in dom S;
set S1 = { F(i) where i is Element of NAT: P[i]};
set S2 = { F(i) where i is Element of NAT: i in dom S};
A1: dom S is finite;
A2: S2 is finite from FRAENKEL:sch 21(A1);
A3: S1 is Subset of REAL from DOMAIN_1:sch 8;
1 in dom S by FINSEQ_5:6;
then F(1) in S1;
then reconsider S1 as non empty finite Subset of REAL by A2,A3;
reconsider mS1 = max S1 as Real;
take mS1, S1;
deffunc G(Nat) = diameter Segm(S,$1);
A4: for i being Element of NAT holds F(i) = G(i);
{ F(i) where i is Element of NAT: P[i]}
= { G(j) where j is Element of NAT: P[j]}
from FRAENKEL:sch 5(A4);
hence thesis;
end;
correctness;
end;
theorem
for S being Segmentation of C, i holds diameter Segm(S,i) <= diameter S
proof
let S be Segmentation of C, i;
consider S1 be non empty finite Subset of REAL such that
A1: S1 = { diameter Segm(S,j) where j is Element of NAT: j in dom S} and
A2: diameter S = max S1 by Def6;
per cases;
suppose 1 <= i & i < len S;
then i in dom S by FINSEQ_3:25;
then diameter Segm(S,i) in S1 by A1;
hence thesis by A2,XXREAL_2:def 8;
end;
suppose
A3: not(1 <= i & i < len S);
A4: Segm(S,len S) = Segment(S/.len S,S/.1,C) by Def4
.= Segm(S,i) by A3,Def4;
len S in dom S by FINSEQ_5:6;
then diameter Segm(S,i) in S1 by A1,A4;
hence thesis by A2,XXREAL_2:def 8;
end;
end;
theorem Th33:
for S being Segmentation of C, e being Real
st for i holds diameter Segm(S,i) < e holds diameter S < e
proof
let S be Segmentation of C, e be Real such that
A1: for i holds diameter Segm(S,i) < e;
consider S1 being non empty finite Subset of REAL such that
A2: S1 = { diameter Segm(S,i) where i is Element of NAT: i in dom S} and
A3: diameter S = max S1 by Def6;
diameter S in S1 by A3,XXREAL_2:def 8;
then ex i being Element of NAT
st diameter S = diameter Segm(S,i) & i in dom S by A2;
hence thesis by A1;
end;
theorem
for e being Real st e > 0 ex S being Segmentation of C st diameter S < e
proof
let e be Real;
assume e > 0;
then consider h being FinSequence of the carrier of TOP-REAL 2 such that
A1: h.1=W-min C and
A2: h is one-to-one and
A3: 8<=len h and
A4: rng h c= C and
A5: for i being Nat st 1<=i & i<len h holds LE h/.i,h/.(i+1),C and
A6: for i being Nat,W being Subset of Euclid 2
st 1<=i & i<len h & W=Segment(h/.i,h/.(i+1),C) holds diameter(W)<e and
A7: for W being Subset of Euclid 2 st
W=Segment(h/.len h,h/.1,C) holds diameter(W)<e and
A8: for i being Nat st 1<=i & i+1<len h holds
Segment(h/.i,h/.(i+1),C)/\ Segment(h/.(i+1),h/.(i+2),C)={h/.(i+1)} and
A9: Segment(h/.len h,h/.1,C)/\ Segment(h/.1,h/.2,C)={h/.1} and
A10: Segment(h/.(len h-' 1),h/.len h,C)/\ Segment(h/.len h,h/.1,C)={h/.len h}
and
A11: Segment(h/.(len h-'1),h/.len h,C) misses Segment(h/.1,h/.2,C) and
A12: for i,j being Nat st 1<=i & i < j & j < len h &
i,j aren't_adjacent
holds Segment(h/.i,h/.(i+1),C) misses Segment(h/.j,h/.(j+1),C) and
A13: for i being Nat st 1 < i & i+1 < len h holds
Segment(h/.len h,h/.1,C) misses Segment(h/.i,h/.(i+1),C) by JORDAN7:20;
h <> {} by A3,CARD_1:27;
then 1 in dom h by FINSEQ_5:6;
then h/.1 = W-min C by A1,PARTFUN1:def 6;
then reconsider h as Segmentation of C
by A2,A3,A4,A5,A8,A9,A10,A11,A12,A13,Def3;
take h;
diameter Segm(h,i) < e
proof
A14: ex W being Subset of Euclid 2 st ( W = Segm(h,i))&(
diameter Segm(h,i) = diameter W) by Def5;
per cases;
suppose
A15: 1<=i & i<len h;
then Segm(h,i) = Segment(h/.i,h/.(i+1),C) by Def4;
hence thesis by A6,A14,A15;
end;
suppose not(1<=i & i<len h);
then Segm(h,i) = Segment(h/.len h,h/.1,C) by Def4;
hence thesis by A7,A14;
end;
end;
hence thesis by Th33;
end;
begin :: The concept of the gap of a segmentation
definition
let C;
let S be Segmentation of C;
func S-Gap S -> Real means
:Def7:
ex S1,S2 being non empty finite Subset of REAL st
S1 = { dist_min(Segm(S,i),Segm(S,j)) where i,j is Element of NAT:
1<=i & i< j & j<len S & i,j aren't_adjacent} &
S2 = { dist_min(Segm(S,len S),Segm(S,k)) where k is Element of NAT:
1<k & k<len S -' 1 } &
it = min(min S1,min S2);
existence
proof
deffunc F(Nat) = dist_min(Segm(S,len S),Segm(S,$1));
deffunc F(Nat,Nat) = dist_min(Segm(S,$1),Segm(S,$2));
defpred P[Nat] means 1<$1 & $1<len S -' 1;
defpred Q[Nat] means $1 in dom S;
defpred R[Nat,Nat] means
1<=$1 & $1< $2 & $2<len S & $1,$2 aren't_adjacent;
defpred W[Nat,Nat] means Q[$1] & Q[$2];
set S1 = { F(i,j) where i,j is Element of NAT: R[i,j] };
set S2 = { F(j) where j is Element of NAT: P[j] };
set B = { F(i,j) where i,j is Element of NAT : W[i,j] };
set B9 = { F(i,j) where i,j is Element of NAT: i in dom S & j in dom S };
set A = { F(j) where j is Element of NAT: Q[j] };
set A9 = { F(j) where j is Element of NAT: j in dom S };
A1: for j being Element of NAT st P[j] holds Q[j]
proof let j be Element of NAT;
assume
A2: 1<j;
A3: len S -' 1 <= len S by NAT_D:35;
assume j<len S -' 1;
then j < len S by A3,XXREAL_0:2;
hence thesis by A2,FINSEQ_3:25;
end;
A4: S2 c= A from FRAENKEL:sch 1(A1);
A5: for i, j being Element of NAT holds R[i,j] implies W[i,j]
proof
let i,j be Element of NAT such that
A6: 1<=i and
A7: i< j and
A8: j<len S and i,j aren't_adjacent;
i < len S by A7,A8,XXREAL_0:2;
hence i in dom S by A6,FINSEQ_3:25;
1 < j by A6,A7,XXREAL_0:2;
hence thesis by A8,FINSEQ_3:25;
end;
A9: S1 c= B from FRAENKEL:sch 2(A5);
A10: S1 c= REAL
proof
let x be object;
assume x in S1;
then ex i,j being Element of NAT st x = dist_min(Segm(S,i),Segm(S,j)) &
1<=i & i<j & j<len S & i,j aren't_adjacent;
hence thesis by XREAL_0:def 1;
end;
A11: S2 c= REAL
proof
let x be object;
assume x in S2;
then ex j being Element of NAT
st x = dist_min(Segm(S,len S),Segm(S,j)) & 1<j & j<len S -' 1;
hence thesis by XREAL_0:def 1;
end;
A12: dom S is finite;
A13: A9 is finite from FRAENKEL:sch 21(A12);
A14: B9 is finite from FRAENKEL:sch 22(A12,A12);
A15: 3 <> 1+1;
1 <> 3+1;
then
A16: 1,3 aren't_adjacent by A15,GOBRD10:def 1;
A17: len S >= 7+1 by Def3;
then 3<len S by XXREAL_0:2;
then
A18: dist_min(Segm(S,1),Segm(S,3)) in S1 by A16;
2+1 < len S by A17,XXREAL_0:2;
then 2<len S -' 1 by NAT_D:52;
then dist_min(Segm(S,len S),Segm(S,2)) in S2;
then reconsider S1, S2 as non empty finite Subset of REAL
by A4,A9,A10,A11,A13,A14,A18;
reconsider mm = min(min S1,min S2) as Element of REAL by XREAL_0:def 1;
take mm,S1,S2;
thus thesis;
end;
correctness;
end;
theorem Th35:
for S being Segmentation of C ex F being finite non empty Subset of REAL st
F = { dist_min(Segm(S,i),Segm(S,j)):
1<=i & i<j & j<=len S & Segm(S,i) misses Segm(S,j)} & S-Gap S = min F
proof
let S be Segmentation of C;
consider S1,S2 being non empty finite Subset of REAL such that
A1: S1 = { dist_min(Segm(S,i),Segm(S,j)) where i,j is Element of NAT:
1<=i & i< j & j<len S & i,j aren't_adjacent} and
A2: S2 = { dist_min(Segm(S,len S),Segm(S,k)) where k is Element of NAT:
1<k & k<len S -' 1 } and
A3: S-Gap S = min(min S1,min S2) by Def7;
take F = S1 \/ S2;
set X = { dist_min(Segm(S,i),Segm(S,j)):
1<=i & i<j & j<=len S & Segm(S,i) misses Segm(S,j)};
thus F c= X
proof
let e be object;
assume
A4: e in F;
per cases by A4,XBOOLE_0:def 3;
suppose e in S1;
then consider i,j being Element of NAT such that
A5: e = dist_min(Segm(S,i),Segm(S,j)) and
A6: 1<=i and
A7: i< j and
A8: j<len S and
A9: i,j aren't_adjacent by A1;
Segm(S,i) misses Segm(S,j) by A6,A7,A8,A9,Th24;
hence thesis by A5,A6,A7,A8;
end;
suppose e in S2;
then consider j being Element of NAT such that
A10: e = dist_min(Segm(S,len S),Segm(S,j)) and
A11: 1<j and
A12: j<len S -' 1 by A2;
A13: j < len S by A12,NAT_D:44;
Segm(S,len S) misses Segm(S,j) by A11,A12,Th25;
hence thesis by A10,A11,A13;
end;
end;
thus X c= F
proof
let e be object;
assume e in X;
then consider i,j such that
A14: e = dist_min(Segm(S,i),Segm(S,j)) and
A15: 1<=i and
A16: i<j and
A17: j<=len S and
A18: Segm(S,i) misses Segm(S,j);
A19: i < len S by A16,A17,XXREAL_0:2;
A20: i in NAT & j in NAT by ORDINAL1:def 12;
per cases by A17,XXREAL_0:1;
suppose that
A21: j < len S;
i,j aren't_adjacent by A15,A16,A18,A21,Th27;
then e in S1 by A1,A14,A15,A16,A21,A20;
hence thesis by XBOOLE_0:def 3;
end;
suppose
A22: j = len S;
then 1 <> i by A18,Th29;
then
A23: 1 < i by A15,XXREAL_0:1;
A24: i <= len S -' 1 by A19,NAT_D:49;
i <> len S -' 1 by A18,A22,Th31;
then i < len S -' 1 by A24,XXREAL_0:1;
then e in S2 by A2,A14,A22,A23,A20;
hence thesis by XBOOLE_0:def 3;
end;
end;
thus thesis by A3,XXREAL_2:9;
end;
theorem
for S being Segmentation of C holds S-Gap S > 0
proof
let S be Segmentation of C;
consider F being finite non empty Subset of REAL such that
A1: F = { dist_min(Segm(S,i),Segm(S,j)):
1<=i & i<j & j<=len S & Segm(S,i) misses Segm(S,j)} and
A2: S-Gap S = min F by Th35;
S-Gap S in F by A2,XXREAL_2:def 7;
then ex i,j st S-Gap S = dist_min(Segm(S,i),Segm(S,j)) &
1<=i & i<j & j<=len S & Segm(S,i) misses Segm(S,j) by A1;
hence thesis by Th7;
end;