:: On the Segmentation of a Simple Closed Curve
:: by Andrzej Trybulec
::
:: Received August 18, 2003
:: Copyright (c) 2003-2018 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~~ 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
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 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 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;
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= 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 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= 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 {} 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 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 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 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~~