Copyright (c) 1999 Association of Mizar Users
environ
vocabulary SEQM_3, GOBOARD5, SPRECT_2, PRE_TOPC, EUCLID, COMPTS_1, SPPOL_1,
GOBOARD1, METRIC_1, CONNSP_1, RELAT_2, RELAT_1, JORDAN2C, SUBSET_1,
LATTICES, BOOLE, TOPREAL1, TARSKI, COMPLEX1, ABSVALUE, SETFAM_1, ARYTM_1,
FINSEQ_1, SQUARE_1, MCART_1, TREES_1, CARD_3, FUNCOP_1, RCOMP_1, FUNCT_1,
MATRIX_1, JORDAN8, GROUP_1, ARYTM_3, PSCOMP_1, INT_1, POWER, GOBOARD9,
GOBOARD2, TOPS_1, JORDAN1, FINSEQ_6, SPRECT_1, ORDINAL2, FUNCT_5, SEQ_2,
FINSEQ_4, ARYTM;
notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_1, FUNCT_1, FUNCT_2,
BINOP_1, ORDINAL1, XCMPLX_0, XREAL_0, REAL_1, SQUARE_1, NAT_1, ABSVALUE,
INT_1, POWER, MATRIX_1, BINARITH, FUNCT_4, SEQ_4, STRUCT_0, GROUP_1,
METRIC_1, LIMFUNC1, TBSP_1, FINSEQ_1, CARD_3, CARD_4, FINSEQ_4, FINSEQ_6,
RCOMP_1, PRE_TOPC, TOPS_1, TOPS_2, CONNSP_1, COMPTS_1, EUCLID, TOPREAL1,
GOBOARD1, GOBOARD2, GOBOARD5, GOBOARD9, PSCOMP_1, SPPOL_1, JGRAPH_1,
SPRECT_1, SPRECT_2, JORDAN2C, JORDAN8;
constructors BINARITH, CARD_4, COMPTS_1, CONNSP_1, FINSEQ_4, GOBOARD2,
GOBOARD9, JORDAN1, JORDAN2C, JORDAN8, LIMFUNC1, POWER, PSCOMP_1, RCOMP_1,
REAL_1, REALSET1, SPPOL_1, SPRECT_1, SPRECT_2, TBSP_1, TOPGRP_1,
TOPREAL2, TOPREAL4, TOPS_1, TOPS_2, WAYBEL_3, TOPRNS_1, MEMBERED,
PARTFUN1;
clusters SUBSET_1, XREAL_0, EUCLID, GOBOARD2, GOBRD11, PRE_TOPC, PSCOMP_1,
RELSET_1, SPRECT_1, SPRECT_3, TOPREAL6, TOPS_1, REVROT_1, INT_1,
JORDAN2C, MEMBERED, FUNCT_2, SEQM_3, RELAT_1, ZFMISC_1;
requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM;
definitions TARSKI, TOPS_2, JORDAN2C, SPRECT_1, XBOOLE_0;
theorems ABSVALUE, AXIOMS, BINARITH, CARD_3, FUNCT_4, COMPTS_1, CONNSP_1,
CQC_THE1, EUCLID, FINSEQ_1, FINSEQ_3, FUNCT_1, FUNCT_2, GOBOARD5,
GOBOARD6, GOBOARD7, GOBOARD9, GOBRD11, GOBRD12, HEINE, INT_1, JGRAPH_1,
JORDAN1, JORDAN2C, JORDAN3, JORDAN8, METRIC_1, NAT_1, POWER, PRE_TOPC,
PRE_FF, PSCOMP_1, RCOMP_1, REAL_1, REAL_2, RELAT_1, RLVECT_1, SEQ_4,
SPRECT_1, SPRECT_3, SPRECT_4, SQUARE_1, SPPOL_2, SUBSET_1, TARSKI,
TBSP_1, TDLAT_1, TOPREAL1, TOPREAL3, TOPREAL6, TOPS_1, TOPS_2, SPRECT_2,
REVROT_1, FINSEQ_6, TOPREAL5, AMI_5, SETFAM_1, XBOOLE_0, XBOOLE_1,
XREAL_0, XCMPLX_0, XCMPLX_1;
begin :: Components
reserve i, j, n for Nat,
f for non constant standard special_circular_sequence,
g for clockwise_oriented
non constant standard special_circular_sequence,
p, q for Point of TOP-REAL 2,
P, Q, R for Subset of TOP-REAL 2,
C for compact non vertical non horizontal Subset of TOP-REAL 2,
G for Go-board;
Lm1: Euclid 2 = MetrStruct(#REAL 2,Pitag_dist 2#) by EUCLID:def 7;
theorem
for T being TopSpace,
A being Subset of T, B being Subset of T
st B is_a_component_of A holds B is connected
proof
let T be TopSpace,
A be Subset of T,
B be Subset of T;
assume B is_a_component_of A;
then consider C being Subset of T|A such that
A1: C = B and
A2: C is_a_component_of T|A by CONNSP_1:def 6;
C is connected by A2,CONNSP_1:def 5;
hence thesis by A1,CONNSP_1:24;
end;
theorem
for A being Subset of TOP-REAL n, B being Subset of TOP-REAL
n
st B is_inside_component_of A holds B is connected
proof
let A be Subset of TOP-REAL n,
B be Subset of TOP-REAL n;
assume B is_inside_component_of A;
then consider C being Subset of (TOP-REAL n)|A` such that
A1: C = B and
A2: C is_a_component_of (TOP-REAL n)|A` and
C is bounded Subset of Euclid n by JORDAN2C:17;
C is connected by A2,CONNSP_1:def 5;
hence thesis by A1,CONNSP_1:24;
end;
theorem Th3:
for A being Subset of TOP-REAL n, B being Subset of TOP-REAL n
st B is_outside_component_of A holds B is connected
proof
let A be Subset of TOP-REAL n,
B be Subset of TOP-REAL n;
assume B is_outside_component_of A;
then consider C being Subset of (TOP-REAL n)|A` such that
A1: C = B and
A2: C is_a_component_of (TOP-REAL n)|A` and
not C is bounded Subset of Euclid n by JORDAN2C:18;
C is connected by A2,CONNSP_1:def 5;
hence thesis by A1,CONNSP_1:24;
end;
theorem
for A being Subset of TOP-REAL n, B being Subset of TOP-REAL
n
st B is_a_component_of A` holds A misses B
proof
let A be Subset of TOP-REAL n,
B be Subset of TOP-REAL n;
assume B is_a_component_of A`;
then B c= A` by SPRECT_1:7;
then A misses B by SUBSET_1:43;
hence A /\ B = {} by XBOOLE_0:def 7;
end;
theorem
P is_outside_component_of Q & R is_inside_component_of Q implies P misses R
proof
assume P is_outside_component_of Q;
then A1: P c= UBD Q by JORDAN2C:27;
assume R is_inside_component_of Q;
then A2: R c= BDD Q by JORDAN2C:26;
(BDD Q) misses (UBD Q) by JORDAN2C:28;
then P misses BDD Q by A1,XBOOLE_1:63;
hence thesis by A2,XBOOLE_1:63;
end;
theorem Th6:
for A, B being Subset of TOP-REAL 2 st
A is_outside_component_of L~f & B is_outside_component_of L~f holds
A = B
proof
let A, B be Subset of TOP-REAL 2 such that
A1: A is_outside_component_of L~f &
B is_outside_component_of L~f;
L~f is Bounded by JORDAN2C:73;
then consider C being Subset of TOP-REAL 2 such that
A2: C is_outside_component_of L~f and
A3: C = UBD L~f by JORDAN2C:76;
A4: A is_a_component_of (L~f)` & B is_a_component_of (L~f)`
by A1,JORDAN2C:def 4;
then A5: A <> {} & B <> {} by SPRECT_1:6;
A6: C is_a_component_of (L~f)` by A2,JORDAN2C:def 4;
A c= UBD L~f & B c= UBD L~f by A1,JORDAN2C:27;
then A meets C & B meets C by A3,A5,XBOOLE_1:69;
then A = C & B = C by A4,A6,GOBOARD9:3;
hence thesis;
end;
theorem
for p being Point of Euclid 2 st p = 0.REAL 2 & P is_outside_component_of L~
f
ex r being Real st r > 0 & Ball(p,r)` c= P
proof
let p be Point of Euclid 2 such that
A1: p = 0.REAL 2 and
A2: P is_outside_component_of L~f;
A3: L~f is Bounded by JORDAN2C:73;
then consider D being Subset of Euclid 2 such that
A4: D = L~f and
A5: D is bounded by JORDAN2C:def 2;
consider r being Real, c being Point of Euclid 2 such that
A6: 0 < r and c in D and
A7: for z being Point of Euclid 2 st z in D holds dist(c,z) <= r
by A4,A5,TBSP_1:15;
set rr = dist(p,c)+r+1;
A8: D c= Ball(p,rr)
proof
let x be set; assume
A9: x in D;
then reconsider z = x as Point of Euclid 2;
dist(c,z) <= r by A7,A9;
then A10: dist(p,c) + dist(c,z) <= dist(p,c) + r by REAL_1:55;
dist(p,z) <= dist(p,c) + dist(c,z) by METRIC_1:4;
then A11: dist(p,z) <= dist(p,c) + r by A10,AXIOMS:22;
dist(p,c) + r + 0 < dist(p,c) + r + 1 by REAL_1:53;
then dist(p,z) < dist(p,c) + r + 1 by A11,AXIOMS:22;
hence x in Ball(p,rr) by METRIC_1:12;
end;
take rr;
A12: 0 <= dist(p,c) by METRIC_1:5;
dist(p,c)+r+0 < rr by REAL_1:67;
hence
A13: 0 < rr by A6,A12,REAL_1:67;
let x be set; assume
A14: x in Ball(p,rr)`;
then reconsider y = x as Point of Euclid 2;
reconsider z = y as Point of TOP-REAL 2 by TOPREAL3:13;
consider B being Subset of TOP-REAL 2 such that
A15: B is_outside_component_of L~f and
A16: B = UBD L~f by A3,JORDAN2C:76;
A17: UBD L~f = union{W where W is Subset of TOP-REAL 2:
W is_outside_component_of L~f} by JORDAN2C:def 6;
A18: P = B by A2,A15,Th6;
set L = (REAL 2) \ {a where a is Point of TOP-REAL 2: |.a.| < rr};
A19: the carrier of TOP-REAL 2 = REAL 2 by EUCLID:25;
A20: L c= REAL 2
proof
let l be set;
assume l in L;
hence l in REAL 2 by XBOOLE_0:def 4;
end;
rr = abs rr by A13,ABSVALUE:def 1;
then for a being Point of TOP-REAL 2 holds a <> |[0,rr]| or |.a.| >= rr
by TOPREAL6:31;
then not |[0,rr]| in {a where a is Point of TOP-REAL 2: |.a.| < rr};
then reconsider L as non empty Subset of TOP-REAL 2
by A19,A20,XBOOLE_0:def 4;
A21: z in REAL 2 by A19;
A22: not x in Ball(p,rr) by A14,SUBSET_1:54;
dist(p,y) = |.z.| by A1,TOPREAL6:33;
then for k being Point of TOP-REAL 2 holds k <> z or |.k.| >= rr
by A22,METRIC_1:12;
then not x in {a where a is Point of TOP-REAL 2: |.a.| < rr};
then A23: x in L by A21,XBOOLE_0:def 4;
A24: L is connected by JORDAN2C:61;
L c= (L~f)`
proof
let l be set; assume
A25: l in L;
then A26: not l in {a where a is Point of TOP-REAL 2: |.a.| < rr} by XBOOLE_0
:def 4;
reconsider j = l as Point of TOP-REAL 2 by A25;
reconsider t = j as Point of Euclid 2 by TOPREAL3:13;
A27: |.j.| >= rr by A26;
now
assume l in L~f;
then dist(t,p) < rr by A4,A8,METRIC_1:12;
hence contradiction by A1,A27,TOPREAL6:33;
end;
hence l in (L~f)` by A25,SUBSET_1:50;
end;
then consider M being Subset of TOP-REAL 2 such that
A28: M is_a_component_of (L~f)` and
A29: L c= M by A24,GOBOARD9:5;
M is_outside_component_of L~f
proof
thus M is_a_component_of (L~f)` by A28;
not L is Bounded
proof
thus for C being Subset of Euclid 2 holds
C <> L or not C is bounded by JORDAN2C:70;
end;
hence not M is Bounded by A29,JORDAN2C:16;
end;
then M in {W where W is Subset of TOP-REAL 2: W is_outside_component_of L~
f};
hence x in P by A16,A17,A18,A23,A29,TARSKI:def 4;
end;
definition let C be closed Subset of TOP-REAL 2;
cluster BDD C -> open;
coherence
proof
set F = {B where B is Subset of TOP-REAL 2: B is_inside_component_of C};
F c= bool the carrier of TOP-REAL 2
proof
let f be set;
assume f in F;
then ex B being Subset of TOP-REAL 2 st f = B & B is_inside_component_of
C;
hence thesis;
end;
then F is Subset-Family of TOP-REAL 2 by SETFAM_1:def 7;
then reconsider F as Subset-Family of TOP-REAL 2;
A1: BDD C = union F by JORDAN2C:def 5;
F is open
proof
let P be Subset of TOP-REAL 2;
assume P in F;
then consider B being Subset of TOP-REAL 2 such that
A2: P = B and
A3: B is_inside_component_of C;
B is_a_component_of C` by A3,JORDAN2C:def 3;
then B is_a_component_of C`;
hence P is open by A2,SPRECT_3:18;
end;
hence thesis by A1,TOPS_2:26;
end;
cluster UBD C -> open;
coherence
proof
set F = {B where B is Subset of TOP-REAL 2: B is_outside_component_of C};
F c= bool the carrier of TOP-REAL 2
proof
let f be set;
assume f in F;
then ex B being Subset of TOP-REAL 2 st f = B & B
is_outside_component_of C;
hence thesis;
end;
then F is Subset-Family of TOP-REAL 2 by SETFAM_1:def 7;
then reconsider F as Subset-Family of TOP-REAL 2;
A4: UBD C = union F by JORDAN2C:def 6;
F is open
proof
let P be Subset of TOP-REAL 2;
assume P in F;
then consider B being Subset of TOP-REAL 2 such that
A5: P = B and
A6: B is_outside_component_of C;
B is_a_component_of C` by A6,JORDAN2C:def 4;
then B is_a_component_of C`;
hence P is open by A5,SPRECT_3:18;
end;
hence thesis by A4,TOPS_2:26;
end;
end;
definition let C be compact Subset of TOP-REAL 2;
cluster UBD C -> connected;
coherence
proof
C is Bounded by JORDAN2C:73;
then ex B being Subset of TOP-REAL 2 st B is_outside_component_of C &
B = UBD C by JORDAN2C:76;
hence thesis by Th3;
end;
end;
begin :: Go-boards
theorem :: TOPREAL1:29
for f being FinSequence of TOP-REAL n st L~f <> {} holds 2 <= len f
proof
let f be FinSequence of TOP-REAL n;
assume L~f <> {};
then len f <> 0 & len f <> 1 by TOPREAL1:28;
then len f > 1 by CQC_THE1:2;
then len f >= 1 + 1 by NAT_1:38;
hence thesis;
end;
definition let n be Nat, a, b be Point of TOP-REAL n;
func dist(a,b) -> Real means :Def1:
ex p, q being Point of Euclid n st p = a & q = b & it = dist(p,q);
existence
proof
reconsider p = a, q = b as Point of Euclid n by TOPREAL3:13;
take dist(p,q);
thus thesis;
end;
uniqueness;
commutativity;
end;
theorem Th9:
dist(p,q) = sqrt ((p`1-q`1)^2 + (p`2-q`2)^2)
proof
A1: ex a, b being Point of Euclid 2 st p = a & q = b & dist(a,b) = dist(p,q)
by Def1;
p = |[p`1, p`2]| & q = |[q`1, q`2]| by EUCLID:57;
hence thesis by A1,GOBOARD6:9;
end;
theorem Th10:
for p being Point of TOP-REAL n holds dist(p,p) = 0
proof
let p be Point of TOP-REAL n;
ex a, b being Point of Euclid n st a = p & b = p & dist(a,b) = dist(p,p)
by Def1;
hence thesis by METRIC_1:1;
end;
theorem
for p, q, r being Point of TOP-REAL n holds
dist(p,r) <= dist (p,q) + dist(q,r)
proof
let p, q, r be Point of TOP-REAL n;
(ex a, b being Point of Euclid n st a = p & b = q & dist(a,b) = dist(p,q)
)
&
(ex a, b being Point of Euclid n st a = p & b = r & dist(a,b) = dist(p,r))
&
ex a, b being Point of Euclid n st a = q & b = r & dist(a,b) = dist(q,r)
by Def1;
hence thesis by METRIC_1:4;
end;
theorem
for x1, x2, y1, y2 being real number,
a, b being Point of TOP-REAL 2 st
x1 <= a`1 & a`1 <= x2 & y1 <= a`2 & a`2 <= y2 &
x1 <= b`1 & b`1 <= x2 & y1 <= b`2 & b`2 <= y2 holds
dist(a,b) <= (x2-x1) + (y2-y1)
proof
let x1, x2, y1, y2 be real number,
a, b be Point of TOP-REAL 2 such that
A1: x1 <= a`1 & a`1 <= x2 & y1 <= a`2 & a`2 <= y2 &
x1 <= b`1 & b`1 <= x2 & y1 <= b`2 & b`2 <= y2;
A2: dist(a,b) = sqrt ((a`1-b`1)^2 + (a`2-b`2)^2) by Th9;
x1 is Real & x2 is Real & y1 is Real & y2 is Real by XREAL_0:def 1;
then abs(a`1-b`1) <= x2 - x1 & abs(a`2-b`2) <= y2 - y1 by A1,JGRAPH_1:31;
then A3: abs(a`1-b`1) + abs(a`2-b`2) <= (x2 - x1) + (y2 - y1) by REAL_1:55;
(a`1-b`1)^2 >= 0 & (a`2-b`2)^2 >= 0 by SQUARE_1:72;
then dist(a,b) <= sqrt(a`1-b`1)^2 + sqrt(a`2-b`2)^2 by A2,TOPREAL6:6;
then dist(a,b) <= abs(a`1-b`1) + sqrt(a`2-b`2)^2 by SQUARE_1:91;
then dist(a,b) <= abs(a`1-b`1) + abs(a`2-b`2) by SQUARE_1:91;
hence thesis by A3,AXIOMS:22;
end;
theorem Th13:
1 <= i & i < len G & 1 <= j & j < width G implies
cell(G,i,j) =
product ((1,2) --> ([.G*(i,1)`1,G*(i+1,1)`1.],[.G*(1,j)`2,G*(1,j+1)`2.]))
proof
assume 1 <= i & i < len G & 1 <= j & j < width G;
then A1: cell(G,i,j) = { |[r,s]| where r, s is Real:
G*(i,1)`1 <= r & r <= G*(i+1,1)`1 &
G*(1,j)`2 <= s & s <= G*(1,j+1)`2 } by GOBRD11:32;
A2: [.G*(i,1)`1,G*(i+1,1)`1.] = {a where a is Real :
G*(i,1)`1 <= a & a <= G*(i+1,1)`1 } &
[.G*(1,j)`2,G*(1,j+1)`2.] = {b where b is Real :
G*(1,j)`2 <= b & b <= G*(1,j+1)`2 }
by RCOMP_1:def 1;
set f = (1,2) --> ([.G*(i,1)`1,G*(i+1,1)`1.],[.G*(1,j)`2,G*(1,j+1)`2.]);
A3: dom f = {1,2} by FUNCT_4:65;
thus cell(G,i,j) c= product f
proof
let c be set;
assume c in cell(G,i,j);
then consider r, s being Real such that
A4: c = |[r,s]| and
A5: G*(i,1)`1 <= r & r <= G*(i+1,1)`1 &
G*(1,j)`2 <= s & s <= G*(1,j+1)`2 by A1;
A6: r in [.G*(i,1)`1,G*(i+1,1)`1.] & s in [.G*(1,j)`2,G*(1,j+1)`2.] by A2,A5;
A7: dom <*r,s*> = {1,2} by FINSEQ_1:4,FINSEQ_3:29;
A8: <*r,s*> = c by A4,EUCLID:def 16;
for x being set st x in dom f holds <*r,s*>.x in f.x
proof
let x be set;
assume x in dom f;
then A9: x = 1 or x = 2 by A3,TARSKI:def 2;
A10: |[r,s]| = <*r,s*> by EUCLID:def 16;
A11: r = |[r,s]|`1 by EUCLID:56
.= <*r,s*>.1 by A10,EUCLID:def 14;
s = |[r,s]|`2 by EUCLID:56
.= <*r,s*>.2 by A10,EUCLID:def 15;
hence thesis by A6,A9,A11,FUNCT_4:66;
end;
hence thesis by A3,A7,A8,CARD_3:18;
end;
let c be set;
assume c in product f;
then consider g being Function such that
A12: c = g and
A13: dom g = dom f and
A14: for x being set st x in dom f holds g.x in f.x by CARD_3:def 5;
1 in dom f & 2 in dom f by A3,TARSKI:def 2;
then A15: g.1 in f.1 & g.2 in f.2 by A14;
then g.1 in [.G*(i,1)`1,G*(i+1,1)`1.] by FUNCT_4:66;
then consider a being Real such that
A16: g.1 = a and
A17: G*(i,1)`1 <= a & a <= G*(i+1,1)`1 by A2;
g.2 in [.G*(1,j)`2,G*(1,j+1)`2.] by A15,FUNCT_4:66;
then consider b being Real such that
A18: g.2 = b and
A19: G*(1,j)`2 <= b & b <= G*(1,j+1)`2 by A2;
A20: dom <*a,b*> = {1,2} by FINSEQ_1:4,FINSEQ_3:29;
A21: dom g = {1,2} by A13,FUNCT_4:65;
for k being set st k in dom g holds g.k = <*a,b*>.k
proof
let k be set;
assume k in dom g;
then k = 1 or k = 2 by A21,TARSKI:def 2;
hence thesis by A16,A18,FINSEQ_1:61;
end;
then g = <*a,b*> by A20,A21,FUNCT_1:9;
then c = |[a,b]| by A12,EUCLID:def 16;
hence thesis by A1,A17,A19;
end;
theorem
1 <= i & i < len G & 1 <= j & j < width G implies cell(G,i,j) is compact
proof
assume 1 <= i & i < len G & 1 <= j & j < width G;
then cell(G,i,j) = product ((1,2) --> ([.G*(i,1)`1,G*(i+1,1)`1.],
[.G*(1,j)`2,G*(1,j+1)`2.])) by Th13;
hence thesis by TOPREAL6:87;
end;
theorem
[i,j] in Indices G & [i+n,j] in Indices G implies
dist(G*(i,j),G*(i+n,j)) = G*(i+n,j)`1 - G*(i,j)`1
proof
assume
A1: [i,j] in Indices G & [i+n,j] in Indices G;
set x = G*(i,j),
y = G*(i+n,j);
per cases;
suppose
A2: n = 0;
hence dist(G*(i,j),G*(i+n,j)) = 0 by Th10
.= G*(i+n,j)`1 - G*(i,j)`1 by A2,XCMPLX_1:14;
suppose
A3: n <> 0;
A4: 1 <= i+n & i+n <= len G by A1,GOBOARD5:1;
A5: 1 <= j & j <= width G & 1 <= i & i <= len G by A1,GOBOARD5:1;
then A6: x`2 = G*(1,j)`2 by GOBOARD5:2
.= y`2 by A4,A5,GOBOARD5:2;
1 <= n by A3,RLVECT_1:99;
then i < i+n by RLVECT_1:103;
then x`1 < y`1 by A4,A5,GOBOARD5:4;
then x`1 - x`1 < y`1 - x`1 by REAL_1:92;
then A7: 0 < y`1 - x`1 by XCMPLX_1:14;
thus dist(G*(i,j),G*(i+n,j))
= sqrt ((x`1-y`1)^2 + (x`2-y`2)^2) by Th9
.= sqrt ((x`1-y`1)^2 + 0) by A6,SQUARE_1:60,XCMPLX_1:14
.= abs(x`1-y`1) by SQUARE_1:91
.= abs(-(x`1-y`1)) by ABSVALUE:17
.= abs(y`1-x`1) by XCMPLX_1:143
.= G*(i+n,j)`1 - G*(i,j)`1 by A7,ABSVALUE:def 1;
end;
theorem
[i,j] in Indices G & [i,j+n] in Indices G implies
dist(G*(i,j),G*(i,j+n)) = G*(i,j+n)`2 - G*(i,j)`2
proof
assume
A1: [i,j] in Indices G & [i,j+n] in Indices G;
set x = G*(i,j),
y = G*(i,j+n);
per cases;
suppose
A2: n = 0;
hence dist(G*(i,j),G*(i,j+n)) = 0 by Th10
.= G*(i,j+n)`2 - G*(i,j)`2 by A2,XCMPLX_1:14;
suppose
A3: n <> 0;
A4: 1 <= j+n & j+n <= width G by A1,GOBOARD5:1;
A5: 1 <= j & j <= width G & 1 <= i & i <= len G by A1,GOBOARD5:1;
then A6: x`1 = G*(i,1)`1 by GOBOARD5:3
.= y`1 by A4,A5,GOBOARD5:3;
1 <= n by A3,RLVECT_1:99;
then j < j+n by RLVECT_1:103;
then x`2 < y`2 by A4,A5,GOBOARD5:5;
then x`2 - x`2 < y`2 - x`2 by REAL_1:92;
then A7: 0 < y`2 - x`2 by XCMPLX_1:14;
thus dist(G*(i,j),G*(i,j+n))
= sqrt ((x`1-y`1)^2 + (x`2-y`2)^2) by Th9
.= sqrt (0 + (x`2-y`2)^2) by A6,SQUARE_1:60,XCMPLX_1:14
.= abs(x`2-y`2) by SQUARE_1:91
.= abs(-(x`2-y`2)) by ABSVALUE:17
.= abs(y`2-x`2) by XCMPLX_1:143
.= G*(i,j+n)`2 - G*(i,j)`2 by A7,ABSVALUE:def 1;
end;
theorem
3 <= len Gauge(C,n)-'1
proof
set G = Gauge(C,n);
4 <= len G by JORDAN8:13;
then A1: 4 - 1 <= len G-1 by REAL_1:92;
then 0 <= len G - 1 by AXIOMS:22;
hence thesis by A1,BINARITH:def 3;
end;
theorem
i <= j implies
for a, b being Nat st 2 <= a & a <= len Gauge(C,i) - 1 &
2 <= b & b <= len Gauge(C,i) - 1
ex c, d being Nat st 2 <= c & c <= len Gauge(C,j) - 1 &
2 <= d & d <= len Gauge(C,j) - 1 &
[c,d] in Indices Gauge(C,j) & Gauge(C,i)*(a,b) = Gauge(C,j)*(c,d) &
c = 2 + 2|^(j-'i)*(a-'2) & d = 2 + 2|^(j-'i)*(b-'2)
proof
assume
A1: i <= j;
let a, b be Nat such that
A2: 2 <= a and
A3: a <= len Gauge(C,i) - 1 and
A4: 2 <= b and
A5: b <= len Gauge(C,i) - 1;
set c = 2 + 2|^(j-'i)*(a-'2),
d = 2 + 2|^(j-'i)*(b-'2);
take c, d;
2|^i + 2 - 2 = 2|^i + (2 - 2) by XCMPLX_1:29
.= 2|^i + 0;
then A6: 2|^i + 2 - 2 >= 0 by NAT_1:18;
A7: 0 <= 2|^(j-'i) by NAT_1:18;
A8: 0 <> 2|^i by HEINE:5;
A9: 0 <> 2|^j by HEINE:5;
A10: len Gauge(C,i) - 1 = 2|^i + 3 - 1 by JORDAN8:def 1
.= 2|^i + (3 - 1) by XCMPLX_1:29
.= 2|^i + 2;
A11: 2|^i + 2 -' 2 = 2|^i + 2 - 2 by A6,BINARITH:def 3
.= 2|^i + (2 - 2) by XCMPLX_1:29
.= 2|^i + 0;
A12: 2|^(j-'i)*(2|^i) = 2|^j / 2|^i*(2|^i) by A1,TOPREAL6:15
.= 2|^j by A8,XCMPLX_1:88;
a -' 2 <= 2|^i + 2 -' 2 by A3,A10,JORDAN3:5;
then A13: 2|^(j-'i)*(a-'2) <= 2|^j by A7,A11,A12,AXIOMS:25;
b -' 2 <= 2|^i + 2 -' 2 by A5,A10,JORDAN3:5;
then A14: 2|^(j-'i)*(b-'2) <= 2|^j by A7,A11,A12,AXIOMS:25;
A15: len Gauge(C,j) - 1 = 2|^j + 3 - 1 by JORDAN8:def 1
.= 2|^j + (3 - 1) by XCMPLX_1:29
.= 2|^j + 2;
0 <= 2|^(j-'i)*(a-'2) & 0 <= 2|^(j-'i)*(b-'2) by NAT_1:18;
then 2+0 <= 2+2|^(j-'i)*(a-'2) & 2+0 <= 2+2|^(j-'i)*(b-'2) by AXIOMS:24;
hence
A16: 2 <= c & c <= len Gauge(C,j) - 1 & 2 <= d & d <= len Gauge(C,j) - 1
by A13,A14,A15,AXIOMS:24;
A17: width Gauge(C,j) = len Gauge(C,j) by JORDAN8:def 1;
len Gauge(C,j) - 1 < len Gauge(C,j) - 0 by REAL_1:92;
then 1 <= c & c <= len Gauge(C,j) & 1 <= d & d <= width Gauge(C,j)
by A16,A17,AXIOMS:22;
hence
A18: [c,d] in Indices Gauge(C,j) by GOBOARD7:10;
A19: width Gauge(C,i) = len Gauge(C,i) by JORDAN8:def 1;
set n = N-bound C, e = E-bound C, s = S-bound C, w = W-bound C;
len Gauge(C,i) - 1 < len Gauge(C,i) - 0 by REAL_1:92;
then 1 <= a & a <= len Gauge(C,i) & 1 <= b & b <= width Gauge(C,i)
by A2,A3,A4,A5,A19,AXIOMS:22;
then [a,b] in Indices Gauge(C,i) by GOBOARD7:10;
then A20: Gauge(C,i)*(a,b) = |[w+(e-w)/(2|^i)*(a-2), s+(n-s)/(2|^i)*(b-2)]|
by JORDAN8:def 1;
A21: Gauge(C,j)*(c,d) = |[w+(e-w)/(2|^j)*(c-2), s+(n-s)/(2|^j)*(d-2)]|
by A18,JORDAN8:def 1;
A22: 0 <= a-2 by A2,SQUARE_1:12;
A23: 0 <= b-2 by A4,SQUARE_1:12;
A24: (e-w)/(2|^j)*(c-2)
= (e-w)/(2|^j)*(2 - 2 + 2|^(j-'i)*(a-'2)) by XCMPLX_1:29
.= (e-w)/(2|^j)*((2|^j/2|^i)*(a-'2)) by A1,TOPREAL6:15
.= (e-w)/(2|^j)*(2|^j/2|^i)*(a-'2) by XCMPLX_1:4
.= (e-w)/((2|^j)/(2|^j/2|^i))*(a-'2) by XCMPLX_1:82
.= (e-w)/(2|^i)*(a-'2) by A9,XCMPLX_1:52
.= (e-w)/(2|^i)*(a-2) by A22,BINARITH:def 3;
A25: (n-s)/(2|^j)*(d-2)
= (n-s)/(2|^j)*(2 - 2 + 2|^(j-'i)*(b-'2)) by XCMPLX_1:29
.= (n-s)/(2|^j)*((2|^j/2|^i)*(b-'2)) by A1,TOPREAL6:15
.= (n-s)/(2|^j)*(2|^j/2|^i)*(b-'2) by XCMPLX_1:4
.= (n-s)/((2|^j)/(2|^j/2|^i))*(b-'2) by XCMPLX_1:82
.= (n-s)/(2|^i)*(b-'2) by A9,XCMPLX_1:52
.= (n-s)/(2|^i)*(b-2) by A23,BINARITH:def 3;
A26: Gauge(C,i)*(a,b)`1 = w+(e-w)/(2|^i)*(a-2) by A20,EUCLID:56
.= Gauge(C,j)*(c,d)`1 by A21,A24,EUCLID:56;
Gauge(C,i)*(a,b)`2 = s+(n-s)/(2|^i)*(b-2) by A20,EUCLID:56
.= Gauge(C,j)*(c,d)`2 by A21,A25,EUCLID:56;
hence Gauge(C,i)*(a,b) = Gauge(C,j)*(c,d) by A26,TOPREAL3:11;
thus thesis;
end;
theorem Th19:
[i,j] in Indices Gauge(C,n) & [i,j+1] in Indices Gauge(C,n) implies
dist(Gauge(C,n)*(i,j),Gauge(C,n)*(i,j+1)) = (N-bound C - S-bound C)/2|^n
proof
set G = Gauge(C,n),
a = N-bound C, e = E-bound C, s = S-bound C, w = W-bound C,
p1 = G*(i,j),
p2 = G*(i,j+1);
assume that
A1: [i,j] in Indices G and
A2: [i,j+1] in Indices G;
consider p, q being Point of Euclid 2 such that
A3: p = p1 & q = p2 and
A4: dist(p1,p2) = dist(p,q) by Def1;
A5: p1 = |[w+(e-w)/(2|^n)*(i-2), s+(a-s)/(2|^n)*(j-2)]| by A1,JORDAN8:def 1;
A6: p2 = |[w+(e-w)/(2|^n)*(i-2), s+(a-s)/(2|^n)*(j+1-2)]| by A2,JORDAN8:def 1;
set x = (a-s)/(2|^n);
A7: 2|^n > 0 by HEINE:5;
a >= s by SPRECT_1:24;
then a - s >= s - s by REAL_1:49;
then A8: a - s >= 0 by XCMPLX_1:14;
dist(p,q) = (Pitag_dist 2).(p,q) by Lm1,METRIC_1:def 1
.= sqrt ((p1`1 - p2`1)^2 + (p1`2 - p2`2)^2) by A3,TOPREAL3:12
.= sqrt ((w+(e-w)/(2|^n)*(i-2) - p2`1)^2 + (p1`2 - p2`2)^2)
by A5,EUCLID:56
.= sqrt ((w+(e-w)/(2|^n)*(i-2) - (w+(e-w)/(2|^n)*(i-2)))^2 +
(p1`2 - p2`2)^2) by A6,EUCLID:56
.= sqrt (0 + (p1`2 - p2`2)^2) by SQUARE_1:60,XCMPLX_1:14
.= abs(p1`2 - p2`2) by SQUARE_1:91
.= abs(s+x*(j-2) - p2`2) by A5,EUCLID:56
.= abs(s+x*(j-2) - (s+x*(j+1-2))) by A6,EUCLID:56
.= abs(s+x*(j-2) - s - x*(j+1-2)) by XCMPLX_1:36
.= abs(s-s+x*(j-2) - x*(j+1-2)) by XCMPLX_1:29
.= abs(0+x*(j-2) - x*(j+1-2)) by XCMPLX_1:14
.= abs(x*j-x*2 - x*(j+1-2)) by XCMPLX_1:40
.= abs(x*j-x*2 - (x*j+x*1-x*2)) by XCMPLX_1:43
.= abs(x*j-x*2 - (x*j+x*1) + x*2) by XCMPLX_1:37
.= abs(x*j-x*2 - x*j-x*1 + x*2) by XCMPLX_1:36
.= abs(x*j-(x*2 + x*j)-x + x*2) by XCMPLX_1:36
.= abs(x*j-x*j - x*2-x + x*2) by XCMPLX_1:36
.= abs(0 - x*2-x + x*2) by XCMPLX_1:14
.= abs(-x*2-x + x*2) by XCMPLX_1:150
.= abs(-x*2 + x*2 - x) by XCMPLX_1:29
.= abs(0 - x) by XCMPLX_0:def 6
.= abs(-x) by XCMPLX_1:150
.= abs(x) by ABSVALUE:17
.= abs(a-s)/abs(2|^n) by ABSVALUE:16
.= (a-s)/abs(2|^n) by A8,ABSVALUE:def 1;
hence thesis by A4,A7,ABSVALUE:def 1;
end;
theorem Th20:
[i,j] in Indices Gauge(C,n) & [i+1,j] in Indices Gauge(C,n) implies
dist(Gauge(C,n)*(i,j),Gauge(C,n)*(i+1,j)) = (E-bound C - W-bound C)/2|^n
proof
set G = Gauge(C,n),
a = N-bound C, e = E-bound C, s = S-bound C, w = W-bound C,
p1 = G*(i,j),
p2 = G*(i+1,j);
assume that
A1: [i,j] in Indices G and
A2: [i+1,j] in Indices G;
consider p, q being Point of Euclid 2 such that
A3: p = p1 & q = p2 and
A4: dist(p1,p2) = dist(p,q) by Def1;
A5: p1 = |[w+(e-w)/(2|^n)*(i-2), s+(a-s)/(2|^n)*(j-2)]| by A1,JORDAN8:def 1;
A6: p2 = |[w+(e-w)/(2|^n)*(i+1-2), s+(a-s)/(2|^n)*(j-2)]| by A2,JORDAN8:def 1;
set x = (e-w)/(2|^n);
A7: 2|^n > 0 by HEINE:5;
e >= w by SPRECT_1:23;
then e - w >= w - w by REAL_1:49;
then A8: e - w >= 0 by XCMPLX_1:14;
dist(p,q) = (Pitag_dist 2).(p,q) by Lm1,METRIC_1:def 1
.= sqrt ((p1`1 - p2`1)^2 + (p1`2 - p2`2)^2) by A3,TOPREAL3:12
.= sqrt ((p1`1 - p2`1)^2 + (s+(a-s)/(2|^n)*(j-2) - p2`2)^2)
by A5,EUCLID:56
.= sqrt ((p1`1 - p2`1)^2 + (s+(a-s)/(2|^n)*(j-2) -
(s+(a-s)/(2|^n)*(j-2)))^2) by A6,EUCLID:56
.= sqrt ((p1`1 - p2`1)^2 + 0) by SQUARE_1:60,XCMPLX_1:14
.= abs(p1`1 - p2`1) by SQUARE_1:91
.= abs(w+x*(i-2) - p2`1) by A5,EUCLID:56
.= abs(w+x*(i-2) - (w+x*(i+1-2))) by A6,EUCLID:56
.= abs(w+x*(i-2) - w - x*(i+1-2)) by XCMPLX_1:36
.= abs(w-w+x*(i-2) - x*(i+1-2)) by XCMPLX_1:29
.= abs(0+x*(i-2) - x*(i+1-2)) by XCMPLX_1:14
.= abs(x*i-x*2 - x*(i+1-2)) by XCMPLX_1:40
.= abs(x*i-x*2 - (x*i+x*1-x*2)) by XCMPLX_1:43
.= abs(x*i-x*2 - (x*i+x*1) + x*2) by XCMPLX_1:37
.= abs(x*i-x*2 - x*i-x*1 + x*2) by XCMPLX_1:36
.= abs(x*i-(x*2 + x*i)-x + x*2) by XCMPLX_1:36
.= abs(x*i-x*i - x*2-x + x*2) by XCMPLX_1:36
.= abs(0 - x*2-x + x*2) by XCMPLX_1:14
.= abs(-x*2-x + x*2) by XCMPLX_1:150
.= abs(-x*2 + x*2 - x) by XCMPLX_1:29
.= abs(0 - x) by XCMPLX_0:def 6
.= abs(-x) by XCMPLX_1:150
.= abs(x) by ABSVALUE:17
.= abs(e-w)/abs(2|^n) by ABSVALUE:16
.= (e-w)/abs(2|^n) by A8,ABSVALUE:def 1;
hence thesis by A4,A7,ABSVALUE:def 1;
end;
theorem
for r, t being real number holds r > 0 & t > 0 implies
ex n being Nat st 1 < n &
dist(Gauge(C,n)*(1,1),Gauge(C,n)*(1,2)) < r &
dist(Gauge(C,n)*(1,1),Gauge(C,n)*(2,1)) < t
proof
let r, t be real number;
assume that
A1: r > 0 and
A2: t > 0;
set n = N-bound C, e = E-bound C, s = S-bound C, w = W-bound C;
set a = abs([\ log(2,(n-s)/r) /]) + 1,
b = abs([\ log(2,(e-w)/t) /]) + 1;
take i = max(a,b)+1;
abs([\ log(2,(n-s)/r) /]) >= 0 by ABSVALUE:5;
then A3: a >= 0+1 by REAL_1:55;
max(a,b) >= a by SQUARE_1:46;
then max(a,b) >= 1 by A3,AXIOMS:22;
then max(a,b)+1 >= 1+1 by REAL_1:55;
hence 1 < i by AXIOMS:22;
a <= max(a,b) & b <= max(a,b) by SQUARE_1:46;
then A4: a+1 <= max(a,b)+1 & b+1 <= max(a,b)+1 by AXIOMS:24;
a < a+1 & b < b+1 by REAL_1:69;
then A5: i > a & i > b by A4,AXIOMS:22;
A6: 2 to_power i > 0 by POWER:39;
then A7: 2|^i > 0 by POWER:48;
[\ log(2,(n-s)/r) /] > log(2,(n-s)/r) - 1 &
[\ log(2,(e-w)/t) /] > log(2,(e-w)/t) - 1 by INT_1:def 4;
then A8: [\ log(2,(n-s)/r) /] + 1 > log(2,(n-s)/r) - 1 + 1 &
[\ log(2,(e-w)/t) /] + 1 > log(2,(e-w)/t) - 1 + 1 by REAL_1:53;
[\ log(2,(n-s)/r) /] <= abs([\ log(2,(n-s)/r) /]) &
[\ log(2,(e-w)/t) /] <= abs([\ log(2,(e-w)/t) /]) by ABSVALUE:11;
then [\ log(2,(n-s)/r) /] + 1 <= a &
[\ log(2,(e-w)/t) /] + 1 <= b by AXIOMS:24;
then a > log(2,(n-s)/r) - 1 + 1 &
b > log(2,(e-w)/t) - 1 + 1 by A8,AXIOMS:22;
then a > log(2,(n-s)/r) & b > log(2,(e-w)/t) by XCMPLX_1:27;
then i > log(2,(n-s)/r) & i > log(2,(e-w)/t) by A5,AXIOMS:22;
then log(2,2 to_power i) > log(2,(n-s)/r) &
log(2,2 to_power i) > log(2,(e-w)/t) by A6,POWER:def 3;
then 2 to_power i > (n-s)/r & 2 to_power i > (e-w)/t by A6,PRE_FF:12;
then 2|^i > (n-s)/r & 2|^i > (e-w)/t by POWER:48;
then 2|^i * r > (n-s)/r * r & 2|^i * t > (e-w)/t * t by A1,A2,REAL_1:70;
then 2|^i * r > n-s & 2|^i * t > e-w by A1,A2,XCMPLX_1:88;
then 2|^i * r / 2|^i > (n-s) / 2|^i & 2|^i * t / 2|^i > (e-w) / 2|^i
by A7,REAL_1:73;
then A9: (n-s)/2|^i < r & (e-w)/2|^i < t by A7,XCMPLX_1:90;
A10: len Gauge(C,i) = width Gauge(C,i) by JORDAN8:def 1;
len Gauge(C,i) >= 4 by JORDAN8:13;
then 1 <= len Gauge(C,i) & 1+1 <= width Gauge(C,i) by A10,AXIOMS:22;
then [1,1] in Indices Gauge(C,i) & [1,1+1] in Indices Gauge(C,i) &
[1+1,1] in Indices Gauge(C,i) by A10,GOBOARD7:10;
hence thesis by A9,Th19,Th20;
end;
begin :: LeftComp and RightComp
theorem Th22:
for P being Subset of (TOP-REAL 2)|(L~f)` st
P is_a_component_of (TOP-REAL 2)|(L~f)` holds
P = RightComp f or P = LeftComp f
proof
let P be Subset of (TOP-REAL 2)|(L~f)`;
assume that
A1: P is_a_component_of (TOP-REAL 2)|(L~f)` and
A2: P <> RightComp f;
LeftComp f is_a_component_of (L~f)` by GOBOARD9:def 1;
then consider L being Subset of (TOP-REAL 2)|(L~f)` such that
A3: L = LeftComp f & L is_a_component_of (TOP-REAL 2)|(L~f)`
by CONNSP_1:def 6;
RightComp f is_a_component_of (L~f)` by GOBOARD9:def 2;
then consider R being Subset of (TOP-REAL 2)|(L~f)` such that
A4: R = RightComp f and
A5: R is_a_component_of (TOP-REAL 2)|(L~f)` by CONNSP_1:def 6;
A6: P misses R by A1,A2,A4,A5,CONNSP_1:37;
P <> {}((TOP-REAL 2)|(L~f)`) by A1,CONNSP_1:34;
then consider a being Point of (TOP-REAL 2)|(L~f)` such that
A7: a in P by SUBSET_1:10;
A8: the carrier of (TOP-REAL 2)|(L~f)` = (L~f)` by JORDAN1:1;
(L~f)` = LeftComp f \/ RightComp f by GOBRD12:11;
then a in LeftComp f or a in RightComp f by A8,XBOOLE_0:def 2;
then P meets LeftComp f by A4,A6,A7,XBOOLE_0:3;
hence P = LeftComp f by A1,A3,CONNSP_1:37;
end;
theorem
for A1, A2 being Subset of TOP-REAL 2 st
(L~f)` = A1 \/ A2 & A1 misses A2 &
for C1, C2 being Subset of (TOP-REAL 2)|(L~f)`
st C1 = A1 & C2 = A2 holds
C1 is_a_component_of (TOP-REAL 2)|(L~f)` &
C2 is_a_component_of (TOP-REAL 2)|(L~f)`
holds A1 = RightComp f & A2 = LeftComp f or
A1 = LeftComp f & A2 = RightComp f
proof
let A1, A2 be Subset of TOP-REAL 2 such that
A1: (L~f)` = A1 \/ A2 and
A2: A1 /\ A2 = {} and
A3: for C1, C2 being Subset of (TOP-REAL 2)|(L~f)`
st C1 = A1 & C2 = A2 holds
C1 is_a_component_of (TOP-REAL 2)|(L~f)` &
C2 is_a_component_of (TOP-REAL 2)|(L~f)`;
A4: the carrier of (TOP-REAL 2)|(L~f)` = (L~f)` by JORDAN1:1;
A1 c= A1 \/ A2 & A2 c= A1 \/ A2 by XBOOLE_1:7;
then reconsider C1 = A1, C2 = A2 as Subset of (TOP-REAL 2)|(L~f)`
by A1,A4;
A5: C1 = A1 & C2 = A2;
then A6: C1 is_a_component_of (TOP-REAL 2)|(L~f)` by A3;
C2 is_a_component_of (TOP-REAL 2)|(L~f)` by A3,A5;
then A7: (C1 = RightComp f or C1 = LeftComp f) &
(C2 = RightComp f or C2 = LeftComp f) by A6,Th22;
assume not thesis;
hence contradiction by A2,A7;
end;
theorem Th24:
LeftComp f misses RightComp f
proof
assume LeftComp f /\ RightComp f <> {};
then consider x being set such that
A1: x in LeftComp f /\ RightComp f by XBOOLE_0:def 1;
A2: LeftComp f meets RightComp f
proof
now take x;
thus x in LeftComp f & x in RightComp f by A1,XBOOLE_0:def 3; end;
hence thesis by XBOOLE_0:3;
end;
LeftComp f is_a_component_of (L~f)` & RightComp f is_a_component_of (L~f)
`
by GOBOARD9:def 1,def 2;
then LeftComp f = RightComp f by A2,GOBOARD9:3;
hence thesis by SPRECT_4:7;
end;
theorem Th25:
L~f \/ RightComp f \/ LeftComp f = the carrier of TOP-REAL 2
proof
A1: (L~f)` = RightComp f \/ LeftComp f by GOBRD12:11;
(L~f)` \/ L~f = [#]the carrier of TOP-REAL 2 by SUBSET_1:25
.= the carrier of TOP-REAL 2 by SUBSET_1:def 4;
hence thesis by A1,XBOOLE_1:4;
end;
theorem Th26:
p in L~f iff not p in LeftComp f & not p in RightComp f
proof
A1: (L~f)` = LeftComp f \/ RightComp f by GOBRD12:11;
p in L~f iff not p in (L~f)` by SUBSET_1:50,54;
hence thesis by A1,XBOOLE_0:def 2;
end;
theorem Th27:
p in LeftComp f iff not p in L~f & not p in RightComp f
proof
A1: (L~f)` = LeftComp f \/ RightComp f by GOBRD12:11;
LeftComp f misses RightComp f by Th24;
then A2: LeftComp f /\ RightComp f = {} by XBOOLE_0:def 7;
p in L~f iff not p in (L~f)` by SUBSET_1:50,54;
hence thesis by A1,A2,XBOOLE_0:def 2,def 3;
end;
theorem
p in RightComp f iff not p in L~f & not p in LeftComp f by Th26,Th27;
theorem Th29:
L~f = (Cl RightComp f) \ RightComp f
proof
thus L~f c= (Cl RightComp f) \ RightComp f
proof
let x be set; assume
A1: x in L~f;
then reconsider p = x as Point of TOP-REAL 2;
consider i such that
A2: 1 <= i & i+1 <= len f and
A3: p in LSeg(f,i) by A1,SPPOL_2:13;
for O being Subset of TOP-REAL 2 st O is open holds
p in O implies RightComp f meets O
proof
let O be Subset of TOP-REAL 2 such that
A4: O is open and
A5: p in O;
left_cell(f,i) /\ right_cell(f,i) = LSeg(f,i) by A2,GOBOARD5:32;
then LSeg(f,i) c= right_cell(f,i) by XBOOLE_1:17;
then A6: p in right_cell(f,i) by A3;
f is_sequence_on GoB f by GOBOARD5:def 5;
then consider i1, j1, i2, j2 being Nat such that
A7: [i1,j1] in Indices GoB f & f/.i = GoB f*(i1,j1) &
[i2,j2] in Indices GoB f & f/.(i+1) = GoB f*(i2,j2) and
A8: i1 = i2 & j1+1 = j2 or i1+1 = i2 & j1 = j2 or
i1 = i2+1 & j1 = j2 or i1 = i2 & j1 = j2+1 by A2,JORDAN8:6;
A9: 1 <= i1 & 1 <= j1 by A7,GOBOARD5:1;
A10: i1 <= len GoB f & j1 <= width GoB f by A7,GOBOARD5:1;
A11: i2 <= len GoB f & j2 <= width GoB f by A7,GOBOARD5:1;
now per cases by A8;
case
A12: i1 = i2 & j1+1 = j2;
set w = i1-'1;
A13: w+1 = i1 by A9,AMI_5:4;
then right_cell(f,i) = cell(GoB f,w+1,j1) by A2,A7,A12,GOBOARD5:28;
hence p in Cl Int right_cell(f,i) by A6,A10,A13,GOBRD11:35;
case
A14: i1+1 = i2 & j1 = j2;
set w = j1-'1;
w+1 = j1 by A9,AMI_5:4;
then A15: right_cell(f,i) = cell(GoB f,i1,w) by A2,A7,A14,GOBOARD5:29;
w <= w+1 & w+1 <= width GoB f by A9,A10,AMI_5:4,NAT_1:29;
then w <= width GoB f by AXIOMS:22;
hence p in Cl Int right_cell(f,i) by A6,A10,A15,GOBRD11:35;
case
A16: i1 = i2+1 & j1 = j2;
set w = j1-'1;
A17: w+1 = j1 by A9,AMI_5:4;
then right_cell(f,i) = cell(GoB f,i2,w+1) by A2,A7,A16,GOBOARD5:30;
hence p in Cl Int right_cell(f,i) by A6,A10,A11,A17,GOBRD11:35;
case
A18: i1 = i2 & j1 = j2+1;
set z = i1-'1;
z+1 = i1 by A9,AMI_5:4;
then A19: right_cell(f,i) = cell(GoB f,z,j2) by A2,A7,A18,GOBOARD5:31;
z <= z+1 & z+1 <= len GoB f by A9,A10,AMI_5:4,NAT_1:29;
then z <= len GoB f by AXIOMS:22;
hence p in Cl Int right_cell(f,i) by A6,A11,A19,GOBRD11:35;
end;
then A20: O meets Int right_cell(f,i) by A4,A5,PRE_TOPC:def 13;
Int right_cell(f,i) c= RightComp f by A2,GOBOARD9:28;
hence RightComp f meets O by A20,XBOOLE_1:63;
end;
then A21: p in Cl RightComp f by PRE_TOPC:def 13;
not x in RightComp f by A1,Th26;
hence thesis by A21,XBOOLE_0:def 4;
end;
assume not (Cl RightComp f) \ RightComp f c= L~f;
then consider q being set such that
A22: q in (Cl RightComp f) \ RightComp f and
A23: not q in L~f by TARSKI:def 3;
reconsider q as Point of TOP-REAL 2 by A22;
A24: q in Cl RightComp f & not q in RightComp f by A22,XBOOLE_0:def 4;
then q in LeftComp f by A23,Th26;
then LeftComp f meets RightComp f by A24,PRE_TOPC:def 13;
hence contradiction by Th24;
end;
theorem Th30:
L~f = (Cl LeftComp f) \ LeftComp f
proof
thus L~f c= (Cl LeftComp f) \ LeftComp f
proof
let x be set; assume
A1: x in L~f;
then reconsider p = x as Point of TOP-REAL 2;
consider i such that
A2: 1 <= i & i+1 <= len f and
A3: p in LSeg(f,i) by A1,SPPOL_2:13;
for O being Subset of TOP-REAL 2 st O is open holds
p in O implies LeftComp f meets O
proof
let O be Subset of TOP-REAL 2 such that
A4: O is open and
A5: p in O;
left_cell(f,i) /\ right_cell(f,i) = LSeg(f,i) by A2,GOBOARD5:32;
then LSeg(f,i) c= left_cell(f,i) by XBOOLE_1:17;
then A6: p in left_cell(f,i) by A3;
f is_sequence_on GoB f by GOBOARD5:def 5;
then consider i1, j1, i2, j2 being Nat such that
A7: [i1,j1] in Indices GoB f & f/.i = GoB f*(i1,j1) &
[i2,j2] in Indices GoB f & f/.(i+1) = GoB f*(i2,j2) and
A8: i1 = i2 & j1+1 = j2 or i1+1 = i2 & j1 = j2 or
i1 = i2+1 & j1 = j2 or i1 = i2 & j1 = j2+1 by A2,JORDAN8:6;
A9: 1 <= i1 & 1 <= j1 by A7,GOBOARD5:1;
A10: i1 <= len GoB f & j1 <= width GoB f by A7,GOBOARD5:1;
A11: i2 <= len GoB f & j2 <= width GoB f by A7,GOBOARD5:1;
now per cases by A8;
case
A12: i1 = i2 & j1+1 = j2;
set w = i1-'1;
w+1 = i1 by A9,AMI_5:4;
then A13: left_cell(f,i) = cell(GoB f,w,j1) by A2,A7,A12,GOBOARD5:28;
w <= w+1 & w+1 <= len GoB f by A9,A10,AMI_5:4,NAT_1:29;
then w <= len GoB f by AXIOMS:22;
hence p in Cl Int left_cell(f,i) by A6,A10,A13,GOBRD11:35;
case
A14: i1+1 = i2 & j1 = j2;
set w = j1-'1;
w+1 = j1 by A9,AMI_5:4;
then A15: left_cell(f,i) = cell(GoB f,i1,w+1) by A2,A7,A14,GOBOARD5:29;
w+1 <= width GoB f by A9,A10,AMI_5:4;
hence p in Cl Int left_cell(f,i) by A6,A10,A15,GOBRD11:35;
case
A16: i1 = i2+1 & j1 = j2;
set w = j1-'1;
w+1 = j1 by A9,AMI_5:4;
then A17: left_cell(f,i) = cell(GoB f,i2,w) by A2,A7,A16,GOBOARD5:30;
w <= w+1 & w+1 <= width GoB f by A9,A10,AMI_5:4,NAT_1:29;
then w <= width GoB f by AXIOMS:22;
hence p in Cl Int left_cell(f,i) by A6,A11,A17,GOBRD11:35;
case
A18: i1 = i2 & j1 = j2+1;
set z = i1-'1;
z+1 = i1 by A9,AMI_5:4;
then A19: left_cell(f,i) = cell(GoB f,z+1,j2) by A2,A7,A18,GOBOARD5:31;
z+1 <= len GoB f by A9,A10,AMI_5:4;
hence p in Cl Int left_cell(f,i) by A6,A11,A19,GOBRD11:35;
end;
then A20: O meets Int left_cell(f,i) by A4,A5,PRE_TOPC:def 13;
Int left_cell(f,i) c= LeftComp f by A2,GOBOARD9:24;
hence LeftComp f meets O by A20,XBOOLE_1:63;
end;
then A21: p in Cl LeftComp f by PRE_TOPC:def 13;
not x in LeftComp f by A1,Th26;
hence thesis by A21,XBOOLE_0:def 4;
end;
assume not (Cl LeftComp f) \ LeftComp f c= L~f;
then consider q being set such that
A22: q in (Cl LeftComp f) \ LeftComp f and
A23: not q in L~f by TARSKI:def 3;
reconsider q as Point of TOP-REAL 2 by A22;
A24: q in Cl LeftComp f & not q in LeftComp f by A22,XBOOLE_0:def 4;
then q in RightComp f by A23,Th26;
then RightComp f meets LeftComp f by A24,PRE_TOPC:def 13;
hence contradiction by Th24;
end;
theorem Th31:
Cl RightComp f = (RightComp f) \/ L~f
proof
thus Cl RightComp f c= RightComp f \/ L~f
proof
let x be set;
assume
A1: x in Cl RightComp f;
now
assume
A2: not x in RightComp f;
now
assume x in LeftComp f;
then LeftComp f meets RightComp f by A1,TOPS_1:39;
hence contradiction by Th24;
end;
hence x in L~f by A1,A2,Th26;
end;
hence thesis by XBOOLE_0:def 2;
end;
L~f c= (Cl RightComp f) \ RightComp f &
(Cl RightComp f) \ RightComp f c= Cl RightComp f by Th29,XBOOLE_1:36
;
then RightComp f c= Cl RightComp f & L~f c= Cl RightComp f
by PRE_TOPC:48,XBOOLE_1:1;
hence thesis by XBOOLE_1:8;
end;
theorem
Cl LeftComp f = (LeftComp f) \/ L~f
proof
thus Cl LeftComp f c= LeftComp f \/ L~f
proof
let x be set;
assume
A1: x in Cl LeftComp f;
now
assume
A2: not x in LeftComp f;
now
assume x in RightComp f;
then LeftComp f meets RightComp f by A1,TOPS_1:39;
hence contradiction by Th24;
end;
hence x in L~f by A1,A2,Th26;
end;
hence thesis by XBOOLE_0:def 2;
end;
L~f c= (Cl LeftComp f) \ LeftComp f &
(Cl LeftComp f) \ LeftComp f c= Cl LeftComp f by Th30,XBOOLE_1:36;
then LeftComp f c= Cl LeftComp f & L~f c= Cl LeftComp f
by PRE_TOPC:48,XBOOLE_1:1;
hence thesis by XBOOLE_1:8;
end;
definition let f be non constant standard special_circular_sequence;
cluster L~f -> Jordan;
coherence
proof
thus (L~f)` <> {};
take A1 = RightComp f, A2 = LeftComp f;
thus (L~f)` = A1 \/ A2 by GOBRD12:11;
A1 misses A2 & L~f = (Cl A1) \ A1 by Th24,Th29;
hence thesis by Th30,GOBOARD9:def 1,def 2;
end;
end;
reserve f for clockwise_oriented
non constant standard special_circular_sequence;
theorem Th33:
p in RightComp f implies W-bound L~f < p`1
proof set g = Rotate(f,N-min L~f);
A1: L~f = L~g by REVROT_1:33;
N-min L~f in rng f by SPRECT_2:43;
then A2: g/.1 = N-min L~g by A1,FINSEQ_6:98;
reconsider u = p as Point of Euclid 2 by TOPREAL3:13;
assume p in RightComp f;
then p in RightComp g by REVROT_1:37;
then u in Int RightComp g by TOPS_1:55;
then consider r being real number such that
A3: r > 0 and
A4: Ball(u,r) c= RightComp g by GOBOARD6:8;
reconsider r as Real by XREAL_0:def 1;
A5: W-bound L~SpStSeq L~g = W-bound L~g by SPRECT_1:66;
A6: W-bound L~SpStSeq L~g = inf(proj1.:L~SpStSeq L~g) by SPRECT_1:48;
A7: proj1.:L~SpStSeq L~g is bounded_below by SPRECT_1:46;
set x = |[p`1-r/2,N-bound L~SpStSeq L~g]|;
reconsider k = |[p`1-r/2,p`2]| as Point of Euclid 2 by TOPREAL3:13;
A8: r/2 > 0 by A3,REAL_2:127;
dist(u,k) = (Pitag_dist 2).(u,k) by Lm1,METRIC_1:def 1
.= sqrt ((p`1 - |[p`1-r/2,p`2]|`1)^2 + (p`2 - |[p`1-r/2,p`2]|`2)^2)
by TOPREAL3:12
.= sqrt ((p`1 - (p`1-r/2))^2 + (p`2 - |[p`1-r/2,p`2]|`2)^2) by EUCLID:56
.= sqrt ((p`1 - (p`1-r/2))^2 + (p`2 - p`2)^2) by EUCLID:56
.= sqrt ((p`1 - (p`1-r/2))^2 + 0) by SQUARE_1:60,XCMPLX_1:14
.= sqrt ((p`1 - p`1 + r/2)^2 + 0) by XCMPLX_1:37
.= sqrt ((0 + r/2)^2) by XCMPLX_1:14
.= r/2 by A8,SQUARE_1:89;
then dist(u,k) < r/1 by A3,REAL_2:200;
then A9: k in Ball(u,r) by METRIC_1:12;
RightComp g misses LeftComp g by Th24;
then A10: not |[p`1-r/2,p`2]| in LeftComp g by A4,A9,XBOOLE_0:3;
then |[p`1-r/2,p`2]|`1 <= E-bound L~g by A2,JORDAN2C:119;
then p`1-r/2 <= E-bound L~g by EUCLID:56;
then A11: x`1 <= E-bound L~g by EUCLID:56;
|[p`1-r/2,p`2]|`1 >= W-bound L~g by A2,A10,JORDAN2C:118;
then p`1-r/2 >= W-bound L~g by EUCLID:56;
then A12: x`1 >= W-bound L~g by EUCLID:56;
x`2 = N-bound L~SpStSeq L~g by EUCLID:56;
then A13: x`2 = N-bound L~g by SPRECT_1:68;
LSeg(NW-corner L~g, NE-corner L~g) =
{ q : q`1 <= E-bound L~g & q`1 >= W-bound L~g & q`2 = N-bound L~g}
by SPRECT_1:27;
then A14: x in LSeg(NW-corner L~g,NE-corner L~g) by A11,A12,A13;
A15: LSeg(NW-corner L~g,NE-corner L~g) c= L~SpStSeq L~g by SPRECT_3:26;
proj1.x = x`1 by PSCOMP_1:def 28
.= p`1-r/2 by EUCLID:56;
then p`1-r/2 in proj1.:L~SpStSeq L~g by A14,A15,FUNCT_2:43;
then A16: inf(proj1.:L~SpStSeq L~g) <= p`1-r/2 by A7,SEQ_4:def 5;
p`1-r/2 < p`1-0 by A8,REAL_1:92; hence thesis by A1,A5,A6,A16,AXIOMS:22
;
end;
theorem Th34:
p in RightComp f implies E-bound L~f > p`1
proof set g = Rotate(f,N-min L~f);
A1: L~f = L~g by REVROT_1:33;
N-min L~f in rng f by SPRECT_2:43;
then A2: g/.1 = N-min L~g by A1,FINSEQ_6:98;
reconsider u = p as Point of Euclid 2 by TOPREAL3:13;
assume p in RightComp f;
then p in RightComp g by REVROT_1:37;
then u in Int RightComp g by TOPS_1:55;
then consider r being real number such that
A3: r > 0 and
A4: Ball(u,r) c= RightComp g by GOBOARD6:8;
reconsider r as Real by XREAL_0:def 1;
A5: E-bound L~SpStSeq L~g = E-bound L~g by SPRECT_1:69;
A6: E-bound L~SpStSeq L~g = sup(proj1.:L~SpStSeq L~g) by SPRECT_1:51;
A7: proj1.:L~SpStSeq L~g is bounded_above by SPRECT_1:47;
set x = |[p`1+r/2,N-bound L~SpStSeq L~g]|;
reconsider k = |[p`1+r/2,p`2]| as Point of Euclid 2 by TOPREAL3:13;
A8: r/2 > 0 by A3,REAL_2:127;
dist(u,k) = (Pitag_dist 2).(u,k) by Lm1,METRIC_1:def 1
.= sqrt ((p`1 - |[p`1+r/2,p`2]|`1)^2 + (p`2 - |[p`1+r/2,p`2]|`2)^2)
by TOPREAL3:12
.= sqrt ((p`1 - (p`1+r/2))^2 + (p`2 - |[p`1+r/2,p`2]|`2)^2) by EUCLID:56
.= sqrt ((p`1 - (p`1+r/2))^2 + (p`2 - p`2)^2) by EUCLID:56
.= sqrt ((p`1 - (p`1+r/2))^2 + 0) by SQUARE_1:60,XCMPLX_1:14
.= sqrt ((p`1 - p`1 - r/2)^2 + 0) by XCMPLX_1:36
.= sqrt ((0 - r/2)^2) by XCMPLX_1:14
.= sqrt ((-r/2)^2) by XCMPLX_1:150
.= sqrt ((r/2)^2) by SQUARE_1:61
.= r/2 by A8,SQUARE_1:89;
then dist(u,k) < r/1 by A3,REAL_2:200;
then A9: k in Ball(u,r) by METRIC_1:12;
RightComp g misses LeftComp g by Th24;
then A10: not |[p`1+r/2,p`2]| in LeftComp g by A4,A9,XBOOLE_0:3;
then |[p`1+r/2,p`2]|`1 <= E-bound L~g by A2,JORDAN2C:119;
then p`1+r/2 <= E-bound L~g by EUCLID:56;
then A11: x`1 <= E-bound L~g by EUCLID:56;
|[p`1+r/2,p`2]|`1 >= W-bound L~g by A2,A10,JORDAN2C:118;
then p`1+r/2 >= W-bound L~g by EUCLID:56;
then A12: x`1 >= W-bound L~g by EUCLID:56;
x`2 = N-bound L~SpStSeq L~g by EUCLID:56;
then A13: x`2 = N-bound L~g by SPRECT_1:68;
LSeg(NW-corner L~g, NE-corner L~g) =
{ q : q`1 <= E-bound L~g & q`1 >= W-bound L~g & q`2 = N-bound L~g}
by SPRECT_1:27;
then A14: x in LSeg(NW-corner L~g,NE-corner L~g) by A11,A12,A13;
A15: LSeg(NW-corner L~g,NE-corner L~g) c= L~SpStSeq L~g by SPRECT_3:26;
proj1.x = x`1 by PSCOMP_1:def 28
.= p`1+r/2 by EUCLID:56;
then p`1+r/2 in proj1.:L~SpStSeq L~g by A14,A15,FUNCT_2:43;
then A16: sup(proj1.:L~SpStSeq L~g) >= p`1+r/2 by A7,SEQ_4:def 4;
p`1+r/2 > p`1+0 by A8,REAL_1:53;
hence thesis by A1,A5,A6,A16,AXIOMS:22;
end;
theorem Th35:
p in RightComp f implies N-bound L~f > p`2
proof set g = Rotate(f,N-min L~f);
A1: L~f = L~g by REVROT_1:33;
N-min L~f in rng f by SPRECT_2:43;
then A2: g/.1 = N-min L~g by A1,FINSEQ_6:98;
reconsider u = p as Point of Euclid 2 by TOPREAL3:13;
assume p in RightComp f;
then p in RightComp g by REVROT_1:37;
then u in Int RightComp g by TOPS_1:55;
then consider r being real number such that
A3: r > 0 and
A4: Ball(u,r) c= RightComp g by GOBOARD6:8;
reconsider r as Real by XREAL_0:def 1;
A5: N-bound L~SpStSeq L~g = N-bound L~g by SPRECT_1:68;
A6: N-bound L~SpStSeq L~g = sup(proj2.:L~SpStSeq L~g) by SPRECT_1:50;
A7: proj2.:L~SpStSeq L~g is bounded_above by SPRECT_1:47;
set x = |[E-bound L~SpStSeq L~g,p`2+r/2]|;
reconsider k = |[p`1,p`2+r/2]| as Point of Euclid 2 by TOPREAL3:13;
A8: r/2 > 0 by A3,REAL_2:127;
dist(u,k) = (Pitag_dist 2).(u,k) by Lm1,METRIC_1:def 1
.= sqrt ((p`1 - |[p`1,p`2+r/2]|`1)^2 + (p`2 - |[p`1,p`2+r/2]|`2)^2)
by TOPREAL3:12
.= sqrt ((p`1 - p`1)^2 + (p`2 - |[p`1,p`2+r/2]|`2)^2) by EUCLID:56
.= sqrt (0 + (p`2 - |[p`1,p`2+r/2]|`2)^2) by SQUARE_1:60,XCMPLX_1:14
.= sqrt ((p`2 - (p`2+r/2))^2) by EUCLID:56
.= sqrt ((p`2 - p`2 - r/2)^2) by XCMPLX_1:36
.= sqrt ((0 - r/2)^2) by XCMPLX_1:14
.= sqrt ((-r/2)^2) by XCMPLX_1:150
.= sqrt ((r/2)^2) by SQUARE_1:61
.= r/2 by A8,SQUARE_1:89;
then dist(u,k) < r/1 by A3,REAL_2:200;
then A9: k in Ball(u,r) by METRIC_1:12;
RightComp g misses LeftComp g by Th24;
then A10: not |[p`1,p`2+r/2]| in LeftComp g by A4,A9,XBOOLE_0:3;
then |[p`1,p`2+r/2]|`2 <= N-bound L~g by A2,JORDAN2C:121;
then p`2+r/2 <= N-bound L~g by EUCLID:56;
then A11: x`2 <= N-bound L~g by EUCLID:56;
|[p`1,p`2+r/2]|`2 >= S-bound L~g by A2,A10,JORDAN2C:120;
then p`2+r/2 >= S-bound L~g by EUCLID:56;
then A12: x`2 >= S-bound L~g by EUCLID:56;
x`1 = E-bound L~SpStSeq L~g by EUCLID:56;
then A13: x`1 = E-bound L~g by SPRECT_1:69;
LSeg(SE-corner L~g, NE-corner L~g) =
{ q : q`1 = E-bound L~g & q`2 <= N-bound L~g & q`2 >= S-bound L~g }
by SPRECT_1:25;
then A14: x in LSeg(SE-corner L~g,NE-corner L~g) by A11,A12,A13;
A15: LSeg(SE-corner L~g,NE-corner L~g) c= L~SpStSeq L~g by TOPREAL6:43;
proj2.x = x`2 by PSCOMP_1:def 29
.= p`2+r/2 by EUCLID:56;
then p`2+r/2 in proj2.:L~SpStSeq L~g by A14,A15,FUNCT_2:43;
then A16: sup(proj2.:L~SpStSeq L~g) >= p`2+r/2 by A7,SEQ_4:def 4;
p`2+r/2 > p`2+0 by A8,REAL_1:53;
hence thesis by A1,A5,A6,A16,AXIOMS:22;
end;
theorem Th36:
p in RightComp f implies S-bound L~f < p`2
proof set g = Rotate(f,N-min L~f);
A1: L~f = L~g by REVROT_1:33;
N-min L~f in rng f by SPRECT_2:43;
then A2: g/.1 = N-min L~g by A1,FINSEQ_6:98;
reconsider u = p as Point of Euclid 2 by TOPREAL3:13;
assume p in RightComp f;
then p in RightComp g by REVROT_1:37;
then u in Int RightComp g by TOPS_1:55;
then consider r being real number such that
A3: r > 0 and
A4: Ball(u,r) c= RightComp g by GOBOARD6:8;
reconsider r as Real by XREAL_0:def 1;
A5: S-bound L~SpStSeq L~g = S-bound L~g by SPRECT_1:67;
A6: S-bound L~SpStSeq L~g = inf(proj2.:L~SpStSeq L~g) by SPRECT_1:49;
A7: proj2.:L~SpStSeq L~g is bounded_below by SPRECT_1:46;
set x = |[E-bound L~SpStSeq L~g,p`2-r/2]|;
reconsider k = |[p`1,p`2-r/2]| as Point of Euclid 2 by TOPREAL3:13;
A8: r/2 > 0 by A3,REAL_2:127;
dist(u,k) = (Pitag_dist 2).(u,k) by Lm1,METRIC_1:def 1
.= sqrt ((p`1 - |[p`1,p`2-r/2]|`1)^2 + (p`2 - |[p`1,p`2-r/2]|`2)^2)
by TOPREAL3:12
.= sqrt ((p`1 - p`1)^2 + (p`2 - |[p`1,p`2-r/2]|`2)^2) by EUCLID:56
.= sqrt (0 + (p`2 - |[p`1,p`2-r/2]|`2)^2) by SQUARE_1:60,XCMPLX_1:14
.= sqrt ((p`2 - (p`2-r/2))^2) by EUCLID:56
.= sqrt ((p`2 - p`2 + r/2)^2) by XCMPLX_1:37
.= sqrt ((0 + r/2)^2) by XCMPLX_1:14
.= r/2 by A8,SQUARE_1:89;
then dist(u,k) < r/1 by A3,REAL_2:200;
then A9: k in Ball(u,r) by METRIC_1:12;
RightComp g misses LeftComp g by Th24;
then A10: not |[p`1,p`2-r/2]| in LeftComp g by A4,A9,XBOOLE_0:3;
then |[p`1,p`2-r/2]|`2 <= N-bound L~g by A2,JORDAN2C:121;
then p`2-r/2 <= N-bound L~g by EUCLID:56;
then A11: x`2 <= N-bound L~g by EUCLID:56;
|[p`1,p`2-r/2]|`2 >= S-bound L~g by A2,A10,JORDAN2C:120;
then p`2-r/2 >= S-bound L~g by EUCLID:56;
then A12: x`2 >= S-bound L~g by EUCLID:56;
x`1 = E-bound L~SpStSeq L~g by EUCLID:56;
then A13: x`1 = E-bound L~g by SPRECT_1:69;
LSeg(SE-corner L~g, NE-corner L~g) =
{ q : q`1 = E-bound L~g & q`2 <= N-bound L~g & q`2 >= S-bound L~g }
by SPRECT_1:25;
then A14: x in LSeg(SE-corner L~g,NE-corner L~g) by A11,A12,A13;
A15: LSeg(SE-corner L~g,NE-corner L~g) c= L~SpStSeq L~g by TOPREAL6:43;
proj2.x = x`2 by PSCOMP_1:def 29
.= p`2-r/2 by EUCLID:56;
then p`2-r/2 in proj2.:L~SpStSeq L~g by A14,A15,FUNCT_2:43;
then A16: inf(proj2.:L~SpStSeq L~g) <= p`2-r/2 by A7,SEQ_4:def 5;
p`2-r/2 < p`2-0 by A8,REAL_1:92; hence thesis by A1,A5,A6,A16,AXIOMS:22
;
end;
theorem Th37:
p in RightComp f & q in LeftComp f implies LSeg(p,q) meets L~f
proof
assume
A1: p in RightComp f & q in LeftComp f;
assume LSeg(p,q) misses L~f;
then LSeg(p,q) c= (L~f)` by TDLAT_1:2;
then LSeg(p,q) c= (L~f)`;
then LSeg(p,q) c= the carrier of (TOP-REAL 2)|(L~f)` by JORDAN1:1;
then reconsider A = LSeg(p,q) as Subset of (TOP-REAL 2)|(L~f)`
;
A2: A is connected by CONNSP_1:24;
RightComp f is_a_component_of (L~f)` by GOBOARD9:def 2;
then consider R being Subset of (TOP-REAL 2)|(L~f)` such that
A3: R = RightComp f and
A4: R is_a_component_of (TOP-REAL 2)|(L~f)` by CONNSP_1:def 6;
LeftComp f is_a_component_of (L~f)` by GOBOARD9:def 1;
then consider L being Subset of (TOP-REAL 2)|(L~f)` such that
A5: L = LeftComp f and
A6: L is_a_component_of (TOP-REAL 2)|(L~f)` by CONNSP_1:def 6;
p in A & q in A by TOPREAL1:6;
then R meets A & L meets A by A1,A3,A5,XBOOLE_0:3;
then RightComp f = LeftComp f by A2,A3,A4,A5,A6,JORDAN2C:100;
hence contradiction by SPRECT_4:7;
end;
theorem Th38:
Cl RightComp SpStSeq C =
product((1,2)-->([.W-bound L~SpStSeq C,E-bound L~SpStSeq C.],
[.S-bound L~SpStSeq C,N-bound L~SpStSeq C.]))
proof
set g = (1,2)-->([.W-bound L~SpStSeq C,E-bound L~SpStSeq C.],
[.S-bound L~SpStSeq C,N-bound L~SpStSeq C.]);
A1: Cl RightComp SpStSeq C = (RightComp SpStSeq C) \/ L~SpStSeq C by Th31;
A2: dom g = {1,2} by FUNCT_4:65;
hereby
let a be set; assume
A3: a in Cl RightComp SpStSeq C;
then consider r, s being Real such that
A4: a = <*r,s*> by EUCLID:55;
reconsider b = a as Point of TOP-REAL 2 by A3;
reconsider h = a as FinSequence by A4;
A5: dom h = {1,2} by A4,FINSEQ_1:4,FINSEQ_3:29;
for x being set st x in {1,2} holds h.x in g.x
proof
let x be set such that
A6: x in {1,2};
per cases by A6,TARSKI:def 2;
suppose
A7: x = 1;
then A8: g.x = [.W-bound L~SpStSeq C,E-bound L~SpStSeq C.] by FUNCT_4:66;
A9: h.x = r by A4,A7,FINSEQ_1:61;
A10: b`1 = |[r,s]|`1 by A4,EUCLID:def 16
.= r by EUCLID:56;
now per cases by A1,A3,XBOOLE_0:def 2;
case a in RightComp SpStSeq C;
then W-bound L~SpStSeq C < b`1 & E-bound L~SpStSeq C > b`1
by Th33,Th34;
hence h.x in g.x by A8,A9,A10,TOPREAL5:1;
case a in L~SpStSeq C;
then W-bound L~SpStSeq C <= b`1 & b`1 <= E-bound L~SpStSeq C
by PSCOMP_1:71;
hence h.x in g.x by A8,A9,A10,TOPREAL5:1;
end;
hence h.x in g.x;
suppose
A11: x = 2;
then A12: g.x = [.S-bound L~SpStSeq C,N-bound L~SpStSeq C.] by FUNCT_4:66;
A13: h.x = s by A4,A11,FINSEQ_1:61;
A14: b`2 = |[r,s]|`2 by A4,EUCLID:def 16
.= s by EUCLID:56;
now per cases by A1,A3,XBOOLE_0:def 2;
case a in RightComp SpStSeq C;
then S-bound L~SpStSeq C < b`2 & N-bound L~SpStSeq C > b`2
by Th35,Th36;
hence h.x in g.x by A12,A13,A14,TOPREAL5:1;
case a in L~SpStSeq C;
then S-bound L~SpStSeq C <= b`2 & b`2 <= N-bound L~SpStSeq C
by PSCOMP_1:71;
hence h.x in g.x by A12,A13,A14,TOPREAL5:1;
end;
hence h.x in g.x;
end;
hence a in product g by A2,A5,CARD_3:18;
end;
let a be set;
assume a in product g;
then consider h being Function such that
A15: a = h and
A16: dom h = dom g and
A17: for x being set st x in dom g holds h.x in g.x by CARD_3:def 5;
1 in dom g & 2 in dom g by A2,TARSKI:def 2;
then A18: h.1 in g.1 & h.2 in g.2 by A17;
then A19: h.1 in [.W-bound L~SpStSeq C,E-bound L~SpStSeq C.] by FUNCT_4:66;
[.W-bound L~SpStSeq C,E-bound L~SpStSeq C.] =
{r where r is Real : W-bound L~SpStSeq C <= r & r <= E-bound L~SpStSeq C}
by RCOMP_1:def 1;
then consider r being Real such that
A20: h.1 = r and
A21: W-bound L~SpStSeq C <= r & r <= E-bound L~SpStSeq C by A19;
A22: h.2 in [.S-bound L~SpStSeq C,N-bound L~SpStSeq C.] by A18,FUNCT_4:66;
[.S-bound L~SpStSeq C,N-bound L~SpStSeq C.] =
{s where s is Real: S-bound L~SpStSeq C <= s & s <= N-bound L~SpStSeq C}
by RCOMP_1:def 1;
then consider s being Real such that
A23: h.2 = s and
A24: S-bound L~SpStSeq C <= s & s <= N-bound L~SpStSeq C by A22;
A25: dom <*r,s*> = {1,2} by FINSEQ_1:4,FINSEQ_3:29;
A26: dom h = {1,2} by A16,FUNCT_4:65;
for k being set st k in dom h holds h.k = <*r,s*>.k
proof
let k be set;
assume k in dom h;
then k = 1 or k = 2 by A26,TARSKI:def 2;
hence thesis by A20,A23,FINSEQ_1:61;
end;
then a = <*r,s*> by A15,A25,A26,FUNCT_1:9;
then A27: a = |[r,s]| by EUCLID:def 16;
assume not a in Cl RightComp SpStSeq C;
then not a in RightComp SpStSeq C & not a in L~SpStSeq C by A1,XBOOLE_0:def
2
;
then A28: a in LeftComp SpStSeq C by A27,Th26;
LeftComp SpStSeq C = {q:
not(W-bound L~SpStSeq C <= q`1 & q`1 <= E-bound L~SpStSeq C &
S-bound L~SpStSeq C <= q`2 & q`2 <= N-bound L~SpStSeq C)}
by SPRECT_3:54;
then ex q st q = a &
not(W-bound L~SpStSeq C <= q`1 & q`1 <= E-bound L~SpStSeq C &
S-bound L~SpStSeq C <= q`2 & q`2 <= N-bound L~SpStSeq C) by A28;
hence contradiction by A21,A24,A27,EUCLID:56;
end;
theorem Th39:
proj1.:(Cl RightComp f) = proj1.:(L~f)
proof set g = Rotate(f,N-min L~f);
A1: L~f = L~g by REVROT_1:33;
N-min L~f in rng f by SPRECT_2:43;
then A2: g/.1 = N-min L~g by A1,FINSEQ_6:98;
L~f = (Cl RightComp f) \ RightComp f by Th29;
then A3: L~f c= Cl RightComp f by XBOOLE_1:36;
thus proj1.:(Cl RightComp f) c= proj1.:(L~f)
proof
let a be set;
assume a in proj1.:(Cl RightComp f);
then consider x being set such that
A4: x in the carrier of TOP-REAL 2 and
A5: x in Cl RightComp f and
A6: a = proj1.x by FUNCT_2:115;
A7: Cl RightComp f = (RightComp f) \/ L~f by Th31;
per cases by A5,A7,XBOOLE_0:def 2;
suppose
A8: x in RightComp f;
reconsider x as Point of TOP-REAL 2 by A4;
set b = |[x`1,N-bound L~f + 1]|;
b`2 = N-bound L~f + 1 & N-bound L~f + 1 > N-bound L~f + 0
by EUCLID:56,REAL_1:53;
then b in LeftComp g by A1,A2,JORDAN2C:121;
then b in LeftComp f by REVROT_1:36;
then LSeg(x,b) meets L~f by A8,Th37;
then consider c being set such that
A9: c in LSeg(x,b) & c in L~f by XBOOLE_0:3;
reconsider c as Point of TOP-REAL 2 by A9;
A10: b`1 = x`1 by EUCLID:56;
proj1.c = c`1 by PSCOMP_1:def 28
.= x`1 by A9,A10,GOBOARD7:5
.= a by A6,PSCOMP_1:def 28;
hence a in proj1.:(L~f) by A9,FUNCT_2:43;
suppose x in L~f;
hence a in proj1.:(L~f) by A6,FUNCT_2:43;
end;
thus thesis by A3,RELAT_1:156;
end;
theorem Th40:
proj2.:(Cl RightComp f) = proj2.:(L~f)
proof set g = Rotate(f,N-min L~f);
A1: L~f = L~g by REVROT_1:33;
N-min L~f in rng f by SPRECT_2:43;
then A2: g/.1 = N-min L~g by A1,FINSEQ_6:98;
L~f = (Cl RightComp f) \ RightComp f by Th29;
then A3: L~f c= Cl RightComp f by XBOOLE_1:36;
thus proj2.:(Cl RightComp f) c= proj2.:(L~f)
proof
let a be set;
assume a in proj2.:(Cl RightComp f);
then consider x being set such that
A4: x in the carrier of TOP-REAL 2 and
A5: x in Cl RightComp f and
A6: a = proj2.x by FUNCT_2:115;
A7: Cl RightComp f = (RightComp f) \/ L~f by Th31;
per cases by A5,A7,XBOOLE_0:def 2;
suppose
A8: x in RightComp f;
reconsider x as Point of TOP-REAL 2 by A4;
set b = |[E-bound L~f + 1,x`2]|;
b`1 = E-bound L~f + 1 & E-bound L~f + 1 > E-bound L~f + 0
by EUCLID:56,REAL_1:53;
then b in LeftComp g by A1,A2,JORDAN2C:119;
then b in LeftComp f by REVROT_1:36;
then LSeg(x,b) meets L~f by A8,Th37;
then consider c be set such that
A9: c in LSeg(x,b) & c in L~f by XBOOLE_0:3;
reconsider c as Point of TOP-REAL 2 by A9;
A10: b`2 = x`2 by EUCLID:56;
proj2.c = c`2 by PSCOMP_1:def 29
.= x`2 by A9,A10,GOBOARD7:6
.= a by A6,PSCOMP_1:def 29;
hence a in proj2.:(L~f) by A9,FUNCT_2:43;
suppose x in L~f;
hence a in proj2.:(L~f) by A6,FUNCT_2:43;
end;
thus thesis by A3,RELAT_1:156;
end;
theorem Th41:
RightComp g c= RightComp SpStSeq L~g
proof
let a be set; assume
A1: a in RightComp g;
then reconsider p = a as Point of TOP-REAL 2;
p`1 > W-bound L~g & p`1 < E-bound L~g & p`2 > S-bound L~g &
p`2 < N-bound L~g by A1,Th33,Th34,Th35,Th36;
then A2: p`1 > W-bound L~SpStSeq L~g & p`1 < E-bound L~SpStSeq L~g &
p`2 > S-bound L~SpStSeq L~g & p`2 < N-bound L~SpStSeq L~g
by SPRECT_1:66,67,68,69;
RightComp SpStSeq L~g =
{q : W-bound L~SpStSeq L~g < q`1 & q`1 < E-bound L~SpStSeq L~g &
S-bound L~SpStSeq L~g < q`2 & q`2 < N-bound L~SpStSeq L~g}
by SPRECT_3:54;
hence a in RightComp SpStSeq L~g by A2;
end;
theorem Th42:
Cl RightComp g is compact
proof
Cl RightComp SpStSeq L~g =
product((1,2)-->([.W-bound L~SpStSeq L~g,E-bound L~SpStSeq L~g.],
[.S-bound L~SpStSeq L~g,N-bound L~SpStSeq L~g.]))
by Th38;
then A1: Cl RightComp SpStSeq L~g is compact by TOPREAL6:87;
RightComp g c= RightComp SpStSeq L~g by Th41;
then Cl RightComp g c= Cl RightComp SpStSeq L~g by PRE_TOPC:49;
hence thesis by A1,COMPTS_1:18;
end;
theorem Th43:
LeftComp g is non Bounded
proof
A1: L~g \/ RightComp g \/ LeftComp g = the carrier of TOP-REAL 2 by Th25;
A2: RightComp g c= Cl RightComp g by PRE_TOPC:48;
Cl RightComp g is compact by Th42;
then A3: L~g is Bounded & Cl RightComp g is Bounded by JORDAN2C:73;
then RightComp g is Bounded by A2,JORDAN2C:16;
then L~g \/ RightComp g is Bounded by A3,TOPREAL6:76;
hence thesis by A1,TOPREAL6:74;
end;
theorem Th44:
LeftComp g is_outside_component_of L~g
proof
thus LeftComp g is_a_component_of (L~g)` by GOBOARD9:def 1;
thus not LeftComp g is Bounded by Th43;
end;
theorem
RightComp g is_inside_component_of L~g
proof
thus RightComp g is_a_component_of (L~g)` by GOBOARD9:def 2;
A1: RightComp g c= Cl RightComp g by PRE_TOPC:48;
Cl RightComp g is compact by Th42;
then Cl RightComp g is Bounded by JORDAN2C:73;
hence RightComp g is Bounded by A1,JORDAN2C:16;
end;
theorem Th46:
UBD L~g = LeftComp g
proof
L~g is Bounded by JORDAN2C:73;
then A1: ex B being Subset of TOP-REAL 2 st B is_outside_component_of L~g &
B = UBD L~g by JORDAN2C:76;
LeftComp g is_outside_component_of L~g by Th44;
hence thesis by A1,Th6;
end;
theorem Th47:
BDD L~g = RightComp g
proof
UBD L~g = LeftComp g &
(L~g)` = LeftComp g \/ RightComp g & (L~g)` = (BDD L~g) \/ (UBD L~g) &
LeftComp g misses RightComp g & (BDD L~g) misses (UBD L~g)
by Th24,Th46,GOBRD12:11,JORDAN2C:28,31;
hence thesis by XBOOLE_1:71;
end;
theorem
P is_outside_component_of L~g implies P = LeftComp g
proof
L~g is Bounded by JORDAN2C:73;
then consider B being Subset of TOP-REAL 2 such that
A1: B is_outside_component_of L~g & B = UBD L~g by JORDAN2C:76;
assume that
A2: P is_outside_component_of L~g;
P = B by A1,A2,Th6;
hence thesis by A1,Th46;
end;
theorem Th49:
P is_inside_component_of L~g implies P meets RightComp g
proof
assume that
A1: P is_inside_component_of L~g;
A2: BDD L~g = RightComp g by Th47;
A3: P c= BDD L~g by A1,JORDAN2C:26;
P is_a_component_of (L~g)` by A1,JORDAN2C:def 3;
then P <> {} by SPRECT_1:6;
hence thesis by A2,A3,XBOOLE_1:67;
end;
theorem
P is_inside_component_of L~g implies P = BDD L~g
proof
assume that
A1: P is_inside_component_of L~g;
A2: P is_a_component_of (L~g)` by A1,JORDAN2C:def 3;
A3: P meets RightComp g by A1,Th49;
A4: RightComp g = BDD L~g by Th47;
L~g is Bounded by JORDAN2C:73;
then BDD L~g is_inside_component_of L~g by JORDAN2C:116;
then BDD L~g is_a_component_of (L~g)` by JORDAN2C:def 3;
hence thesis by A2,A3,A4,GOBOARD9:3;
end;
theorem
W-bound L~g = W-bound RightComp g
proof
set A = (Cl RightComp g) \ RightComp g;
A1: L~g = A by Th29;
then reconsider A as non empty Subset of TOP-REAL 2;
A2: proj1.:(Cl RightComp g) = proj1.:(L~g) by Th39;
Cl RightComp g is compact by Th42;
then RightComp g c= Cl RightComp g & Cl RightComp g is Bounded
by JORDAN2C:73,PRE_TOPC:48;
then A3: RightComp g is Bounded by JORDAN2C:16;
W-bound A = inf (proj1.:A) &
W-bound Cl RightComp g = inf (proj1.:(Cl RightComp g)) by SPRECT_1:48;
hence thesis by A1,A2,A3,TOPREAL6:94;
end;
theorem
E-bound L~g = E-bound RightComp g
proof
set A = (Cl RightComp g) \ RightComp g;
A1: L~g = A by Th29;
then reconsider A as non empty Subset of TOP-REAL 2;
A2: proj1.:(Cl RightComp g) = proj1.:(L~g) by Th39;
Cl RightComp g is compact by Th42;
then RightComp g c= Cl RightComp g & Cl RightComp g is Bounded
by JORDAN2C:73,PRE_TOPC:48;
then A3: RightComp g is Bounded by JORDAN2C:16;
E-bound A = sup (proj1.:A) &
E-bound Cl RightComp g = sup (proj1.:(Cl RightComp g)) by SPRECT_1:51;
hence thesis by A1,A2,A3,TOPREAL6:95;
end;
theorem
N-bound L~g = N-bound RightComp g
proof
set A = (Cl RightComp g) \ RightComp g;
A1: L~g = A by Th29;
then reconsider A as non empty Subset of TOP-REAL 2;
A2: proj2.:(Cl RightComp g) = proj2.:(L~g) by Th40;
Cl RightComp g is compact by Th42;
then RightComp g c= Cl RightComp g & Cl RightComp g is Bounded
by JORDAN2C:73,PRE_TOPC:48;
then A3: RightComp g is Bounded by JORDAN2C:16;
N-bound A = sup (proj2.:A) &
N-bound Cl RightComp g = sup (proj2.:(Cl RightComp g)) by SPRECT_1:50;
hence thesis by A1,A2,A3,TOPREAL6:96;
end;
theorem
S-bound L~g = S-bound RightComp g
proof
set A = (Cl RightComp g) \ RightComp g;
A1: L~g = A by Th29;
then reconsider A as non empty Subset of TOP-REAL 2;
A2: proj2.:(Cl RightComp g) = proj2.:(L~g) by Th40;
Cl RightComp g is compact by Th42;
then RightComp g c= Cl RightComp g & Cl RightComp g is Bounded
by JORDAN2C:73,PRE_TOPC:48;
then A3: RightComp g is Bounded by JORDAN2C:16;
S-bound A = inf (proj2.:A) &
S-bound Cl RightComp g = inf (proj2.:(Cl RightComp g)) by SPRECT_1:49;
hence thesis by A1,A2,A3,TOPREAL6:97;
end;