:: Properties of Left-, and Right Components
:: by Artur Korni{\l}owicz
::
:: Received May 5, 1999
:: Copyright (c) 1999-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies NUMBERS, SUBSET_1, FUNCT_1, GOBOARD5, SPRECT_2, PRE_TOPC, EUCLID,
RCOMP_1, SPPOL_1, GOBOARD1, STRUCT_0, JORDAN2C, TOPREAL1, REAL_1,
XXREAL_0, CARD_1, METRIC_1, TARSKI, XXREAL_2, ARYTM_3, XBOOLE_0,
COMPLEX1, RELAT_2, CONNSP_1, FINSEQ_1, TREES_1, CARD_3, FUNCOP_1,
XXREAL_1, RELAT_1, MCART_1, MATRIX_1, ARYTM_1, SQUARE_1, JORDAN8, NEWTON,
PSCOMP_1, INT_1, POWER, GOBOARD9, RLTOPSP1, GOBOARD2, PARTFUN1, TOPS_1,
JORDAN1, FINSEQ_6, SPRECT_1, SEQ_4, FINSEQ_2, NAT_1;
notations TARSKI, XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1, RELSET_1, PARTFUN1,
BINOP_1, ORDINAL1, NUMBERS, XCMPLX_0, XREAL_0, COMPLEX1, REAL_1,
XXREAL_0, XXREAL_2, SQUARE_1, NAT_1, INT_1, INT_2, NEWTON, POWER,
MATRIX_0, NAT_D, MATRIX_1, FUNCT_4, SEQ_4, METRIC_1, TBSP_1, FINSEQ_1,
CARD_3, FINSEQ_2, FINSEQ_6, STRUCT_0, RCOMP_1, PRE_TOPC, TOPS_1,
CONNSP_1, COMPTS_1, RLTOPSP1, EUCLID, TOPREAL1, GOBOARD1, GOBOARD2,
GOBOARD5, GOBOARD9, PSCOMP_1, SPPOL_1, SPRECT_1, SPRECT_2, JORDAN2C,
JORDAN8, TOPREAL6;
constructors FUNCT_4, REAL_1, SQUARE_1, RCOMP_1, NEWTON, POWER, NAT_D, TOPS_1,
CONNSP_1, COMPTS_1, TBSP_1, MONOID_0, TOPREAL4, GOBOARD2, SPPOL_1,
JORDAN1, PSCOMP_1, GOBOARD9, SPRECT_1, SPRECT_2, JORDAN2C, TOPREAL6,
JORDAN8, GOBOARD1, SEQ_4, RELSET_1, CONVEX1, BINOP_2, MATRIX_1, BINOP_1;
registrations SUBSET_1, NUMBERS, XREAL_0, NAT_1, INT_1, MEMBERED, FINSEQ_6,
STRUCT_0, PRE_TOPC, TOPS_1, MONOID_0, EUCLID, GOBOARD2, GOBRD11,
SPRECT_1, SPRECT_3, JORDAN2C, REVROT_1, TOPREAL6, FUNCT_1, FINSEQ_1,
PSCOMP_1, RELSET_1, JORDAN5A, NEWTON, SQUARE_1, ORDINAL1;
requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM;
definitions TARSKI, JORDAN2C, SPRECT_1, XBOOLE_0;
equalities JORDAN2C, XBOOLE_0, SQUARE_1, SUBSET_1, EUCLID;
expansions TARSKI, JORDAN2C, XBOOLE_0;
theorems ABSVALUE, CARD_3, FUNCT_4, COMPTS_1, CONNSP_1, EUCLID, FINSEQ_1,
FUNCT_1, FUNCT_2, GOBOARD5, GOBOARD6, GOBOARD7, GOBOARD9, GOBRD11,
GOBRD12, INT_1, JORDAN2C, JORDAN8, METRIC_1, NAT_1, POWER, PRE_TOPC,
PRE_FF, PSCOMP_1, RCOMP_1, RELAT_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, SPRECT_2, REVROT_1, FINSEQ_6, XBOOLE_0, XBOOLE_1,
XREAL_0, XCMPLX_1, COMPLEX1, XREAL_1, NEWTON, XXREAL_0, FINSEQ_2,
MATRIX_0, XXREAL_1, NAT_D, RLTOPSP1;
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 for Subset of TOP-REAL 2,
C for compact non vertical non horizontal Subset of TOP-REAL 2,
G for Go-board;
Lm1: the carrier of TOP-REAL 2 = REAL 2 by EUCLID:22;
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;
reconsider D = L~f as bounded Subset of Euclid 2 by JORDAN2C:11;
consider r being Real, c being Point of Euclid 2 such that
A3: 0 < r and
c in D and
A4: for z being Point of Euclid 2 st z in D holds dist(c,z) <= r by TBSP_1:10;
set rr = dist(p,c)+r+1;
take rr;
set L = (REAL 2) \ {a where a is Point of TOP-REAL 2: |.a.| < rr};
dist(p,c)+r+0 < rr by XREAL_1:8;
hence 0 < rr by A3,METRIC_1:5,XREAL_1:8;
then rr = |.rr.| by ABSVALUE:def 1;
then for a being Point of TOP-REAL 2 holds a <> |[0,rr]| or |.a.| >= rr by
TOPREAL6:23;
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 Lm1,XBOOLE_0:def 5;
let x be object;
assume
A5: x in Ball(p,rr)`;
then reconsider y = x as Point of Euclid 2;
reconsider z = y as Point of TOP-REAL 2 by EUCLID:22;
A6: dist(p,y) = |.z.| by A1,TOPREAL6:25;
A7: D c= Ball(p,rr)
proof
let x be object;
A8: dist(p,c) + r + 0 < dist(p,c) + r + 1 by XREAL_1:6;
assume
A9: x in D;
then reconsider z = x as Point of Euclid 2;
dist(c,z) <= r by A4,A9;
then
A10: dist(p,c) + dist(c,z) <= dist(p,c) + r by XREAL_1:7;
dist(p,z) <= dist(p,c) + dist(c,z) by METRIC_1:4;
then dist(p,z) <= dist(p,c) + r by A10,XXREAL_0:2;
then dist(p,z) < dist(p,c) + r + 1 by A8,XXREAL_0:2;
hence thesis by METRIC_1:11;
end;
A11: L c= (L~f)`
proof
let l be object;
assume
A12: l in L;
then reconsider j = l as Point of TOP-REAL 2;
reconsider t = j as Point of Euclid 2 by EUCLID:22;
not l in {a where a is Point of TOP-REAL 2: |.a.| < rr} by A12,
XBOOLE_0:def 5;
then
A13: |.j.| >= rr;
now
assume l in L~f;
then dist(t,p) < rr by A7,METRIC_1:11;
hence contradiction by A1,A13,TOPREAL6:25;
end;
hence thesis by A12,SUBSET_1:29;
end;
L is connected by JORDAN2C:53;
then consider M being Subset of TOP-REAL 2 such that
A14: M is_a_component_of (L~f)` and
A15: L c= M by A11,GOBOARD9:3;
M is_outside_component_of L~f
proof
reconsider W = L as Subset of Euclid 2;
thus M is_a_component_of (L~f)` by A14;
W is not bounded by JORDAN2C:62;
then L is not bounded by JORDAN2C:11;
hence thesis by A15,RLTOPSP1:42;
end;
then
A16: M in {W where W is Subset of TOP-REAL 2: W is_outside_component_of L~ f };
not x in Ball(p,rr) by A5,XBOOLE_0:def 5;
then for k being Point of TOP-REAL 2 holds k <> z or |.k.| >= rr by A6,
METRIC_1:11;
then z in REAL 2 & not x in {a where a is Point of TOP-REAL 2: |.a.| < rr};
then
A17: x in L by XBOOLE_0:def 5;
UBD L~f is_outside_component_of L~f by JORDAN2C:68;
then P = UBD L~f by A2,JORDAN2C:119;
hence thesis by A17,A15,A16,TARSKI:def 4;
end;
begin :: Go-boards
theorem
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:22;
then len f > 1 by NAT_1:25;
then len f >= 1 + 1 by NAT_1:13;
hence thesis;
end;
theorem Th3:
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
A1: [.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.]);
A2: dom f = {1,2} by FUNCT_4:62;
assume 1 <= i & i < len G & 1 <= j & j < width G;
then
A3: 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;
A4: [.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 } by RCOMP_1:def 1;
thus cell(G,i,j) c= product f
proof
let c be object;
assume c in cell(G,i,j);
then consider r, s being Real such that
A5: c = |[r,s]| and
A6: G*(i,1)`1 <= r & r <= G*(i+1,1)`1 & G*(1,j)`2 <= s & s <= G*(1,j+1
)`2 by A3;
A7: r in [.G*(i,1)`1,G*(i+1,1)`1.] & s in [.G*(1,j)`2,G*(1,j+1)`2.] by A4,A1,A6
;
A8: for x being object st x in dom f holds <*r,s*>.x in f.x
proof
let x be object;
assume x in dom f;
then
A10: x = 1 or x = 2 by TARSKI:def 2;
thus thesis by A7,A10,FUNCT_4:63;
end;
dom <*r,s*> = {1,2} by FINSEQ_1:2,89;
hence thesis by A2,A5,A8,CARD_3:9;
end;
let c be object;
assume c in product f;
then consider g being Function such that
A11: c = g and
A12: dom g = dom f and
A13: for x being object st x in dom f holds g.x in f.x by CARD_3:def 5;
2 in dom f by A2,TARSKI:def 2;
then g.2 in f.2 by A13;
then g.2 in [.G*(1,j)`2,G*(1,j+1)`2.] by FUNCT_4:63;
then consider b being Real such that
A14: g.2 = b and
A15: G*(1,j)`2 <= b & b <= G*(1,j+1)`2 by A1;
1 in dom f by A2,TARSKI:def 2;
then g.1 in f.1 by A13;
then g.1 in [.G*(i,1)`1,G*(i+1,1)`1.] by FUNCT_4:63;
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 A4;
A18: for k being object st k in dom g holds g.k = <*a,b*>.k
proof
let k be object;
assume k in dom g;
then k = 1 or k = 2 by A12,TARSKI:def 2;
hence thesis by A16,A14;
end;
dom <*a,b*> = {1,2} by FINSEQ_1:2,89;
then c = |[a,b]| by A11,A12,A18,FUNCT_1:2,FUNCT_4:62;
hence thesis by A3,A17,A15;
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 Th3;
hence thesis by TOPREAL6:78;
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 that
A1: [i,j] in Indices G and
A2: [i+n,j] in Indices G;
set x = G*(i,j), y = G*(i+n,j);
per cases;
suppose
n = 0;
hence thesis by TOPREAL6:93;
end;
suppose
A3: n <> 0;
A4: i+n <= len G by A2,MATRIX_0:32;
A5: 1 <= i by A1,MATRIX_0:32;
A6: 1 <= i+n by A2,MATRIX_0:32;
A7: 1 <= j & j <= width G by A1,MATRIX_0:32;
1 <= n by A3,NAT_1:14;
then i < i+n by NAT_1:19;
then x`1 < y`1 by A4,A7,A5,GOBOARD5:3;
then
A8: x`1 - x`1 < y`1 - x`1 by XREAL_1:14;
i <= len G by A1,MATRIX_0:32;
then
A9: x`2 = G*(1,j)`2 by A7,A5,GOBOARD5:1
.= y`2 by A6,A4,A7,GOBOARD5:1;
thus dist(G*(i,j),G*(i+n,j)) = sqrt ((x`1-y`1)^2 + (x`2-y`2)^2) by
TOPREAL6:92
.= |.x`1-y`1.| by A9,COMPLEX1:72
.= |.-(x`1-y`1).| by COMPLEX1:52
.= G*(i+n,j)`1 - G*(i,j)`1 by A8,ABSVALUE:def 1;
end;
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 that
A1: [i,j] in Indices G and
A2: [i,j+n] in Indices G;
set x = G*(i,j), y = G*(i,j+n);
per cases;
suppose
n = 0;
hence thesis by TOPREAL6:93;
end;
suppose
A3: n <> 0;
A4: j+n <= width G by A2,MATRIX_0:32;
A5: 1 <= i & i <= len G by A1,MATRIX_0:32;
A6: 1 <= j+n by A2,MATRIX_0:32;
A7: 1 <= j by A1,MATRIX_0:32;
1 <= n by A3,NAT_1:14;
then j < j+n by NAT_1:19;
then x`2 < y`2 by A4,A7,A5,GOBOARD5:4;
then
A8: x`2 - x`2 < y`2 - x`2 by XREAL_1:14;
j <= width G by A1,MATRIX_0:32;
then
A9: x`1 = G*(i,1)`1 by A7,A5,GOBOARD5:2
.= y`1 by A6,A4,A5,GOBOARD5:2;
thus dist(G*(i,j),G*(i,j+n)) = sqrt ((x`1-y`1)^2 + (x`2-y`2)^2) by
TOPREAL6:92
.= |.x`2-y`2.| by A9,COMPLEX1:72
.= |.-(x`2-y`2).| by COMPLEX1:52
.= G*(i,j+n)`2 - G*(i,j)`2 by A8,ABSVALUE:def 1;
end;
end;
theorem
3 <= len Gauge(C,n)-'1
proof
set G = Gauge(C,n);
4 <= len G by JORDAN8:10;
then 4 - 1 <= len G-1 by XREAL_1:13;
hence thesis by XREAL_0:def 2;
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
A1: 0 <> 2|^i by NEWTON:83;
assume
A2: i <= j;
then
A3: 2|^(j-'i)*(2|^i) = 2|^j / 2|^i*(2|^i) by TOPREAL6:10
.= 2|^j by A1,XCMPLX_1:87;
let a, b be Nat such that
A4: 2 <= a and
A5: a <= len Gauge(C,i) - 1 and
A6: 2 <= b and
A7: b <= len Gauge(C,i) - 1;
A8: 1 <= a & 1 <= b by A4,A6,XXREAL_0:2;
set c = 2 + 2|^(j-'i)*(a-'2), d = 2 + 2|^(j-'i)*(b-'2);
A9: 0 <= b-2 by A6,XREAL_1:48;
set n = N-bound C, e = E-bound C, s = S-bound C, w = W-bound C;
A10: 0 <> 2|^j by NEWTON:83;
A11: (n-s)/(2|^j)*(d-2) = (n-s)/(2|^j)*((2|^j/2|^i)*(b-'2)) by A2,TOPREAL6:10
.= (n-s)/(2|^j)*(2|^j/2|^i)*(b-'2)
.= (n-s)/((2|^j)/(2|^j/2|^i))*(b-'2) by XCMPLX_1:81
.= (n-s)/(2|^i)*(b-'2) by A10,XCMPLX_1:52
.= (n-s)/(2|^i)*(b-2) by A9,XREAL_0:def 2;
take c, d;
A12: 2+0 <= 2+2|^(j-'i)*(a-'2) by XREAL_1:6;
then
A13: 1 <= c by XXREAL_0:2;
2|^i + 2 - 2 >= 0;
then
A14: 2|^i + 2 -' 2 = 2|^i + 0 by XREAL_0:def 2;
A15: 0 <= a-2 by A4,XREAL_1:48;
A16: (e-w)/(2|^j)*(c-2) = (e-w)/(2|^j)*((2|^j/2|^i)*(a-'2)) by A2,TOPREAL6:10
.= (e-w)/(2|^j)*(2|^j/2|^i)*(a-'2)
.= (e-w)/((2|^j)/(2|^j/2|^i))*(a-'2) by XCMPLX_1:81
.= (e-w)/(2|^i)*(a-'2) by A10,XCMPLX_1:52
.= (e-w)/(2|^i)*(a-2) by A15,XREAL_0:def 2;
A17: len Gauge(C,j) - 1 < len Gauge(C,j) - 0 by XREAL_1:15;
A18: len Gauge(C,i) - 1 = 2|^i + 3 - 1 by JORDAN8:def 1
.= 2|^i + 2;
then a -' 2 <= 2|^i + 2 -' 2 by A5,NAT_D:42;
then
A19: 2|^(j-'i)*(a-'2) <= 2|^j by A14,A3,XREAL_1:64;
b -' 2 <= 2|^i + 2 -' 2 by A7,A18,NAT_D:42;
then
A20: 2|^(j-'i)*(b-'2) <= 2|^j by A14,A3,XREAL_1:64;
A21: len Gauge(C,i) - 1 < len Gauge(C,i) - 0 by XREAL_1:15;
then
A22: a <= len Gauge(C,i) by A5,XXREAL_0:2;
len Gauge(C,j) - 1 = 2|^j + 3 - 1 by JORDAN8:def 1
.= 2|^j + 2;
hence
A23: 2 <= c & c <= len Gauge(C,j) - 1 & 2 <= d & d <= len Gauge(C,j ) -
1 by A19,A20,A12,XREAL_1:6;
then
A24: 1 <= d by XXREAL_0:2;
width Gauge(C,j) = len Gauge(C,j) by JORDAN8:def 1;
then
A25: d <= width Gauge(C,j) by A23,A17,XXREAL_0:2;
c <= len Gauge(C,j) by A23,A17,XXREAL_0:2;
hence [c,d] in Indices Gauge(C,j) by A13,A24,A25,MATRIX_0:30;
then
A26: Gauge(C,j)*(c,d) = |[w+(e-w)/(2|^j)*(c-2), s+(n-s)/(2|^j)*(d-2)]| by
JORDAN8:def 1;
width Gauge(C,i) = len Gauge(C,i) by JORDAN8:def 1;
then b <= width Gauge(C,i) by A7,A21,XXREAL_0:2;
then [a,b] in Indices Gauge(C,i) by A22,A8,MATRIX_0:30;
then
A27: Gauge(C,i)*(a,b) = |[w+(e-w)/(2|^i)*(a-2), s+(n-s)/(2|^i)*(b-2)]| by
JORDAN8:def 1;
then
A28: Gauge(C,i)*(a,b)`2 = s+(n-s)/(2|^i)*(b-2)
.= Gauge(C,j)*(c,d)`2 by A26,A11;
Gauge(C,i)*(a,b)`1 = w+(e-w)/(2|^i)*(a-2) by A27
.= Gauge(C,j)*(c,d)`1 by A26,A16;
hence Gauge(C,i)*(a,b) = Gauge(C,j)*(c,d) by A28,TOPREAL3:6;
thus thesis;
end;
theorem Th9:
[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;
A3: p2 = |[w+(e-w)/(2|^n)*(i-2), s+(a-s)/(2|^n)*(j+1-2)]| by A2,JORDAN8:def 1;
a >= s by SPRECT_1:22;
then
A4: a - s >= s - s by XREAL_1:9;
set x = (a-s)/(2|^n);
consider p, q being Point of Euclid 2 such that
A5: p = p1 & q = p2 and
A6: dist(p1,p2) = dist(p,q) by TOPREAL6:def 1;
A7: p1 = |[w+(e-w)/(2|^n)*(i-2), s+(a-s)/(2|^n)*(j-2)]| by A1,JORDAN8:def 1;
dist(p,q) = (Pitag_dist 2).(p,q) by METRIC_1:def 1
.= sqrt ((p1`1 - p2`1)^2 + (p1`2 - p2`2)^2) by A5,TOPREAL3:7
.= sqrt ((w+(e-w)/(2|^n)*(i-2) - p2`1)^2 + (p1`2 - p2`2)^2) by A7
.= sqrt ((w+(e-w)/(2|^n)*(i-2) - (w+(e-w)/(2|^n)*(i-2)))^2 + (p1`2 - p2
`2)^2) by A3
.= |.p1`2 - p2`2.| by COMPLEX1:72
.= |.s+x*(j-2) - p2`2.| by A7
.= |.s+x*(j-2) - (s+x*(j+1-2)).| by A3
.= |.-x.|
.= |.x.| by COMPLEX1:52
.= |.a-s.|/|.2|^n.| by COMPLEX1:67
.= (a-s)/|.2|^n.| by A4,ABSVALUE:def 1;
hence thesis by A6,ABSVALUE:def 1;
end;
theorem Th10:
[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;
A3: p2 = |[w+(e-w)/(2|^n)*(i+1-2), s+(a-s)/(2|^n)*(j-2)]| by A2,JORDAN8:def 1;
e >= w by SPRECT_1:21;
then
A4: e - w >= w - w by XREAL_1:9;
set x = (e-w)/(2|^n);
consider p, q being Point of Euclid 2 such that
A5: p = p1 & q = p2 and
A6: dist(p1,p2) = dist(p,q) by TOPREAL6:def 1;
A7: p1 = |[w+(e-w)/(2|^n)*(i-2), s+(a-s)/(2|^n)*(j-2)]| by A1,JORDAN8:def 1;
dist(p,q) = (Pitag_dist 2).(p,q) by METRIC_1:def 1
.= sqrt ((p1`1 - p2`1)^2 + (p1`2 - p2`2)^2) by A5,TOPREAL3:7
.= sqrt ((p1`1 - p2`1)^2 + (s+(a-s)/(2|^n)*(j-2) - p2`2)^2) by A7
.= sqrt ((p1`1 - p2`1)^2 + (s+(a-s)/(2|^n)*(j-2) - (s+(a-s)/(2|^n)*(j-2)
))^2) by A3
.= |.p1`1 - p2`1.| by COMPLEX1:72
.= |.w+x*(i-2) - p2`1.| by A7
.= |.w+x*(i-2) - (w+x*(i+1-2)).| by A3
.= |.-x.|
.= |.x.| by COMPLEX1:52
.= |.e-w.|/|.2|^n.| by COMPLEX1:67
.= (e-w)/|.2|^n.| by A4,ABSVALUE:def 1;
hence thesis by A6,ABSVALUE:def 1;
end;
theorem
for r, t being Real 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;
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 = |.[\ log(2,(n-s)/r) /].| + 1, b = |.[\ log(2,(e-w)/t) /].| + 1;
take i = max(a,b)+1;
A3: 2 to_power i > 0 by POWER:34;
then
A4: 2|^i > 0 by POWER:41;
[\ log(2,(n-s)/r) /] <= |.[\ log(2,(n-s)/r) /].| by ABSVALUE:4;
then
A5: [\ log(2,(n-s)/r) /] + 1 <= a by XREAL_1:6;
[\ log(2,(n-s)/r) /] > log(2,(n-s)/r) - 1 by INT_1:def 6;
then [\ log(2,(n-s)/r) /] + 1 > log(2,(n-s)/r) - 1 + 1 by XREAL_1:6;
then
A6: a > log(2,(n-s)/r) - 1 + 1 by A5,XXREAL_0:2;
a <= max(a,b) by XXREAL_0:25;
then
A7: a+1 <= max(a,b)+1 by XREAL_1:6;
a < a+1 by XREAL_1:29;
then i > a by A7,XXREAL_0:2;
then i > log(2,(n-s)/r) by A6,XXREAL_0:2;
then log(2,2 to_power i) > log(2,(n-s)/r) by A3,POWER:def 3;
then 2 to_power i > (n-s)/r by A3,PRE_FF:10;
then 2|^i > (n-s)/r by POWER:41;
then 2|^i * r > (n-s)/r * r by A1,XREAL_1:68;
then 2|^i * r > n-s by A1,XCMPLX_1:87;
then 2|^i * r / 2|^i > (n-s) / 2|^i by A4,XREAL_1:74;
then
A8: (n-s)/2|^i < r by A4,XCMPLX_1:89;
a >= 0+1 & max(a,b) >= a by XREAL_1:7,XXREAL_0:25;
then max(a,b) >= 1 by XXREAL_0:2;
then max(a,b)+1 >= 1+1 by XREAL_1:7;
hence 1 < i by XXREAL_0:2;
A9: len Gauge(C,i) >= 4 by JORDAN8:10;
then
A10: 1 <= len Gauge(C,i) by XXREAL_0:2;
[\ log(2,(e-w)/t) /] <= |.[\ log(2,(e-w)/t) /].| by ABSVALUE:4;
then
A11: [\ log(2,(e-w)/t) /] + 1 <= b by XREAL_1:6;
[\ log(2,(e-w)/t) /] > log(2,(e-w)/t) - 1 by INT_1:def 6;
then [\ log(2,(e-w)/t) /] + 1 > log(2,(e-w)/t) - 1 + 1 by XREAL_1:6;
then
A12: b > log(2,(e-w)/t) - 1 + 1 by A11,XXREAL_0:2;
b <= max(a,b) by XXREAL_0:25;
then
A13: b+1 <= max(a,b)+1 by XREAL_1:6;
b < b+1 by XREAL_1:29;
then i > b by A13,XXREAL_0:2;
then i > log(2,(e-w)/t) by A12,XXREAL_0:2;
then log(2,2 to_power i) > log(2,(e-w)/t) by A3,POWER:def 3;
then 2 to_power i > (e-w)/t by A3,PRE_FF:10;
then 2|^i > (e-w)/t by POWER:41;
then 2|^i * t > (e-w)/t * t by A2,XREAL_1:68;
then 2|^i * t > e-w by A2,XCMPLX_1:87;
then 2|^i * t / 2|^i > (e-w) / 2|^i by A4,XREAL_1:74;
then
A14: (e-w)/2|^i < t by A4,XCMPLX_1:89;
A15: len Gauge(C,i) = width Gauge(C,i) by JORDAN8:def 1;
then
A16: [1,1] in Indices Gauge(C,i) by A10,MATRIX_0:30;
A17: 1+1 <= width Gauge(C,i) by A15,A9,XXREAL_0:2;
then
A18: [1,1+1] in Indices Gauge(C,i) by A10,MATRIX_0:30;
[1+1,1] in Indices Gauge(C,i) by A15,A10,A17,MATRIX_0:30;
hence thesis by A8,A14,A16,A18,Th9,Th10;
end;
begin :: LeftComp and RightComp
theorem Th12:
for P being Subset of (TOP-REAL 2)|(L~f)` st P is a_component
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 and
A2: P <> RightComp f;
P <> {}((TOP-REAL 2)|(L~f)`) by A1,CONNSP_1:32;
then consider a being Point of (TOP-REAL 2)|(L~f)` such that
A3: a in P by SUBSET_1:4;
the carrier of (TOP-REAL 2)|(L~f)` = (L~f)` & (L~f)` = LeftComp f \/
RightComp f by GOBRD12:10,PRE_TOPC:8;
then
A4: a in LeftComp f or a in RightComp f by XBOOLE_0:def 3;
LeftComp f is_a_component_of (L~f)` by GOBOARD9:def 1;
then
A5: ex L being Subset of (TOP-REAL 2)|(L~f)` st L = LeftComp f & L
is a_component 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
A6: R = RightComp f and
A7: R is a_component by CONNSP_1:def 6;
P misses R by A1,A2,A6,A7,CONNSP_1:35;
then P meets LeftComp f by A6,A3,A4,XBOOLE_0:3;
hence thesis by A1,A5,CONNSP_1:35;
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 & C2 is a_component
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 & C2 is a_component;
the carrier of (TOP-REAL 2)|(L~f)` = (L~f)` by PRE_TOPC:8;
then reconsider C1 = A1, C2 = A2 as Subset of (TOP-REAL 2)|(L~f)` by A1,
XBOOLE_1:7;
C1 = A1;
then C2 is a_component by A3;
then
A4: C2 = RightComp f or C2 = LeftComp f by Th12;
C2 = A2;
then C1 is a_component by A3;
then
A5: C1 = RightComp f or C1 = LeftComp f by Th12;
assume not thesis;
hence contradiction by A2,A5,A4;
end;
theorem Th14:
LeftComp f misses RightComp f
proof
assume LeftComp f /\ RightComp f <> {};
then consider x being object such that
A1: x in LeftComp f /\ RightComp f by XBOOLE_0:def 1;
now
take x;
thus x in LeftComp f & x in RightComp f by A1,XBOOLE_0:def 4;
end;
then
A2: LeftComp f meets RightComp f by XBOOLE_0:3;
LeftComp f is_a_component_of (L~f)` & RightComp f is_a_component_of (L~f
) ` by GOBOARD9:def 1,def 2;
hence thesis by A2,GOBOARD9:1,SPRECT_4:6;
end;
theorem Th15:
L~f \/ RightComp f \/ LeftComp f = the carrier of TOP-REAL 2
proof
A1: (L~f)` \/ L~f = [#]the carrier of TOP-REAL 2 by SUBSET_1:10
.= the carrier of TOP-REAL 2;
(L~f)` = RightComp f \/ LeftComp f by GOBRD12:10;
hence thesis by A1,XBOOLE_1:4;
end;
theorem Th16:
p in L~f iff not p in LeftComp f & not p in RightComp f
proof
A1: p in L~f iff not p in (L~f)` by XBOOLE_0:def 5;
(L~f)` = LeftComp f \/ RightComp f by GOBRD12:10;
hence thesis by A1,XBOOLE_0:def 3;
end;
theorem Th17:
p in LeftComp f iff not p in L~f & not p in RightComp f
proof
LeftComp f misses RightComp f by Th14;
then
A1: (L~f)` = LeftComp f \/ RightComp f & LeftComp f /\ RightComp f = {} by
GOBRD12:10;
p in L~f iff not p in (L~f)` by XBOOLE_0:def 5;
hence thesis by A1,XBOOLE_0:def 3,def 4;
end;
theorem
p in RightComp f iff not p in L~f & not p in LeftComp f by Th16,Th17;
theorem Th19:
L~f = (Cl RightComp f) \ RightComp f
proof
thus L~f c= (Cl RightComp f) \ RightComp f
proof
let x be object;
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
left_cell(f,i) /\ right_cell(f,i) = LSeg(f,i) by A2,GOBOARD5:31;
then LSeg(f,i) c= right_cell(f,i) by XBOOLE_1:17;
then
A4: 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
A5: [i1,j1] in Indices GoB f and
A6: f/.i = GoB f*(i1,j1) and
A7: [i2,j2] in Indices GoB f and
A8: f/.(i+1) = GoB f*(i2,j2) and
A9: 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:3;
A10: 1 <= i1 by A5,MATRIX_0:32;
A11: j2 <= width GoB f by A7,MATRIX_0:32;
A12: 1 <= j1 by A5,MATRIX_0:32;
A13: j1 <= width GoB f by A5,MATRIX_0:32;
A14: i1 <= len GoB f by A5,MATRIX_0:32;
A15: i2 <= len GoB f by A7,MATRIX_0:32;
A16: now
per cases by A9;
case
A17: i1 = i2 & j1+1 = j2;
set w = i1-'1;
A18: w+1 = i1 by A10,XREAL_1:235;
then right_cell(f,i) = cell(GoB f,w+1,j1) by A2,A5,A6,A7,A8,A17,
GOBOARD5:27;
hence p in Cl Int right_cell(f,i) by A4,A14,A13,A18,GOBRD11:35;
end;
case
A19: i1+1 = i2 & j1 = j2;
set w = j1-'1;
w <= w+1 & w+1 <= width GoB f by A12,A13,NAT_1:11,XREAL_1:235;
then
A20: w <= width GoB f by XXREAL_0:2;
w+1 = j1 by A12,XREAL_1:235;
then right_cell(f,i) = cell(GoB f,i1,w) by A2,A5,A6,A7,A8,A19,
GOBOARD5:28;
hence p in Cl Int right_cell(f,i) by A4,A14,A20,GOBRD11:35;
end;
case
A21: i1 = i2+1 & j1 = j2;
set w = j1-'1;
A22: w+1 = j1 by A12,XREAL_1:235;
then right_cell(f,i) = cell(GoB f,i2,w+1) by A2,A5,A6,A7,A8,A21,
GOBOARD5:29;
hence p in Cl Int right_cell(f,i) by A4,A13,A15,A22,GOBRD11:35;
end;
case
A23: i1 = i2 & j1 = j2+1;
set z = i1-'1;
z <= z+1 & z+1 <= len GoB f by A10,A14,NAT_1:11,XREAL_1:235;
then
A24: z <= len GoB f by XXREAL_0:2;
z+1 = i1 by A10,XREAL_1:235;
then right_cell(f,i) = cell(GoB f,z,j2) by A2,A5,A6,A7,A8,A23,
GOBOARD5:30;
hence p in Cl Int right_cell(f,i) by A4,A11,A24,GOBRD11:35;
end;
end;
let O be Subset of TOP-REAL 2;
assume O is open & p in O;
then O meets Int right_cell(f,i) by A16,PRE_TOPC:def 7;
hence thesis by A2,GOBOARD9:25,XBOOLE_1:63;
end;
then
A25: p in Cl RightComp f by PRE_TOPC:def 7;
not x in RightComp f by A1,Th16;
hence thesis by A25,XBOOLE_0:def 5;
end;
assume not (Cl RightComp f) \ RightComp f c= L~f;
then consider q being object such that
A26: q in (Cl RightComp f) \ RightComp f and
A27: not q in L~f;
reconsider q as Point of TOP-REAL 2 by A26;
not q in RightComp f by A26,XBOOLE_0:def 5;
then
A28: q in LeftComp f by A27,Th16;
q in Cl RightComp f by A26,XBOOLE_0:def 5;
then LeftComp f meets RightComp f by A28,PRE_TOPC:def 7;
hence contradiction by Th14;
end;
theorem Th20:
L~f = (Cl LeftComp f) \ LeftComp f
proof
thus L~f c= (Cl LeftComp f) \ LeftComp f
proof
let x be object;
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
left_cell(f,i) /\ right_cell(f,i) = LSeg(f,i) by A2,GOBOARD5:31;
then LSeg(f,i) c= left_cell(f,i) by XBOOLE_1:17;
then
A4: 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
A5: [i1,j1] in Indices GoB f and
A6: f/.i = GoB f*(i1,j1) and
A7: [i2,j2] in Indices GoB f and
A8: f/.(i+1) = GoB f*(i2,j2) and
A9: 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:3;
A10: 1 <= i1 by A5,MATRIX_0:32;
A11: j2 <= width GoB f by A7,MATRIX_0:32;
A12: 1 <= j1 by A5,MATRIX_0:32;
A13: j1 <= width GoB f by A5,MATRIX_0:32;
A14: i1 <= len GoB f by A5,MATRIX_0:32;
A15: i2 <= len GoB f by A7,MATRIX_0:32;
A16: now
per cases by A9;
case
A17: i1 = i2 & j1+1 = j2;
set w = i1-'1;
w <= w+1 & w+1 <= len GoB f by A10,A14,NAT_1:11,XREAL_1:235;
then
A18: w <= len GoB f by XXREAL_0:2;
w+1 = i1 by A10,XREAL_1:235;
then left_cell(f,i) = cell(GoB f,w,j1) by A2,A5,A6,A7,A8,A17,
GOBOARD5:27;
hence p in Cl Int left_cell(f,i) by A4,A13,A18,GOBRD11:35;
end;
case
A19: i1+1 = i2 & j1 = j2;
set w = j1-'1;
w+1 = j1 by A12,XREAL_1:235;
then
A20: left_cell(f,i) = cell(GoB f,i1,w+1) by A2,A5,A6,A7,A8,A19,GOBOARD5:28
;
w+1 <= width GoB f by A12,A13,XREAL_1:235;
hence p in Cl Int left_cell(f,i) by A4,A14,A20,GOBRD11:35;
end;
case
A21: i1 = i2+1 & j1 = j2;
set w = j1-'1;
w <= w+1 & w+1 <= width GoB f by A12,A13,NAT_1:11,XREAL_1:235;
then
A22: w <= width GoB f by XXREAL_0:2;
w+1 = j1 by A12,XREAL_1:235;
then left_cell(f,i) = cell(GoB f,i2,w) by A2,A5,A6,A7,A8,A21,
GOBOARD5:29;
hence p in Cl Int left_cell(f,i) by A4,A15,A22,GOBRD11:35;
end;
case
A23: i1 = i2 & j1 = j2+1;
set z = i1-'1;
z+1 = i1 by A10,XREAL_1:235;
then
A24: left_cell(f,i) = cell(GoB f,z+1,j2) by A2,A5,A6,A7,A8,A23,GOBOARD5:30
;
z+1 <= len GoB f by A10,A14,XREAL_1:235;
hence p in Cl Int left_cell(f,i) by A4,A11,A24,GOBRD11:35;
end;
end;
let O be Subset of TOP-REAL 2;
assume O is open & p in O;
then O meets Int left_cell(f,i) by A16,PRE_TOPC:def 7;
hence thesis by A2,GOBOARD9:21,XBOOLE_1:63;
end;
then
A25: p in Cl LeftComp f by PRE_TOPC:def 7;
not x in LeftComp f by A1,Th16;
hence thesis by A25,XBOOLE_0:def 5;
end;
assume not (Cl LeftComp f) \ LeftComp f c= L~f;
then consider q being object such that
A26: q in (Cl LeftComp f) \ LeftComp f and
A27: not q in L~f;
reconsider q as Point of TOP-REAL 2 by A26;
not q in LeftComp f by A26,XBOOLE_0:def 5;
then
A28: q in RightComp f by A27,Th16;
q in Cl LeftComp f by A26,XBOOLE_0:def 5;
then RightComp f meets LeftComp f by A28,PRE_TOPC:def 7;
hence contradiction by Th14;
end;
theorem Th21:
Cl RightComp f = (RightComp f) \/ L~f
proof
thus Cl RightComp f c= RightComp f \/ L~f
proof
let x be object;
assume
A1: x in Cl RightComp f;
now
A2: now
assume x in LeftComp f;
then LeftComp f meets RightComp f by A1,TOPS_1:12;
hence contradiction by Th14;
end;
assume not x in RightComp f;
hence x in L~f by A1,A2,Th16;
end;
hence thesis by XBOOLE_0:def 3;
end;
(Cl RightComp f) \ RightComp f c= Cl RightComp f by XBOOLE_1:36;
then RightComp f c= Cl RightComp f & L~f c= Cl RightComp f by Th19,
PRE_TOPC:18;
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 object;
assume
A1: x in Cl LeftComp f;
now
A2: not x in RightComp f by A1,Th14,TOPS_1:12;
assume not x in LeftComp f;
hence x in L~f by A1,A2,Th16;
end;
hence thesis by XBOOLE_0:def 3;
end;
(Cl LeftComp f) \ LeftComp f c= Cl LeftComp f by XBOOLE_1:36;
then LeftComp f c= Cl LeftComp f & L~f c= Cl LeftComp f by Th20,PRE_TOPC:18;
hence thesis by XBOOLE_1:8;
end;
registration
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:10;
L~f = (Cl A1) \ A1 by Th19;
hence thesis by Th14,Th20,GOBOARD9:def 1,def 2;
end;
end;
reserve f for clockwise_oriented non constant standard
special_circular_sequence;
theorem Th23:
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;
reconsider u = p as Point of Euclid 2 by EUCLID:22;
assume p in RightComp f;
then p in RightComp g by REVROT_1:37;
then u in Int RightComp g by TOPS_1:23;
then consider r being Real such that
A2: r > 0 and
A3: Ball(u,r) c= RightComp g by GOBOARD6:5;
reconsider r as Real;
reconsider k = |[p`1-r/2,p`2]| as Point of Euclid 2 by EUCLID:22;
dist(u,k) = (Pitag_dist 2).(u,k) by 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:7
.= sqrt ((p`1 - (p`1-r/2))^2 + (p`2 - |[p`1-r/2,p`2]|`2)^2)
.= sqrt ((p`1 - (p`1-r/2))^2 + (p`2 - p`2)^2)
.= r/2 by A2,SQUARE_1:22;
then dist(u,k) < r/1 by A2,XREAL_1:76;
then
A4: k in Ball(u,r) by METRIC_1:11;
RightComp g misses LeftComp g by Th14;
then
A5: not |[p`1-r/2,p`2]| in LeftComp g by A3,A4,XBOOLE_0:3;
set x = |[p`1-r/2,N-bound L~SpStSeq L~g]|;
A6: LSeg(NW-corner L~g,NE-corner L~g) c= L~SpStSeq L~g by SPRECT_3:14;
A7: proj1.x = x`1 by PSCOMP_1:def 5
.= p`1-r/2;
N-min L~f in rng f by SPRECT_2:39;
then
A8: g/.1 = N-min L~g by A1,FINSEQ_6:92;
then |[p`1-r/2,p`2]|`1 <= E-bound L~g by A5,JORDAN2C:111;
then p`1-r/2 <= E-bound L~g;
then
A9: x`1 <= E-bound L~g;
A10: x`2 = N-bound L~g by SPRECT_1:60;
|[p`1-r/2,p`2]|`1 >= W-bound L~g by A8,A5,JORDAN2C:110;
then p`1-r/2 >= W-bound L~g;
then
A11: x`1 >= W-bound L~g;
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:25;
then x in LSeg(NW-corner L~g,NE-corner L~g) by A9,A11,A10;
then
proj1.:L~SpStSeq L~g is bounded_below & p`1-r/2 in proj1.:L~SpStSeq L~g
by A6,A7,FUNCT_2:35;
then
A12: lower_bound(proj1.:L~SpStSeq L~g) <= p`1-r/2 by SEQ_4:def 2;
r/2 > 0 by A2,XREAL_1:139;
then
A13: p`1-r/2 < p`1-0 by XREAL_1:15;
W-bound L~SpStSeq L~g = W-bound L~g & W-bound L~SpStSeq L~g =
lower_bound( proj1.:L~SpStSeq L~g) by SPRECT_1:43,58;
hence thesis by A1,A12,A13,XXREAL_0:2;
end;
theorem Th24:
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;
reconsider u = p as Point of Euclid 2 by EUCLID:22;
assume p in RightComp f;
then p in RightComp g by REVROT_1:37;
then u in Int RightComp g by TOPS_1:23;
then consider r being Real such that
A2: r > 0 and
A3: Ball(u,r) c= RightComp g by GOBOARD6:5;
reconsider r as Real;
reconsider k = |[p`1+r/2,p`2]| as Point of Euclid 2 by EUCLID:22;
dist(u,k) = (Pitag_dist 2).(u,k) by 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:7
.= sqrt ((p`1 - (p`1+r/2))^2 + (p`2 - |[p`1+r/2,p`2]|`2)^2)
.= sqrt ((p`1 - (p`1+r/2))^2 + (p`2 - p`2)^2)
.= sqrt ((r/2)^2)
.= r/2 by A2,SQUARE_1:22;
then dist(u,k) < r/1 by A2,XREAL_1:76;
then
A4: k in Ball(u,r) by METRIC_1:11;
RightComp g misses LeftComp g by Th14;
then
A5: not |[p`1+r/2,p`2]| in LeftComp g by A3,A4,XBOOLE_0:3;
set x = |[p`1+r/2,N-bound L~SpStSeq L~g]|;
A6: LSeg(NW-corner L~g,NE-corner L~g) c= L~SpStSeq L~g by SPRECT_3:14;
A7: proj1.x = x`1 by PSCOMP_1:def 5
.= p`1+r/2;
N-min L~f in rng f by SPRECT_2:39;
then
A8: g/.1 = N-min L~g by A1,FINSEQ_6:92;
then |[p`1+r/2,p`2]|`1 <= E-bound L~g by A5,JORDAN2C:111;
then p`1+r/2 <= E-bound L~g;
then
A9: x`1 <= E-bound L~g;
A10: x`2 = N-bound L~g by SPRECT_1:60;
|[p`1+r/2,p`2]|`1 >= W-bound L~g by A8,A5,JORDAN2C:110;
then p`1+r/2 >= W-bound L~g;
then
A11: x`1 >= W-bound L~g;
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:25;
then x in LSeg(NW-corner L~g,NE-corner L~g) by A9,A11,A10;
then
proj1.:L~SpStSeq L~g is bounded_above & p`1+r/2 in proj1.:L~SpStSeq L~g
by A6,A7,FUNCT_2:35;
then
A12: upper_bound(proj1.:L~SpStSeq L~g) >= p`1+r/2 by SEQ_4:def 1;
r/2 > 0 by A2,XREAL_1:139;
then
A13: p`1+r/2 > p`1+0 by XREAL_1:6;
E-bound L~SpStSeq L~g = E-bound L~g &
E-bound L~SpStSeq L~g = upper_bound(proj1
.:L~ SpStSeq L~g) by SPRECT_1:46,61;
hence thesis by A1,A12,A13,XXREAL_0:2;
end;
theorem Th25:
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;
reconsider u = p as Point of Euclid 2 by EUCLID:22;
assume p in RightComp f;
then p in RightComp g by REVROT_1:37;
then u in Int RightComp g by TOPS_1:23;
then consider r being Real such that
A2: r > 0 and
A3: Ball(u,r) c= RightComp g by GOBOARD6:5;
reconsider r as Real;
reconsider k = |[p`1,p`2+r/2]| as Point of Euclid 2 by EUCLID:22;
dist(u,k) = (Pitag_dist 2).(u,k) by 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:7
.= sqrt ((p`1 - p`1)^2 + (p`2 - |[p`1,p`2+r/2]|`2)^2)
.= sqrt ((p`2 - (p`2+r/2))^2)
.= sqrt ((r/2)^2)
.= r/2 by A2,SQUARE_1:22;
then dist(u,k) < r/1 by A2,XREAL_1:76;
then
A4: k in Ball(u,r) by METRIC_1:11;
RightComp g misses LeftComp g by Th14;
then
A5: not |[p`1,p`2+r/2]| in LeftComp g by A3,A4,XBOOLE_0:3;
set x = |[E-bound L~SpStSeq L~g,p`2+r/2]|;
A6: LSeg(SE-corner L~g,NE-corner L~g) c= L~SpStSeq L~g by TOPREAL6:35;
A7: proj2.x = x`2 by PSCOMP_1:def 6
.= p`2+r/2;
N-min L~f in rng f by SPRECT_2:39;
then
A8: g/.1 = N-min L~g by A1,FINSEQ_6:92;
then |[p`1,p`2+r/2]|`2 <= N-bound L~g by A5,JORDAN2C:113;
then p`2+r/2 <= N-bound L~g;
then
A9: x`2 <= N-bound L~g;
A10: x`1 = E-bound L~g by SPRECT_1:61;
|[p`1,p`2+r/2]|`2 >= S-bound L~g by A8,A5,JORDAN2C:112;
then p`2+r/2 >= S-bound L~g;
then
A11: x`2 >= S-bound L~g;
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:23;
then x in LSeg(SE-corner L~g,NE-corner L~g) by A9,A11,A10;
then
proj2.:L~SpStSeq L~g is bounded_above & p`2+r/2 in proj2.:L~SpStSeq L~g
by A6,A7,FUNCT_2:35;
then
A12: upper_bound(proj2.:L~SpStSeq L~g) >= p`2+r/2 by SEQ_4:def 1;
r/2 > 0 by A2,XREAL_1:139;
then
A13: p`2+r/2 > p`2+0 by XREAL_1:6;
N-bound L~SpStSeq L~g = N-bound L~g &
N-bound L~SpStSeq L~g = upper_bound(proj2
.:L~ SpStSeq L~g) by SPRECT_1:45,60;
hence thesis by A1,A12,A13,XXREAL_0:2;
end;
theorem Th26:
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;
reconsider u = p as Point of Euclid 2 by EUCLID:22;
assume p in RightComp f;
then p in RightComp g by REVROT_1:37;
then u in Int RightComp g by TOPS_1:23;
then consider r being Real such that
A2: r > 0 and
A3: Ball(u,r) c= RightComp g by GOBOARD6:5;
reconsider r as Real;
reconsider k = |[p`1,p`2-r/2]| as Point of Euclid 2 by EUCLID:22;
dist(u,k) = (Pitag_dist 2).(u,k) by 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:7
.= sqrt ((p`1 - p`1)^2 + (p`2 - |[p`1,p`2-r/2]|`2)^2)
.= sqrt ((p`2 - (p`2-r/2))^2)
.= r/2 by A2,SQUARE_1:22;
then dist(u,k) < r/1 by A2,XREAL_1:76;
then
A4: k in Ball(u,r) by METRIC_1:11;
RightComp g misses LeftComp g by Th14;
then
A5: not |[p`1,p`2-r/2]| in LeftComp g by A3,A4,XBOOLE_0:3;
set x = |[E-bound L~SpStSeq L~g,p`2-r/2]|;
A6: LSeg(SE-corner L~g,NE-corner L~g) c= L~SpStSeq L~g by TOPREAL6:35;
A7: proj2.x = x`2 by PSCOMP_1:def 6
.= p`2-r/2;
N-min L~f in rng f by SPRECT_2:39;
then
A8: g/.1 = N-min L~g by A1,FINSEQ_6:92;
then |[p`1,p`2-r/2]|`2 <= N-bound L~g by A5,JORDAN2C:113;
then p`2-r/2 <= N-bound L~g;
then
A9: x`2 <= N-bound L~g;
A10: x`1 = E-bound L~g by SPRECT_1:61;
|[p`1,p`2-r/2]|`2 >= S-bound L~g by A8,A5,JORDAN2C:112;
then p`2-r/2 >= S-bound L~g;
then
A11: x`2 >= S-bound L~g;
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:23;
then x in LSeg(SE-corner L~g,NE-corner L~g) by A9,A11,A10;
then
proj2.:L~SpStSeq L~g is bounded_below & p`2-r/2 in proj2.:L~SpStSeq L~g
by A6,A7,FUNCT_2:35;
then
A12: lower_bound(proj2.:L~SpStSeq L~g) <= p`2-r/2 by SEQ_4:def 2;
r/2 > 0 by A2,XREAL_1:139;
then
A13: p`2-r/2 < p`2-0 by XREAL_1:15;
S-bound L~SpStSeq L~g = S-bound L~g & S-bound L~SpStSeq L~g =
lower_bound( proj2.:L~SpStSeq L~g) by SPRECT_1:44,59;
hence thesis by A1,A12,A13,XXREAL_0:2;
end;
theorem Th27:
p in RightComp f & q in LeftComp f implies LSeg(p,q) meets L~f
proof
assume that
A1: p in RightComp f and
A2: q in LeftComp f;
assume LSeg(p,q) misses L~f;
then LSeg(p,q) c= (L~f)` by TDLAT_1:2;
then reconsider A = LSeg(p,q) as Subset of (TOP-REAL 2)|(L~f)` by PRE_TOPC:8;
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 and
A4: L is a_component by CONNSP_1:def 6;
q in A by RLTOPSP1:68;
then
A5: L meets A by A2,A3,XBOOLE_0:3;
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
A6: R = RightComp f and
A7: R is a_component by CONNSP_1:def 6;
p in A by RLTOPSP1:68;
then A is connected & R meets A by A1,A6,CONNSP_1:23,XBOOLE_0:3;
hence contradiction by A6,A7,A3,A4,A5,JORDAN2C:92,SPRECT_4:6;
end;
theorem Th28:
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: dom g = {1,2} by FUNCT_4:62;
A2: Cl RightComp SpStSeq C = (RightComp SpStSeq C) \/ L~SpStSeq C by Th21;
hereby
let a be object;
assume
A3: a in Cl RightComp SpStSeq C;
then reconsider b = a as Point of TOP-REAL 2;
reconsider h = a as FinSequence by A3;
A4: for x being object st x in {1,2} holds h.x in g.x
proof
let x be object such that
A5: x in {1,2};
per cases by A5,TARSKI:def 2;
suppose
A6: x = 1;
then
A7: g.x = [.W-bound L~SpStSeq C,E-bound L~SpStSeq C.] by FUNCT_4:63;
now
per cases by A2,A3,XBOOLE_0:def 3;
case
a in RightComp SpStSeq C;
then W-bound L~SpStSeq C < b`1 & E-bound L~SpStSeq C > b`1 by Th23
,Th24;
hence thesis by A6,A7,XXREAL_1:1;
end;
case
a in L~SpStSeq C;
then W-bound L~SpStSeq C <= b`1 & b`1 <= E-bound L~SpStSeq C by
PSCOMP_1:24;
hence thesis by A6,A7,XXREAL_1:1;
end;
end;
hence thesis;
end;
suppose
A8: x = 2;
then
A9: g.x = [.S-bound L~SpStSeq C,N-bound L~SpStSeq C.] by FUNCT_4:63;
now
per cases by A2,A3,XBOOLE_0:def 3;
case
a in RightComp SpStSeq C;
then S-bound L~SpStSeq C < b`2 & N-bound L~SpStSeq C > b`2 by Th25
,Th26;
hence thesis by A8,A9,XXREAL_1:1;
end;
case
a in L~SpStSeq C;
then S-bound L~SpStSeq C <= b`2 & b`2 <= N-bound L~SpStSeq C by
PSCOMP_1:24;
hence thesis by A8,A9,XXREAL_1:1;
end;
end;
hence thesis;
end;
end;
a is Tuple of 2,REAL by A3,Lm1,FINSEQ_2:131;
then ex r, s being Element of REAL st a = <*r,s*> by FINSEQ_2:100;
then dom h = {1,2} by FINSEQ_1:2,89;
hence a in product g by A1,A4,CARD_3:9;
end;
let a be object;
assume a in product g;
then consider h being Function such that
A10: a = h and
A11: dom h = dom g and
A12: for x being object st x in dom g holds h.x in g.x by CARD_3:def 5;
A13: [.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;
2 in dom g by A1,TARSKI:def 2;
then h.2 in g.2 by A12;
then h.2 in [.S-bound L~SpStSeq C,N-bound L~SpStSeq C.] by FUNCT_4:63;
then consider s being Real such that
A14: h.2 = s and
A15: S-bound L~SpStSeq C <= s & s <= N-bound L~SpStSeq C by A13;
A16: [.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;
1 in dom g by A1,TARSKI:def 2;
then h.1 in g.1 by A12;
then h.1 in [.W-bound L~SpStSeq C,E-bound L~SpStSeq C.] by FUNCT_4:63;
then consider r being Real such that
A17: h.1 = r and
A18: W-bound L~SpStSeq C <= r & r <= E-bound L~SpStSeq C by A16;
A19: 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:37;
A20: for k being object st k in dom h holds h.k = <*r,s*>.k
proof
let k be object;
assume k in dom h;
then k = 1 or k = 2 by A11,TARSKI:def 2;
hence thesis by A17,A14;
end;
dom <*r,s*> = {1,2} by FINSEQ_1:2,89;
then
A21: a = |[r,s]| by A10,A11,A20,FUNCT_1:2,FUNCT_4:62;
assume not a in Cl RightComp SpStSeq C;
then ( not a in RightComp SpStSeq C)& not a in L~SpStSeq C by A2,
XBOOLE_0:def 3;
then a in LeftComp SpStSeq C by A21,Th16;
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 A19;
hence contradiction by A18,A15,A21;
end;
theorem Th29:
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:39;
then
A2: g/.1 = N-min L~g by A1,FINSEQ_6:92;
thus proj1.:(Cl RightComp f) c= proj1.:(L~f)
proof
A3: Cl RightComp f = (RightComp f) \/ L~f by Th21;
let a be object;
assume a in proj1.:(Cl RightComp f);
then consider x being object 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:64;
per cases by A5,A3,XBOOLE_0:def 3;
suppose
A7: 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 XREAL_1:6;
then b in LeftComp g by A1,A2,JORDAN2C:113;
then b in LeftComp f by REVROT_1:36;
then LSeg(x,b) meets L~f by A7,Th27;
then consider c being object such that
A8: c in LSeg(x,b) and
A9: c in L~f by XBOOLE_0:3;
reconsider c as Point of TOP-REAL 2 by A8;
A10: b`1 = x`1;
proj1.c = c`1 by PSCOMP_1:def 5
.= x`1 by A8,A10,GOBOARD7:5
.= a by A6,PSCOMP_1:def 5;
hence thesis by A9,FUNCT_2:35;
end;
suppose
x in L~f;
hence thesis by A6,FUNCT_2:35;
end;
end;
L~f = (Cl RightComp f) \ RightComp f by Th19;
hence thesis by RELAT_1:123,XBOOLE_1:36;
end;
theorem Th30:
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:39;
then
A2: g/.1 = N-min L~g by A1,FINSEQ_6:92;
thus proj2.:(Cl RightComp f) c= proj2.:(L~f)
proof
A3: Cl RightComp f = (RightComp f) \/ L~f by Th21;
let a be object;
assume a in proj2.:(Cl RightComp f);
then consider x being object 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:64;
per cases by A5,A3,XBOOLE_0:def 3;
suppose
A7: 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 XREAL_1:6;
then b in LeftComp g by A1,A2,JORDAN2C:111;
then b in LeftComp f by REVROT_1:36;
then LSeg(x,b) meets L~f by A7,Th27;
then consider c be object such that
A8: c in LSeg(x,b) and
A9: c in L~f by XBOOLE_0:3;
reconsider c as Point of TOP-REAL 2 by A8;
A10: b`2 = x`2;
proj2.c = c`2 by PSCOMP_1:def 6
.= x`2 by A8,A10,GOBOARD7:6
.= a by A6,PSCOMP_1:def 6;
hence thesis by A9,FUNCT_2:35;
end;
suppose
x in L~f;
hence thesis by A6,FUNCT_2:35;
end;
end;
L~f = (Cl RightComp f) \ RightComp f by Th19;
hence thesis by RELAT_1:123,XBOOLE_1:36;
end;
theorem Th31:
RightComp g c= RightComp SpStSeq L~g
proof
let a be object;
assume
A1: a in RightComp g;
then reconsider p = a as Point of TOP-REAL 2;
p`1 > W-bound L~g by A1,Th23;
then
A2: p`1 > W-bound L~SpStSeq L~g by SPRECT_1:58;
p`2 > S-bound L~g by A1,Th26;
then
A3: p`2 > S-bound L~SpStSeq L~g by SPRECT_1:59;
p`1 < E-bound L~g by A1,Th24;
then
A4: p`1 < E-bound L~SpStSeq L~g by SPRECT_1:61;
p`2 < N-bound L~g by A1,Th25;
then
A5: p`2 < N-bound L~SpStSeq L~g by SPRECT_1:60;
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:37;
hence thesis by A2,A4,A3,A5;
end;
theorem Th32:
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 Th28;
then
A1: Cl RightComp SpStSeq L~g is compact by TOPREAL6:78;
RightComp g c= RightComp SpStSeq L~g by Th31;
hence thesis by A1,COMPTS_1:9,PRE_TOPC:19;
end;
theorem Th33:
LeftComp g is non bounded
proof
Cl RightComp g is compact by Th32;
then RightComp g is bounded by PRE_TOPC:18,RLTOPSP1:42;
then
A1: L~g \/ RightComp g is bounded by TOPREAL6:67;
L~g \/ RightComp g \/ LeftComp g = the carrier of TOP-REAL 2 by Th15;
hence thesis by A1,TOPREAL6:66;
end;
theorem Th34:
LeftComp g is_outside_component_of L~g
by GOBOARD9:def 1,Th33;
theorem
RightComp g is_inside_component_of L~g
proof
thus RightComp g is_a_component_of (L~g)` by GOBOARD9:def 2;
Cl RightComp g is compact by Th32;
hence thesis by PRE_TOPC:18,RLTOPSP1:42;
end;
theorem Th36:
UBD L~g = LeftComp g
proof
UBD L~g is_outside_component_of L~g & LeftComp g is_outside_component_of
L~g by Th34,JORDAN2C:68;
hence thesis by JORDAN2C:119;
end;
theorem Th37:
BDD L~g = RightComp g
proof
A1: (BDD L~g) misses (UBD L~g) by JORDAN2C:24;
A2: (L~g)` = (BDD L~g) \/ (UBD L~g) & LeftComp g misses RightComp g by Th14,
JORDAN2C:27;
UBD L~g = LeftComp g & (L~g)` = LeftComp g \/ RightComp g by Th36,GOBRD12:10;
hence thesis by A2,A1,XBOOLE_1:71;
end;
theorem
P is_outside_component_of L~g implies P = LeftComp g
proof
assume
A1: P is_outside_component_of L~g;
UBD L~g is_outside_component_of L~g by JORDAN2C:68;
then P = UBD L~g by A1,JORDAN2C:119;
hence thesis by Th36;
end;
theorem Th39:
P is_inside_component_of L~g implies P meets RightComp g
proof
assume P is_inside_component_of L~g;
then
A1: P c= BDD L~g & P is_a_component_of (L~g)` by JORDAN2C:22;
BDD L~g = RightComp g by Th37;
hence thesis by A1,SPRECT_1:4,XBOOLE_1:67;
end;
theorem
P is_inside_component_of L~g implies P = BDD L~g
proof
A1: RightComp g = BDD L~g by Th37;
BDD L~g is_inside_component_of L~g by JORDAN2C:108;
then
A2: BDD L~g is_a_component_of (L~g)`;
assume
A3: P is_inside_component_of L~g;
thus thesis by A3,A1,A2,Th39,GOBOARD9:1;
end;
theorem
W-bound L~g = W-bound RightComp g
proof
set A = (Cl RightComp g) \ RightComp g;
A1: W-bound Cl RightComp g = lower_bound (proj1.:(Cl RightComp g)) by
SPRECT_1:43;
A2: L~g = A by Th19;
Cl RightComp g is compact by Th32;
then
A3: RightComp g is bounded by PRE_TOPC:18,RLTOPSP1:42;
reconsider A as non empty Subset of TOP-REAL 2 by A2;
proj1.:(Cl RightComp g) = proj1.:(L~g) & W-bound A = lower_bound (proj1
.:A) by Th29,SPRECT_1:43;
hence thesis by A2,A3,A1,TOPREAL6:85;
end;
theorem
E-bound L~g = E-bound RightComp g
proof
set A = (Cl RightComp g) \ RightComp g;
A1: E-bound Cl RightComp g = upper_bound (proj1.:(Cl RightComp g))
by SPRECT_1:46;
A2: L~g = A by Th19;
Cl RightComp g is compact by Th32;
then
A3: RightComp g is bounded by PRE_TOPC:18,RLTOPSP1:42;
reconsider A as non empty Subset of TOP-REAL 2 by A2;
proj1.:(Cl RightComp g) = proj1.:(L~g) & E-bound A =
upper_bound (proj1.:A) by Th29,SPRECT_1:46;
hence thesis by A2,A3,A1,TOPREAL6:86;
end;
theorem
N-bound L~g = N-bound RightComp g
proof
set A = (Cl RightComp g) \ RightComp g;
A1: N-bound Cl RightComp g = upper_bound (proj2.:(Cl RightComp g))
by SPRECT_1:45;
A2: L~g = A by Th19;
Cl RightComp g is compact by Th32;
then
A3: RightComp g is bounded by PRE_TOPC:18,RLTOPSP1:42;
reconsider A as non empty Subset of TOP-REAL 2 by A2;
proj2.:(Cl RightComp g) = proj2.:(L~g) &
N-bound A = upper_bound (proj2.:A) by Th30,SPRECT_1:45;
hence thesis by A2,A3,A1,TOPREAL6:87;
end;
theorem
S-bound L~g = S-bound RightComp g
proof
set A = (Cl RightComp g) \ RightComp g;
A1: S-bound Cl RightComp g = lower_bound (proj2.:(Cl RightComp g)) by
SPRECT_1:44;
A2: L~g = A by Th19;
Cl RightComp g is compact by Th32;
then
A3: RightComp g is bounded by PRE_TOPC:18,RLTOPSP1:42;
reconsider A as non empty Subset of TOP-REAL 2 by A2;
proj2.:(Cl RightComp g) = proj2.:(L~g) & S-bound A = lower_bound (proj2
.:A) by Th30,SPRECT_1:44;
hence thesis by A2,A3,A1,TOPREAL6:88;
end;