:: GOBRD14 semantic presentation
begin
Lm1: the carrier of (TOP-REAL 2) = REAL 2
by EUCLID:22;
theorem :: GOBRD14:1
for f being non constant standard special_circular_sequence
for P being Subset of (TOP-REAL 2)
for p being Point of (Euclid 2) st p = 0.REAL 2 & P is_outside_component_of L~ f holds
ex r being Real st
( r > 0 & (Ball (p,r)) ` c= P )
proof
let f be non constant standard special_circular_sequence; ::_thesis: for P being Subset of (TOP-REAL 2)
for p being Point of (Euclid 2) st p = 0.REAL 2 & P is_outside_component_of L~ f holds
ex r being Real st
( r > 0 & (Ball (p,r)) ` c= P )
let P be Subset of (TOP-REAL 2); ::_thesis: for p being Point of (Euclid 2) st p = 0.REAL 2 & P is_outside_component_of L~ f holds
ex r being Real st
( r > 0 & (Ball (p,r)) ` c= P )
let p be Point of (Euclid 2); ::_thesis: ( p = 0.REAL 2 & P is_outside_component_of L~ f implies ex r being Real st
( r > 0 & (Ball (p,r)) ` c= P ) )
assume that
A1: p = 0.REAL 2 and
A2: P is_outside_component_of L~ f ; ::_thesis: ex r being Real st
( r > 0 & (Ball (p,r)) ` c= P )
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 ((dist (p,c)) + r) + 1 ; ::_thesis: ( ((dist (p,c)) + r) + 1 > 0 & (Ball (p,(((dist (p,c)) + r) + 1))) ` c= P )
set L = (REAL 2) \ { a where a is Point of (TOP-REAL 2) : |.a.| < ((dist (p,c)) + r) + 1 } ;
((dist (p,c)) + r) + 0 < ((dist (p,c)) + r) + 1 by XREAL_1:8;
hence 0 < ((dist (p,c)) + r) + 1 by A3, METRIC_1:5, XREAL_1:8; ::_thesis: (Ball (p,(((dist (p,c)) + r) + 1))) ` c= P
then ((dist (p,c)) + r) + 1 = abs (((dist (p,c)) + r) + 1) by ABSVALUE:def_1;
then for a being Point of (TOP-REAL 2) holds
( a <> |[0,(((dist (p,c)) + r) + 1)]| or |.a.| >= ((dist (p,c)) + r) + 1 ) by TOPREAL6:23;
then not |[0,(((dist (p,c)) + r) + 1)]| in { a where a is Point of (TOP-REAL 2) : |.a.| < ((dist (p,c)) + r) + 1 } ;
then reconsider L = (REAL 2) \ { a where a is Point of (TOP-REAL 2) : |.a.| < ((dist (p,c)) + r) + 1 } as non empty Subset of (TOP-REAL 2) by Lm1, XBOOLE_0:def_5;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (Ball (p,(((dist (p,c)) + r) + 1))) ` or x in P )
assume A5: x in (Ball (p,(((dist (p,c)) + r) + 1))) ` ; ::_thesis: x in P
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,(((dist (p,c)) + r) + 1))
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in D or x in Ball (p,(((dist (p,c)) + r) + 1)) )
A8: ((dist (p,c)) + r) + 0 < ((dist (p,c)) + r) + 1 by XREAL_1:6;
assume A9: x in D ; ::_thesis: x in Ball (p,(((dist (p,c)) + r) + 1))
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 x in Ball (p,(((dist (p,c)) + r) + 1)) by METRIC_1:11; ::_thesis: verum
end;
A11: L c= (L~ f) `
proof
let l be set ; :: according to TARSKI:def_3 ::_thesis: ( not l in L or l in (L~ f) ` )
assume A12: l in L ; ::_thesis: l in (L~ f) `
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.| < ((dist (p,c)) + r) + 1 } by A12, XBOOLE_0:def_5;
then A13: |.j.| >= ((dist (p,c)) + r) + 1 ;
now__::_thesis:_not_l_in_L~_f
assume l in L~ f ; ::_thesis: contradiction
then dist (t,p) < ((dist (p,c)) + r) + 1 by A7, METRIC_1:11;
hence contradiction by A1, A13, TOPREAL6:25; ::_thesis: verum
end;
hence l in (L~ f) ` by A12, SUBSET_1:29; ::_thesis: verum
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; :: according to JORDAN2C:def_3 ::_thesis: not M is bounded
not W is bounded by JORDAN2C:62;
then not L is bounded by JORDAN2C:11;
hence not M is bounded by A15, RLTOPSP1:42; ::_thesis: verum
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,(((dist (p,c)) + r) + 1)) by A5, XBOOLE_0:def_5;
then for k being Point of (TOP-REAL 2) holds
( k <> z or |.k.| >= ((dist (p,c)) + r) + 1 ) by A6, METRIC_1:11;
then ( z in REAL 2 & not x in { a where a is Point of (TOP-REAL 2) : |.a.| < ((dist (p,c)) + r) + 1 } ) ;
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 x in P by A17, A15, A16, TARSKI:def_4; ::_thesis: verum
end;
begin
theorem :: GOBRD14:2
for n being Element of NAT
for f being FinSequence of (TOP-REAL n) st L~ f <> {} holds
2 <= len f
proof
let n be Element of NAT ; ::_thesis: for f being FinSequence of (TOP-REAL n) st L~ f <> {} holds
2 <= len f
let f be FinSequence of (TOP-REAL n); ::_thesis: ( L~ f <> {} implies 2 <= len f )
assume L~ f <> {} ; ::_thesis: 2 <= len 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 2 <= len f ; ::_thesis: verum
end;
theorem Th3: :: GOBRD14:3
for i, j being Element of NAT
for G being Go-board st 1 <= i & i < len G & 1 <= j & j < width G holds
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
let i, j be Element of NAT ; ::_thesis: for G being Go-board st 1 <= i & i < len G & 1 <= j & j < width G holds
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).]))
let G be Go-board; ::_thesis: ( 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).])) )
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 ((1,2) --> ([.((G * (i,1)) `1),((G * ((i + 1),1)) `1).],[.((G * (1,j)) `2),((G * (1,(j + 1))) `2).])) = {1,2} by FUNCT_4:62;
assume ( 1 <= i & i < len G & 1 <= j & j < width G ) ; ::_thesis: 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).]))
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 ((1,2) --> ([.((G * (i,1)) `1),((G * ((i + 1),1)) `1).],[.((G * (1,j)) `2),((G * (1,(j + 1))) `2).])) :: according to XBOOLE_0:def_10 ::_thesis: product ((1,2) --> ([.((G * (i,1)) `1),((G * ((i + 1),1)) `1).],[.((G * (1,j)) `2),((G * (1,(j + 1))) `2).])) c= cell (G,i,j)
proof
let c be set ; :: according to TARSKI:def_3 ::_thesis: ( not c in cell (G,i,j) or c in product ((1,2) --> ([.((G * (i,1)) `1),((G * ((i + 1),1)) `1).],[.((G * (1,j)) `2),((G * (1,(j + 1))) `2).])) )
assume c in cell (G,i,j) ; ::_thesis: c in product ((1,2) --> ([.((G * (i,1)) `1),((G * ((i + 1),1)) `1).],[.((G * (1,j)) `2),((G * (1,(j + 1))) `2).]))
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 set st x in dom ((1,2) --> ([.((G * (i,1)) `1),((G * ((i + 1),1)) `1).],[.((G * (1,j)) `2),((G * (1,(j + 1))) `2).])) holds
<*r,s*> . x in ((1,2) --> ([.((G * (i,1)) `1),((G * ((i + 1),1)) `1).],[.((G * (1,j)) `2),((G * (1,(j + 1))) `2).])) . x
proof
let x be set ; ::_thesis: ( x in dom ((1,2) --> ([.((G * (i,1)) `1),((G * ((i + 1),1)) `1).],[.((G * (1,j)) `2),((G * (1,(j + 1))) `2).])) implies <*r,s*> . x in ((1,2) --> ([.((G * (i,1)) `1),((G * ((i + 1),1)) `1).],[.((G * (1,j)) `2),((G * (1,(j + 1))) `2).])) . x )
A9: s = |[r,s]| `2 by EUCLID:52
.= <*r,s*> . 2 ;
assume x in dom ((1,2) --> ([.((G * (i,1)) `1),((G * ((i + 1),1)) `1).],[.((G * (1,j)) `2),((G * (1,(j + 1))) `2).])) ; ::_thesis: <*r,s*> . x in ((1,2) --> ([.((G * (i,1)) `1),((G * ((i + 1),1)) `1).],[.((G * (1,j)) `2),((G * (1,(j + 1))) `2).])) . x
then A10: ( x = 1 or x = 2 ) by TARSKI:def_2;
r = |[r,s]| `1 by EUCLID:52
.= <*r,s*> . 1 ;
hence <*r,s*> . x in ((1,2) --> ([.((G * (i,1)) `1),((G * ((i + 1),1)) `1).],[.((G * (1,j)) `2),((G * (1,(j + 1))) `2).])) . x by A7, A10, A9, FUNCT_4:63; ::_thesis: verum
end;
dom <*r,s*> = {1,2} by FINSEQ_1:2, FINSEQ_1:89;
hence c in product ((1,2) --> ([.((G * (i,1)) `1),((G * ((i + 1),1)) `1).],[.((G * (1,j)) `2),((G * (1,(j + 1))) `2).])) by A2, A5, A8, CARD_3:9; ::_thesis: verum
end;
let c be set ; :: according to TARSKI:def_3 ::_thesis: ( not c in product ((1,2) --> ([.((G * (i,1)) `1),((G * ((i + 1),1)) `1).],[.((G * (1,j)) `2),((G * (1,(j + 1))) `2).])) or c in cell (G,i,j) )
assume c in product ((1,2) --> ([.((G * (i,1)) `1),((G * ((i + 1),1)) `1).],[.((G * (1,j)) `2),((G * (1,(j + 1))) `2).])) ; ::_thesis: c in cell (G,i,j)
then consider g being Function such that
A11: c = g and
A12: dom g = dom ((1,2) --> ([.((G * (i,1)) `1),((G * ((i + 1),1)) `1).],[.((G * (1,j)) `2),((G * (1,(j + 1))) `2).])) and
A13: for x being set st x in dom ((1,2) --> ([.((G * (i,1)) `1),((G * ((i + 1),1)) `1).],[.((G * (1,j)) `2),((G * (1,(j + 1))) `2).])) holds
g . x in ((1,2) --> ([.((G * (i,1)) `1),((G * ((i + 1),1)) `1).],[.((G * (1,j)) `2),((G * (1,(j + 1))) `2).])) . x by CARD_3:def_5;
2 in dom ((1,2) --> ([.((G * (i,1)) `1),((G * ((i + 1),1)) `1).],[.((G * (1,j)) `2),((G * (1,(j + 1))) `2).])) by A2, TARSKI:def_2;
then g . 2 in ((1,2) --> ([.((G * (i,1)) `1),((G * ((i + 1),1)) `1).],[.((G * (1,j)) `2),((G * (1,(j + 1))) `2).])) . 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 ((1,2) --> ([.((G * (i,1)) `1),((G * ((i + 1),1)) `1).],[.((G * (1,j)) `2),((G * (1,(j + 1))) `2).])) by A2, TARSKI:def_2;
then g . 1 in ((1,2) --> ([.((G * (i,1)) `1),((G * ((i + 1),1)) `1).],[.((G * (1,j)) `2),((G * (1,(j + 1))) `2).])) . 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 set st k in dom g holds
g . k = <*a,b*> . k
proof
let k be set ; ::_thesis: ( k in dom g implies g . k = <*a,b*> . k )
assume k in dom g ; ::_thesis: g . k = <*a,b*> . k
then ( k = 1 or k = 2 ) by A12, TARSKI:def_2;
hence g . k = <*a,b*> . k by A16, A14, FINSEQ_1:44; ::_thesis: verum
end;
dom <*a,b*> = {1,2} by FINSEQ_1:2, FINSEQ_1:89;
then c = |[a,b]| by A11, A12, A18, FUNCT_1:2, FUNCT_4:62;
hence c in cell (G,i,j) by A3, A17, A15; ::_thesis: verum
end;
theorem :: GOBRD14:4
for i, j being Element of NAT
for G being Go-board st 1 <= i & i < len G & 1 <= j & j < width G holds
cell (G,i,j) is compact
proof
let i, j be Element of NAT ; ::_thesis: for G being Go-board st 1 <= i & i < len G & 1 <= j & j < width G holds
cell (G,i,j) is compact
let G be Go-board; ::_thesis: ( 1 <= i & i < len G & 1 <= j & j < width G implies cell (G,i,j) is compact )
assume ( 1 <= i & i < len G & 1 <= j & j < width G ) ; ::_thesis: cell (G,i,j) is compact
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 cell (G,i,j) is compact by TOPREAL6:78; ::_thesis: verum
end;
theorem :: GOBRD14:5
for i, j, n being Element of NAT
for G being Go-board st [i,j] in Indices G & [(i + n),j] in Indices G holds
dist ((G * (i,j)),(G * ((i + n),j))) = ((G * ((i + n),j)) `1) - ((G * (i,j)) `1)
proof
let i, j, n be Element of NAT ; ::_thesis: for G being Go-board st [i,j] in Indices G & [(i + n),j] in Indices G holds
dist ((G * (i,j)),(G * ((i + n),j))) = ((G * ((i + n),j)) `1) - ((G * (i,j)) `1)
let G be Go-board; ::_thesis: ( [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) )
assume that
A1: [i,j] in Indices G and
A2: [(i + n),j] in Indices G ; ::_thesis: dist ((G * (i,j)),(G * ((i + n),j))) = ((G * ((i + n),j)) `1) - ((G * (i,j)) `1)
set x = G * (i,j);
set y = G * ((i + n),j);
percases ( n = 0 or n <> 0 ) ;
suppose n = 0 ; ::_thesis: dist ((G * (i,j)),(G * ((i + n),j))) = ((G * ((i + n),j)) `1) - ((G * (i,j)) `1)
hence dist ((G * (i,j)),(G * ((i + n),j))) = ((G * ((i + n),j)) `1) - ((G * (i,j)) `1) by TOPREAL6:93; ::_thesis: verum
end;
supposeA3: n <> 0 ; ::_thesis: dist ((G * (i,j)),(G * ((i + n),j))) = ((G * ((i + n),j)) `1) - ((G * (i,j)) `1)
A4: i + n <= len G by A2, MATRIX_1:38;
A5: 1 <= i by A1, MATRIX_1:38;
A6: 1 <= i + n by A2, MATRIX_1:38;
A7: ( 1 <= j & j <= width G ) by A1, MATRIX_1:38;
1 <= n by A3, NAT_1:14;
then i < i + n by NAT_1:19;
then (G * (i,j)) `1 < (G * ((i + n),j)) `1 by A4, A7, A5, GOBOARD5:3;
then A8: ((G * (i,j)) `1) - ((G * (i,j)) `1) < ((G * ((i + n),j)) `1) - ((G * (i,j)) `1) by XREAL_1:14;
i <= len G by A1, MATRIX_1:38;
then A9: (G * (i,j)) `2 = (G * (1,j)) `2 by A7, A5, GOBOARD5:1
.= (G * ((i + n),j)) `2 by A6, A4, A7, GOBOARD5:1 ;
thus dist ((G * (i,j)),(G * ((i + n),j))) = sqrt (((((G * (i,j)) `1) - ((G * ((i + n),j)) `1)) ^2) + ((((G * (i,j)) `2) - ((G * ((i + n),j)) `2)) ^2)) by TOPREAL6:92
.= abs (((G * (i,j)) `1) - ((G * ((i + n),j)) `1)) by A9, COMPLEX1:72
.= abs (- (((G * (i,j)) `1) - ((G * ((i + n),j)) `1))) by COMPLEX1:52
.= ((G * ((i + n),j)) `1) - ((G * (i,j)) `1) by A8, ABSVALUE:def_1 ; ::_thesis: verum
end;
end;
end;
theorem :: GOBRD14:6
for i, j, n being Element of NAT
for G being Go-board st [i,j] in Indices G & [i,(j + n)] in Indices G holds
dist ((G * (i,j)),(G * (i,(j + n)))) = ((G * (i,(j + n))) `2) - ((G * (i,j)) `2)
proof
let i, j, n be Element of NAT ; ::_thesis: for G being Go-board st [i,j] in Indices G & [i,(j + n)] in Indices G holds
dist ((G * (i,j)),(G * (i,(j + n)))) = ((G * (i,(j + n))) `2) - ((G * (i,j)) `2)
let G be Go-board; ::_thesis: ( [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) )
assume that
A1: [i,j] in Indices G and
A2: [i,(j + n)] in Indices G ; ::_thesis: dist ((G * (i,j)),(G * (i,(j + n)))) = ((G * (i,(j + n))) `2) - ((G * (i,j)) `2)
set x = G * (i,j);
set y = G * (i,(j + n));
percases ( n = 0 or n <> 0 ) ;
suppose n = 0 ; ::_thesis: dist ((G * (i,j)),(G * (i,(j + n)))) = ((G * (i,(j + n))) `2) - ((G * (i,j)) `2)
hence dist ((G * (i,j)),(G * (i,(j + n)))) = ((G * (i,(j + n))) `2) - ((G * (i,j)) `2) by TOPREAL6:93; ::_thesis: verum
end;
supposeA3: n <> 0 ; ::_thesis: dist ((G * (i,j)),(G * (i,(j + n)))) = ((G * (i,(j + n))) `2) - ((G * (i,j)) `2)
A4: j + n <= width G by A2, MATRIX_1:38;
A5: ( 1 <= i & i <= len G ) by A1, MATRIX_1:38;
A6: 1 <= j + n by A2, MATRIX_1:38;
A7: 1 <= j by A1, MATRIX_1:38;
1 <= n by A3, NAT_1:14;
then j < j + n by NAT_1:19;
then (G * (i,j)) `2 < (G * (i,(j + n))) `2 by A4, A7, A5, GOBOARD5:4;
then A8: ((G * (i,j)) `2) - ((G * (i,j)) `2) < ((G * (i,(j + n))) `2) - ((G * (i,j)) `2) by XREAL_1:14;
j <= width G by A1, MATRIX_1:38;
then A9: (G * (i,j)) `1 = (G * (i,1)) `1 by A7, A5, GOBOARD5:2
.= (G * (i,(j + n))) `1 by A6, A4, A5, GOBOARD5:2 ;
thus dist ((G * (i,j)),(G * (i,(j + n)))) = sqrt (((((G * (i,j)) `1) - ((G * (i,(j + n))) `1)) ^2) + ((((G * (i,j)) `2) - ((G * (i,(j + n))) `2)) ^2)) by TOPREAL6:92
.= abs (((G * (i,j)) `2) - ((G * (i,(j + n))) `2)) by A9, COMPLEX1:72
.= abs (- (((G * (i,j)) `2) - ((G * (i,(j + n))) `2))) by COMPLEX1:52
.= ((G * (i,(j + n))) `2) - ((G * (i,j)) `2) by A8, ABSVALUE:def_1 ; ::_thesis: verum
end;
end;
end;
theorem :: GOBRD14:7
for n being Element of NAT
for C being compact non horizontal non vertical Subset of (TOP-REAL 2) holds 3 <= (len (Gauge (C,n))) -' 1
proof
let n be Element of NAT ; ::_thesis: for C being compact non horizontal non vertical Subset of (TOP-REAL 2) holds 3 <= (len (Gauge (C,n))) -' 1
let C be compact non horizontal non vertical Subset of (TOP-REAL 2); ::_thesis: 3 <= (len (Gauge (C,n))) -' 1
set G = Gauge (C,n);
4 <= len (Gauge (C,n)) by JORDAN8:10;
then 4 - 1 <= (len (Gauge (C,n))) - 1 by XREAL_1:13;
hence 3 <= (len (Gauge (C,n))) -' 1 by XREAL_0:def_2; ::_thesis: verum
end;
theorem :: GOBRD14:8
for i, j being Element of NAT
for C being compact non horizontal non vertical Subset of (TOP-REAL 2) st i <= j holds
for a, b being Element of NAT st 2 <= a & a <= (len (Gauge (C,i))) - 1 & 2 <= b & b <= (len (Gauge (C,i))) - 1 holds
ex c, d being Element of 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
let i, j be Element of NAT ; ::_thesis: for C being compact non horizontal non vertical Subset of (TOP-REAL 2) st i <= j holds
for a, b being Element of NAT st 2 <= a & a <= (len (Gauge (C,i))) - 1 & 2 <= b & b <= (len (Gauge (C,i))) - 1 holds
ex c, d being Element of 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)) )
let C be compact non horizontal non vertical Subset of (TOP-REAL 2); ::_thesis: ( i <= j implies for a, b being Element of NAT st 2 <= a & a <= (len (Gauge (C,i))) - 1 & 2 <= b & b <= (len (Gauge (C,i))) - 1 holds
ex c, d being Element of 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)) ) )
A1: 0 <> 2 |^ i by NEWTON:83;
assume A2: i <= j ; ::_thesis: for a, b being Element of NAT st 2 <= a & a <= (len (Gauge (C,i))) - 1 & 2 <= b & b <= (len (Gauge (C,i))) - 1 holds
ex c, d being Element of 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)) )
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 Element of NAT ; ::_thesis: ( 2 <= a & a <= (len (Gauge (C,i))) - 1 & 2 <= b & b <= (len (Gauge (C,i))) - 1 implies ex c, d being Element of 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)) ) )
assume that
A4: 2 <= a and
A5: a <= (len (Gauge (C,i))) - 1 and
A6: 2 <= b and
A7: b <= (len (Gauge (C,i))) - 1 ; ::_thesis: ex c, d being Element of 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)) )
A8: ( 1 <= a & 1 <= b ) by A4, A6, XXREAL_0:2;
set c = 2 + ((2 |^ (j -' i)) * (a -' 2));
set d = 2 + ((2 |^ (j -' i)) * (b -' 2));
A9: 0 <= b - 2 by A6, XREAL_1:48;
set n = N-bound C;
set e = E-bound C;
set s = S-bound C;
set w = W-bound C;
A10: 0 <> 2 |^ j by NEWTON:83;
A11: (((N-bound C) - (S-bound C)) / (2 |^ j)) * ((2 + ((2 |^ (j -' i)) * (b -' 2))) - 2) = (((N-bound C) - (S-bound C)) / (2 |^ j)) * (((2 |^ j) / (2 |^ i)) * (b -' 2)) by A2, TOPREAL6:10
.= ((((N-bound C) - (S-bound C)) / (2 |^ j)) * ((2 |^ j) / (2 |^ i))) * (b -' 2)
.= (((N-bound C) - (S-bound C)) / ((2 |^ j) / ((2 |^ j) / (2 |^ i)))) * (b -' 2) by XCMPLX_1:81
.= (((N-bound C) - (S-bound C)) / (2 |^ i)) * (b -' 2) by A10, XCMPLX_1:52
.= (((N-bound C) - (S-bound C)) / (2 |^ i)) * (b - 2) by A9, XREAL_0:def_2 ;
take 2 + ((2 |^ (j -' i)) * (a -' 2)) ; ::_thesis: ex d being Element of NAT st
( 2 <= 2 + ((2 |^ (j -' i)) * (a -' 2)) & 2 + ((2 |^ (j -' i)) * (a -' 2)) <= (len (Gauge (C,j))) - 1 & 2 <= d & d <= (len (Gauge (C,j))) - 1 & [(2 + ((2 |^ (j -' i)) * (a -' 2))),d] in Indices (Gauge (C,j)) & (Gauge (C,i)) * (a,b) = (Gauge (C,j)) * ((2 + ((2 |^ (j -' i)) * (a -' 2))),d) & 2 + ((2 |^ (j -' i)) * (a -' 2)) = 2 + ((2 |^ (j -' i)) * (a -' 2)) & d = 2 + ((2 |^ (j -' i)) * (b -' 2)) )
take 2 + ((2 |^ (j -' i)) * (b -' 2)) ; ::_thesis: ( 2 <= 2 + ((2 |^ (j -' i)) * (a -' 2)) & 2 + ((2 |^ (j -' i)) * (a -' 2)) <= (len (Gauge (C,j))) - 1 & 2 <= 2 + ((2 |^ (j -' i)) * (b -' 2)) & 2 + ((2 |^ (j -' i)) * (b -' 2)) <= (len (Gauge (C,j))) - 1 & [(2 + ((2 |^ (j -' i)) * (a -' 2))),(2 + ((2 |^ (j -' i)) * (b -' 2)))] in Indices (Gauge (C,j)) & (Gauge (C,i)) * (a,b) = (Gauge (C,j)) * ((2 + ((2 |^ (j -' i)) * (a -' 2))),(2 + ((2 |^ (j -' i)) * (b -' 2)))) & 2 + ((2 |^ (j -' i)) * (a -' 2)) = 2 + ((2 |^ (j -' i)) * (a -' 2)) & 2 + ((2 |^ (j -' i)) * (b -' 2)) = 2 + ((2 |^ (j -' i)) * (b -' 2)) )
A12: 2 + 0 <= 2 + ((2 |^ (j -' i)) * (a -' 2)) by XREAL_1:6;
then A13: 1 <= 2 + ((2 |^ (j -' i)) * (a -' 2)) 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-bound C) - (W-bound C)) / (2 |^ j)) * ((2 + ((2 |^ (j -' i)) * (a -' 2))) - 2) = (((E-bound C) - (W-bound C)) / (2 |^ j)) * (((2 |^ j) / (2 |^ i)) * (a -' 2)) by A2, TOPREAL6:10
.= ((((E-bound C) - (W-bound C)) / (2 |^ j)) * ((2 |^ j) / (2 |^ i))) * (a -' 2)
.= (((E-bound C) - (W-bound C)) / ((2 |^ j) / ((2 |^ j) / (2 |^ i)))) * (a -' 2) by XCMPLX_1:81
.= (((E-bound C) - (W-bound C)) / (2 |^ i)) * (a -' 2) by A10, XCMPLX_1:52
.= (((E-bound C) - (W-bound C)) / (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 <= 2 + ((2 |^ (j -' i)) * (a -' 2)) & 2 + ((2 |^ (j -' i)) * (a -' 2)) <= (len (Gauge (C,j))) - 1 & 2 <= 2 + ((2 |^ (j -' i)) * (b -' 2)) & 2 + ((2 |^ (j -' i)) * (b -' 2)) <= (len (Gauge (C,j))) - 1 ) by A19, A20, A12, XREAL_1:6; ::_thesis: ( [(2 + ((2 |^ (j -' i)) * (a -' 2))),(2 + ((2 |^ (j -' i)) * (b -' 2)))] in Indices (Gauge (C,j)) & (Gauge (C,i)) * (a,b) = (Gauge (C,j)) * ((2 + ((2 |^ (j -' i)) * (a -' 2))),(2 + ((2 |^ (j -' i)) * (b -' 2)))) & 2 + ((2 |^ (j -' i)) * (a -' 2)) = 2 + ((2 |^ (j -' i)) * (a -' 2)) & 2 + ((2 |^ (j -' i)) * (b -' 2)) = 2 + ((2 |^ (j -' i)) * (b -' 2)) )
then A24: 1 <= 2 + ((2 |^ (j -' i)) * (b -' 2)) by XXREAL_0:2;
width (Gauge (C,j)) = len (Gauge (C,j)) by JORDAN8:def_1;
then A25: 2 + ((2 |^ (j -' i)) * (b -' 2)) <= width (Gauge (C,j)) by A23, A17, XXREAL_0:2;
2 + ((2 |^ (j -' i)) * (a -' 2)) <= len (Gauge (C,j)) by A23, A17, XXREAL_0:2;
hence [(2 + ((2 |^ (j -' i)) * (a -' 2))),(2 + ((2 |^ (j -' i)) * (b -' 2)))] in Indices (Gauge (C,j)) by A13, A24, A25, MATRIX_1:36; ::_thesis: ( (Gauge (C,i)) * (a,b) = (Gauge (C,j)) * ((2 + ((2 |^ (j -' i)) * (a -' 2))),(2 + ((2 |^ (j -' i)) * (b -' 2)))) & 2 + ((2 |^ (j -' i)) * (a -' 2)) = 2 + ((2 |^ (j -' i)) * (a -' 2)) & 2 + ((2 |^ (j -' i)) * (b -' 2)) = 2 + ((2 |^ (j -' i)) * (b -' 2)) )
then A26: (Gauge (C,j)) * ((2 + ((2 |^ (j -' i)) * (a -' 2))),(2 + ((2 |^ (j -' i)) * (b -' 2)))) = |[((W-bound C) + ((((E-bound C) - (W-bound C)) / (2 |^ j)) * ((2 + ((2 |^ (j -' i)) * (a -' 2))) - 2))),((S-bound C) + ((((N-bound C) - (S-bound C)) / (2 |^ j)) * ((2 + ((2 |^ (j -' i)) * (b -' 2))) - 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_1:36;
then A27: (Gauge (C,i)) * (a,b) = |[((W-bound C) + ((((E-bound C) - (W-bound C)) / (2 |^ i)) * (a - 2))),((S-bound C) + ((((N-bound C) - (S-bound C)) / (2 |^ i)) * (b - 2)))]| by JORDAN8:def_1;
then A28: ((Gauge (C,i)) * (a,b)) `2 = (S-bound C) + ((((N-bound C) - (S-bound C)) / (2 |^ i)) * (b - 2)) by EUCLID:52
.= ((Gauge (C,j)) * ((2 + ((2 |^ (j -' i)) * (a -' 2))),(2 + ((2 |^ (j -' i)) * (b -' 2))))) `2 by A26, A11, EUCLID:52 ;
((Gauge (C,i)) * (a,b)) `1 = (W-bound C) + ((((E-bound C) - (W-bound C)) / (2 |^ i)) * (a - 2)) by A27, EUCLID:52
.= ((Gauge (C,j)) * ((2 + ((2 |^ (j -' i)) * (a -' 2))),(2 + ((2 |^ (j -' i)) * (b -' 2))))) `1 by A26, A16, EUCLID:52 ;
hence (Gauge (C,i)) * (a,b) = (Gauge (C,j)) * ((2 + ((2 |^ (j -' i)) * (a -' 2))),(2 + ((2 |^ (j -' i)) * (b -' 2)))) by A28, TOPREAL3:6; ::_thesis: ( 2 + ((2 |^ (j -' i)) * (a -' 2)) = 2 + ((2 |^ (j -' i)) * (a -' 2)) & 2 + ((2 |^ (j -' i)) * (b -' 2)) = 2 + ((2 |^ (j -' i)) * (b -' 2)) )
thus ( 2 + ((2 |^ (j -' i)) * (a -' 2)) = 2 + ((2 |^ (j -' i)) * (a -' 2)) & 2 + ((2 |^ (j -' i)) * (b -' 2)) = 2 + ((2 |^ (j -' i)) * (b -' 2)) ) ; ::_thesis: verum
end;
theorem Th9: :: GOBRD14:9
for i, j, n being Element of NAT
for C being compact non horizontal non vertical Subset of (TOP-REAL 2) st [i,j] in Indices (Gauge (C,n)) & [i,(j + 1)] in Indices (Gauge (C,n)) holds
dist (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * (i,(j + 1)))) = ((N-bound C) - (S-bound C)) / (2 |^ n)
proof
let i, j, n be Element of NAT ; ::_thesis: for C being compact non horizontal non vertical Subset of (TOP-REAL 2) st [i,j] in Indices (Gauge (C,n)) & [i,(j + 1)] in Indices (Gauge (C,n)) holds
dist (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * (i,(j + 1)))) = ((N-bound C) - (S-bound C)) / (2 |^ n)
let C be compact non horizontal non vertical Subset of (TOP-REAL 2); ::_thesis: ( [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) )
set G = Gauge (C,n);
set a = N-bound C;
set e = E-bound C;
set s = S-bound C;
set w = W-bound C;
set p1 = (Gauge (C,n)) * (i,j);
set p2 = (Gauge (C,n)) * (i,(j + 1));
assume that
A1: [i,j] in Indices (Gauge (C,n)) and
A2: [i,(j + 1)] in Indices (Gauge (C,n)) ; ::_thesis: dist (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * (i,(j + 1)))) = ((N-bound C) - (S-bound C)) / (2 |^ n)
A3: (Gauge (C,n)) * (i,(j + 1)) = |[((W-bound C) + ((((E-bound C) - (W-bound C)) / (2 |^ n)) * (i - 2))),((S-bound C) + ((((N-bound C) - (S-bound C)) / (2 |^ n)) * ((j + 1) - 2)))]| by A2, JORDAN8:def_1;
N-bound C >= S-bound C by SPRECT_1:22;
then A4: (N-bound C) - (S-bound C) >= (S-bound C) - (S-bound C) by XREAL_1:9;
set x = ((N-bound C) - (S-bound C)) / (2 |^ n);
consider p, q being Point of (Euclid 2) such that
A5: ( p = (Gauge (C,n)) * (i,j) & q = (Gauge (C,n)) * (i,(j + 1)) ) and
A6: dist (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * (i,(j + 1)))) = dist (p,q) by TOPREAL6:def_1;
A7: (Gauge (C,n)) * (i,j) = |[((W-bound C) + ((((E-bound C) - (W-bound C)) / (2 |^ n)) * (i - 2))),((S-bound C) + ((((N-bound C) - (S-bound C)) / (2 |^ n)) * (j - 2)))]| by A1, JORDAN8:def_1;
dist (p,q) = (Pitag_dist 2) . (p,q) by METRIC_1:def_1
.= sqrt ((((((Gauge (C,n)) * (i,j)) `1) - (((Gauge (C,n)) * (i,(j + 1))) `1)) ^2) + (((((Gauge (C,n)) * (i,j)) `2) - (((Gauge (C,n)) * (i,(j + 1))) `2)) ^2)) by A5, TOPREAL3:7
.= sqrt (((((W-bound C) + ((((E-bound C) - (W-bound C)) / (2 |^ n)) * (i - 2))) - (((Gauge (C,n)) * (i,(j + 1))) `1)) ^2) + (((((Gauge (C,n)) * (i,j)) `2) - (((Gauge (C,n)) * (i,(j + 1))) `2)) ^2)) by A7, EUCLID:52
.= sqrt (((((W-bound C) + ((((E-bound C) - (W-bound C)) / (2 |^ n)) * (i - 2))) - ((W-bound C) + ((((E-bound C) - (W-bound C)) / (2 |^ n)) * (i - 2)))) ^2) + (((((Gauge (C,n)) * (i,j)) `2) - (((Gauge (C,n)) * (i,(j + 1))) `2)) ^2)) by A3, EUCLID:52
.= abs ((((Gauge (C,n)) * (i,j)) `2) - (((Gauge (C,n)) * (i,(j + 1))) `2)) by COMPLEX1:72
.= abs (((S-bound C) + ((((N-bound C) - (S-bound C)) / (2 |^ n)) * (j - 2))) - (((Gauge (C,n)) * (i,(j + 1))) `2)) by A7, EUCLID:52
.= abs (((S-bound C) + ((((N-bound C) - (S-bound C)) / (2 |^ n)) * (j - 2))) - ((S-bound C) + ((((N-bound C) - (S-bound C)) / (2 |^ n)) * ((j + 1) - 2)))) by A3, EUCLID:52
.= abs (- (((N-bound C) - (S-bound C)) / (2 |^ n)))
.= abs (((N-bound C) - (S-bound C)) / (2 |^ n)) by COMPLEX1:52
.= (abs ((N-bound C) - (S-bound C))) / (abs (2 |^ n)) by COMPLEX1:67
.= ((N-bound C) - (S-bound C)) / (abs (2 |^ n)) by A4, ABSVALUE:def_1 ;
hence dist (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * (i,(j + 1)))) = ((N-bound C) - (S-bound C)) / (2 |^ n) by A6, ABSVALUE:def_1; ::_thesis: verum
end;
theorem Th10: :: GOBRD14:10
for i, j, n being Element of NAT
for C being compact non horizontal non vertical Subset of (TOP-REAL 2) st [i,j] in Indices (Gauge (C,n)) & [(i + 1),j] in Indices (Gauge (C,n)) holds
dist (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * ((i + 1),j))) = ((E-bound C) - (W-bound C)) / (2 |^ n)
proof
let i, j, n be Element of NAT ; ::_thesis: for C being compact non horizontal non vertical Subset of (TOP-REAL 2) st [i,j] in Indices (Gauge (C,n)) & [(i + 1),j] in Indices (Gauge (C,n)) holds
dist (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * ((i + 1),j))) = ((E-bound C) - (W-bound C)) / (2 |^ n)
let C be compact non horizontal non vertical Subset of (TOP-REAL 2); ::_thesis: ( [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) )
set G = Gauge (C,n);
set a = N-bound C;
set e = E-bound C;
set s = S-bound C;
set w = W-bound C;
set p1 = (Gauge (C,n)) * (i,j);
set p2 = (Gauge (C,n)) * ((i + 1),j);
assume that
A1: [i,j] in Indices (Gauge (C,n)) and
A2: [(i + 1),j] in Indices (Gauge (C,n)) ; ::_thesis: dist (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * ((i + 1),j))) = ((E-bound C) - (W-bound C)) / (2 |^ n)
A3: (Gauge (C,n)) * ((i + 1),j) = |[((W-bound C) + ((((E-bound C) - (W-bound C)) / (2 |^ n)) * ((i + 1) - 2))),((S-bound C) + ((((N-bound C) - (S-bound C)) / (2 |^ n)) * (j - 2)))]| by A2, JORDAN8:def_1;
E-bound C >= W-bound C by SPRECT_1:21;
then A4: (E-bound C) - (W-bound C) >= (W-bound C) - (W-bound C) by XREAL_1:9;
set x = ((E-bound C) - (W-bound C)) / (2 |^ n);
consider p, q being Point of (Euclid 2) such that
A5: ( p = (Gauge (C,n)) * (i,j) & q = (Gauge (C,n)) * ((i + 1),j) ) and
A6: dist (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * ((i + 1),j))) = dist (p,q) by TOPREAL6:def_1;
A7: (Gauge (C,n)) * (i,j) = |[((W-bound C) + ((((E-bound C) - (W-bound C)) / (2 |^ n)) * (i - 2))),((S-bound C) + ((((N-bound C) - (S-bound C)) / (2 |^ n)) * (j - 2)))]| by A1, JORDAN8:def_1;
dist (p,q) = (Pitag_dist 2) . (p,q) by METRIC_1:def_1
.= sqrt ((((((Gauge (C,n)) * (i,j)) `1) - (((Gauge (C,n)) * ((i + 1),j)) `1)) ^2) + (((((Gauge (C,n)) * (i,j)) `2) - (((Gauge (C,n)) * ((i + 1),j)) `2)) ^2)) by A5, TOPREAL3:7
.= sqrt ((((((Gauge (C,n)) * (i,j)) `1) - (((Gauge (C,n)) * ((i + 1),j)) `1)) ^2) + ((((S-bound C) + ((((N-bound C) - (S-bound C)) / (2 |^ n)) * (j - 2))) - (((Gauge (C,n)) * ((i + 1),j)) `2)) ^2)) by A7, EUCLID:52
.= sqrt ((((((Gauge (C,n)) * (i,j)) `1) - (((Gauge (C,n)) * ((i + 1),j)) `1)) ^2) + ((((S-bound C) + ((((N-bound C) - (S-bound C)) / (2 |^ n)) * (j - 2))) - ((S-bound C) + ((((N-bound C) - (S-bound C)) / (2 |^ n)) * (j - 2)))) ^2)) by A3, EUCLID:52
.= abs ((((Gauge (C,n)) * (i,j)) `1) - (((Gauge (C,n)) * ((i + 1),j)) `1)) by COMPLEX1:72
.= abs (((W-bound C) + ((((E-bound C) - (W-bound C)) / (2 |^ n)) * (i - 2))) - (((Gauge (C,n)) * ((i + 1),j)) `1)) by A7, EUCLID:52
.= abs (((W-bound C) + ((((E-bound C) - (W-bound C)) / (2 |^ n)) * (i - 2))) - ((W-bound C) + ((((E-bound C) - (W-bound C)) / (2 |^ n)) * ((i + 1) - 2)))) by A3, EUCLID:52
.= abs (- (((E-bound C) - (W-bound C)) / (2 |^ n)))
.= abs (((E-bound C) - (W-bound C)) / (2 |^ n)) by COMPLEX1:52
.= (abs ((E-bound C) - (W-bound C))) / (abs (2 |^ n)) by COMPLEX1:67
.= ((E-bound C) - (W-bound C)) / (abs (2 |^ n)) by A4, ABSVALUE:def_1 ;
hence dist (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * ((i + 1),j))) = ((E-bound C) - (W-bound C)) / (2 |^ n) by A6, ABSVALUE:def_1; ::_thesis: verum
end;
theorem :: GOBRD14:11
for C being compact non horizontal non vertical Subset of (TOP-REAL 2)
for r, t being real number st r > 0 & t > 0 holds
ex n being Element of 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 C be compact non horizontal non vertical Subset of (TOP-REAL 2); ::_thesis: for r, t being real number st r > 0 & t > 0 holds
ex n being Element of 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 )
let r, t be real number ; ::_thesis: ( r > 0 & t > 0 implies ex n being Element of 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 ) )
assume that
A1: r > 0 and
A2: t > 0 ; ::_thesis: ex n being Element of 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 )
set n = N-bound C;
set e = E-bound C;
set s = S-bound C;
set w = W-bound C;
set a = (abs [\(log (2,(((N-bound C) - (S-bound C)) / r)))/]) + 1;
set b = (abs [\(log (2,(((E-bound C) - (W-bound C)) / t)))/]) + 1;
take i = (max (((abs [\(log (2,(((N-bound C) - (S-bound C)) / r)))/]) + 1),((abs [\(log (2,(((E-bound C) - (W-bound C)) / t)))/]) + 1))) + 1; ::_thesis: ( 1 < i & dist (((Gauge (C,i)) * (1,1)),((Gauge (C,i)) * (1,2))) < r & dist (((Gauge (C,i)) * (1,1)),((Gauge (C,i)) * (2,1))) < t )
A3: 2 to_power i > 0 by POWER:34;
then A4: 2 |^ i > 0 by POWER:41;
[\(log (2,(((N-bound C) - (S-bound C)) / r)))/] <= abs [\(log (2,(((N-bound C) - (S-bound C)) / r)))/] by ABSVALUE:4;
then A5: [\(log (2,(((N-bound C) - (S-bound C)) / r)))/] + 1 <= (abs [\(log (2,(((N-bound C) - (S-bound C)) / r)))/]) + 1 by XREAL_1:6;
[\(log (2,(((N-bound C) - (S-bound C)) / r)))/] > (log (2,(((N-bound C) - (S-bound C)) / r))) - 1 by INT_1:def_6;
then [\(log (2,(((N-bound C) - (S-bound C)) / r)))/] + 1 > ((log (2,(((N-bound C) - (S-bound C)) / r))) - 1) + 1 by XREAL_1:6;
then A6: (abs [\(log (2,(((N-bound C) - (S-bound C)) / r)))/]) + 1 > ((log (2,(((N-bound C) - (S-bound C)) / r))) - 1) + 1 by A5, XXREAL_0:2;
(abs [\(log (2,(((N-bound C) - (S-bound C)) / r)))/]) + 1 <= max (((abs [\(log (2,(((N-bound C) - (S-bound C)) / r)))/]) + 1),((abs [\(log (2,(((E-bound C) - (W-bound C)) / t)))/]) + 1)) by XXREAL_0:25;
then A7: ((abs [\(log (2,(((N-bound C) - (S-bound C)) / r)))/]) + 1) + 1 <= (max (((abs [\(log (2,(((N-bound C) - (S-bound C)) / r)))/]) + 1),((abs [\(log (2,(((E-bound C) - (W-bound C)) / t)))/]) + 1))) + 1 by XREAL_1:6;
(abs [\(log (2,(((N-bound C) - (S-bound C)) / r)))/]) + 1 < ((abs [\(log (2,(((N-bound C) - (S-bound C)) / r)))/]) + 1) + 1 by XREAL_1:29;
then i > (abs [\(log (2,(((N-bound C) - (S-bound C)) / r)))/]) + 1 by A7, XXREAL_0:2;
then i > log (2,(((N-bound C) - (S-bound C)) / r)) by A6, XXREAL_0:2;
then log (2,(2 to_power i)) > log (2,(((N-bound C) - (S-bound C)) / r)) by A3, POWER:def_3;
then 2 to_power i > ((N-bound C) - (S-bound C)) / r by A3, PRE_FF:10;
then 2 |^ i > ((N-bound C) - (S-bound C)) / r by POWER:41;
then (2 |^ i) * r > (((N-bound C) - (S-bound C)) / r) * r by A1, XREAL_1:68;
then (2 |^ i) * r > (N-bound C) - (S-bound C) by A1, XCMPLX_1:87;
then ((2 |^ i) * r) / (2 |^ i) > ((N-bound C) - (S-bound C)) / (2 |^ i) by A4, XREAL_1:74;
then A8: ((N-bound C) - (S-bound C)) / (2 |^ i) < r by A4, XCMPLX_1:89;
( (abs [\(log (2,(((N-bound C) - (S-bound C)) / r)))/]) + 1 >= 0 + 1 & max (((abs [\(log (2,(((N-bound C) - (S-bound C)) / r)))/]) + 1),((abs [\(log (2,(((E-bound C) - (W-bound C)) / t)))/]) + 1)) >= (abs [\(log (2,(((N-bound C) - (S-bound C)) / r)))/]) + 1 ) by XREAL_1:7, XXREAL_0:25;
then max (((abs [\(log (2,(((N-bound C) - (S-bound C)) / r)))/]) + 1),((abs [\(log (2,(((E-bound C) - (W-bound C)) / t)))/]) + 1)) >= 1 by XXREAL_0:2;
then (max (((abs [\(log (2,(((N-bound C) - (S-bound C)) / r)))/]) + 1),((abs [\(log (2,(((E-bound C) - (W-bound C)) / t)))/]) + 1))) + 1 >= 1 + 1 by XREAL_1:7;
hence 1 < i by XXREAL_0:2; ::_thesis: ( dist (((Gauge (C,i)) * (1,1)),((Gauge (C,i)) * (1,2))) < r & dist (((Gauge (C,i)) * (1,1)),((Gauge (C,i)) * (2,1))) < t )
A9: len (Gauge (C,i)) >= 4 by JORDAN8:10;
then A10: 1 <= len (Gauge (C,i)) by XXREAL_0:2;
[\(log (2,(((E-bound C) - (W-bound C)) / t)))/] <= abs [\(log (2,(((E-bound C) - (W-bound C)) / t)))/] by ABSVALUE:4;
then A11: [\(log (2,(((E-bound C) - (W-bound C)) / t)))/] + 1 <= (abs [\(log (2,(((E-bound C) - (W-bound C)) / t)))/]) + 1 by XREAL_1:6;
[\(log (2,(((E-bound C) - (W-bound C)) / t)))/] > (log (2,(((E-bound C) - (W-bound C)) / t))) - 1 by INT_1:def_6;
then [\(log (2,(((E-bound C) - (W-bound C)) / t)))/] + 1 > ((log (2,(((E-bound C) - (W-bound C)) / t))) - 1) + 1 by XREAL_1:6;
then A12: (abs [\(log (2,(((E-bound C) - (W-bound C)) / t)))/]) + 1 > ((log (2,(((E-bound C) - (W-bound C)) / t))) - 1) + 1 by A11, XXREAL_0:2;
(abs [\(log (2,(((E-bound C) - (W-bound C)) / t)))/]) + 1 <= max (((abs [\(log (2,(((N-bound C) - (S-bound C)) / r)))/]) + 1),((abs [\(log (2,(((E-bound C) - (W-bound C)) / t)))/]) + 1)) by XXREAL_0:25;
then A13: ((abs [\(log (2,(((E-bound C) - (W-bound C)) / t)))/]) + 1) + 1 <= (max (((abs [\(log (2,(((N-bound C) - (S-bound C)) / r)))/]) + 1),((abs [\(log (2,(((E-bound C) - (W-bound C)) / t)))/]) + 1))) + 1 by XREAL_1:6;
(abs [\(log (2,(((E-bound C) - (W-bound C)) / t)))/]) + 1 < ((abs [\(log (2,(((E-bound C) - (W-bound C)) / t)))/]) + 1) + 1 by XREAL_1:29;
then i > (abs [\(log (2,(((E-bound C) - (W-bound C)) / t)))/]) + 1 by A13, XXREAL_0:2;
then i > log (2,(((E-bound C) - (W-bound C)) / t)) by A12, XXREAL_0:2;
then log (2,(2 to_power i)) > log (2,(((E-bound C) - (W-bound C)) / t)) by A3, POWER:def_3;
then 2 to_power i > ((E-bound C) - (W-bound C)) / t by A3, PRE_FF:10;
then 2 |^ i > ((E-bound C) - (W-bound C)) / t by POWER:41;
then (2 |^ i) * t > (((E-bound C) - (W-bound C)) / t) * t by A2, XREAL_1:68;
then (2 |^ i) * t > (E-bound C) - (W-bound C) by A2, XCMPLX_1:87;
then ((2 |^ i) * t) / (2 |^ i) > ((E-bound C) - (W-bound C)) / (2 |^ i) by A4, XREAL_1:74;
then A14: ((E-bound C) - (W-bound C)) / (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_1:36;
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_1:36;
[(1 + 1),1] in Indices (Gauge (C,i)) by A15, A10, A17, MATRIX_1:36;
hence ( dist (((Gauge (C,i)) * (1,1)),((Gauge (C,i)) * (1,2))) < r & dist (((Gauge (C,i)) * (1,1)),((Gauge (C,i)) * (2,1))) < t ) by A8, A14, A16, A18, Th9, Th10; ::_thesis: verum
end;
begin
theorem Th12: :: GOBRD14:12
for f being non constant standard special_circular_sequence
for P being Subset of ((TOP-REAL 2) | ((L~ f) `)) holds
( not P is a_component or P = RightComp f or P = LeftComp f )
proof
let f be non constant standard special_circular_sequence; ::_thesis: for P being Subset of ((TOP-REAL 2) | ((L~ f) `)) holds
( not P is a_component or P = RightComp f or P = LeftComp f )
let P be Subset of ((TOP-REAL 2) | ((L~ f) `)); ::_thesis: ( not P is a_component or P = RightComp f or P = LeftComp f )
assume that
A1: P is a_component and
A2: P <> RightComp f ; ::_thesis: P = LeftComp 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 P = LeftComp f by A1, A5, CONNSP_1:35; ::_thesis: verum
end;
theorem :: GOBRD14:13
for f being non constant standard special_circular_sequence
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 ) ) & not ( A1 = RightComp f & A2 = LeftComp f ) holds
( A1 = LeftComp f & A2 = RightComp f )
proof
let f be non constant standard special_circular_sequence; ::_thesis: 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 ) ) & not ( A1 = RightComp f & A2 = LeftComp f ) holds
( A1 = LeftComp f & A2 = RightComp f )
let A1, A2 be Subset of (TOP-REAL 2); ::_thesis: ( (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 ) ) & not ( A1 = RightComp f & A2 = LeftComp f ) implies ( A1 = LeftComp f & A2 = RightComp f ) )
assume 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 ) ; :: according to XBOOLE_0:def_7 ::_thesis: ( ( A1 = RightComp f & A2 = LeftComp f ) or ( A1 = LeftComp f & A2 = RightComp f ) )
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 ( A1 = RightComp f & A2 = LeftComp f ) & not ( A1 = LeftComp f & A2 = RightComp f ) ) ; ::_thesis: contradiction
hence contradiction by A2, A5, A4; ::_thesis: verum
end;
theorem Th14: :: GOBRD14:14
for f being non constant standard special_circular_sequence holds LeftComp f misses RightComp f
proof
let f be non constant standard special_circular_sequence; ::_thesis: LeftComp f misses RightComp f
assume (LeftComp f) /\ (RightComp f) <> {} ; :: according to XBOOLE_0:def_7 ::_thesis: contradiction
then consider x being set such that
A1: x in (LeftComp f) /\ (RightComp f) by XBOOLE_0:def_1;
now__::_thesis:_ex_x_being_set_st_
(_x_in_LeftComp_f_&_x_in_RightComp_f_)
take x = x; ::_thesis: ( x in LeftComp f & x in RightComp f )
thus ( x in LeftComp f & x in RightComp f ) by A1, XBOOLE_0:def_4; ::_thesis: verum
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, GOBOARD9:def_2;
hence contradiction by A2, GOBOARD9:1, SPRECT_4:6; ::_thesis: verum
end;
theorem Th15: :: GOBRD14:15
for f being non constant standard special_circular_sequence holds ((L~ f) \/ (RightComp f)) \/ (LeftComp f) = the carrier of (TOP-REAL 2)
proof
let f be non constant standard special_circular_sequence; ::_thesis: ((L~ f) \/ (RightComp f)) \/ (LeftComp f) = the carrier of (TOP-REAL 2)
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 ((L~ f) \/ (RightComp f)) \/ (LeftComp f) = the carrier of (TOP-REAL 2) by A1, XBOOLE_1:4; ::_thesis: verum
end;
theorem Th16: :: GOBRD14:16
for f being non constant standard special_circular_sequence
for p being Point of (TOP-REAL 2) holds
( p in L~ f iff ( not p in LeftComp f & not p in RightComp f ) )
proof
let f be non constant standard special_circular_sequence; ::_thesis: for p being Point of (TOP-REAL 2) holds
( p in L~ f iff ( not p in LeftComp f & not p in RightComp f ) )
let p be Point of (TOP-REAL 2); ::_thesis: ( p in L~ f iff ( not p in LeftComp f & not p in RightComp f ) )
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 ( p in L~ f iff ( not p in LeftComp f & not p in RightComp f ) ) by A1, XBOOLE_0:def_3; ::_thesis: verum
end;
theorem Th17: :: GOBRD14:17
for f being non constant standard special_circular_sequence
for p being Point of (TOP-REAL 2) holds
( p in LeftComp f iff ( not p in L~ f & not p in RightComp f ) )
proof
let f be non constant standard special_circular_sequence; ::_thesis: for p being Point of (TOP-REAL 2) holds
( p in LeftComp f iff ( not p in L~ f & not p in RightComp f ) )
let p be Point of (TOP-REAL 2); ::_thesis: ( p in LeftComp f iff ( not p in L~ f & not p in RightComp f ) )
LeftComp f misses RightComp f by Th14;
then A1: ( (L~ f) ` = (LeftComp f) \/ (RightComp f) & (LeftComp f) /\ (RightComp f) = {} ) by GOBRD12:10, XBOOLE_0:def_7;
( p in L~ f iff not p in (L~ f) ` ) by XBOOLE_0:def_5;
hence ( p in LeftComp f iff ( not p in L~ f & not p in RightComp f ) ) by A1, XBOOLE_0:def_3, XBOOLE_0:def_4; ::_thesis: verum
end;
theorem :: GOBRD14:18
for f being non constant standard special_circular_sequence
for p being Point of (TOP-REAL 2) holds
( p in RightComp f iff ( not p in L~ f & not p in LeftComp f ) ) by Th16, Th17;
theorem Th19: :: GOBRD14:19
for f being non constant standard special_circular_sequence holds L~ f = (Cl (RightComp f)) \ (RightComp f)
proof
let f be non constant standard special_circular_sequence; ::_thesis: L~ f = (Cl (RightComp f)) \ (RightComp f)
thus L~ f c= (Cl (RightComp f)) \ (RightComp f) :: according to XBOOLE_0:def_10 ::_thesis: (Cl (RightComp f)) \ (RightComp f) c= L~ f
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in L~ f or x in (Cl (RightComp f)) \ (RightComp f) )
assume A1: x in L~ f ; ::_thesis: x in (Cl (RightComp f)) \ (RightComp f)
then reconsider p = x as Point of (TOP-REAL 2) ;
consider i being Element of NAT 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 & p in O holds
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 Element of 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_1:38;
A11: j2 <= width (GoB f) by A7, MATRIX_1:38;
A12: 1 <= j1 by A5, MATRIX_1:38;
A13: j1 <= width (GoB f) by A5, MATRIX_1:38;
A14: i1 <= len (GoB f) by A5, MATRIX_1:38;
A15: i2 <= len (GoB f) by A7, MATRIX_1:38;
A16: now__::_thesis:_(_(_i1_=_i2_&_j1_+_1_=_j2_&_p_in_Cl_(Int_(right_cell_(f,i)))_)_or_(_i1_+_1_=_i2_&_j1_=_j2_&_p_in_Cl_(Int_(right_cell_(f,i)))_)_or_(_i1_=_i2_+_1_&_j1_=_j2_&_p_in_Cl_(Int_(right_cell_(f,i)))_)_or_(_i1_=_i2_&_j1_=_j2_+_1_&_p_in_Cl_(Int_(right_cell_(f,i)))_)_)
percases ( ( i1 = i2 & j1 + 1 = j2 ) or ( i1 + 1 = i2 & j1 = j2 ) or ( i1 = i2 + 1 & j1 = j2 ) or ( i1 = i2 & j1 = j2 + 1 ) ) by A9;
caseA17: ( i1 = i2 & j1 + 1 = j2 ) ; ::_thesis: p in Cl (Int (right_cell (f,i)))
set w = i1 -' 1;
A18: (i1 -' 1) + 1 = i1 by A10, XREAL_1:235;
then right_cell (f,i) = cell ((GoB f),((i1 -' 1) + 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; ::_thesis: verum
end;
caseA19: ( i1 + 1 = i2 & j1 = j2 ) ; ::_thesis: p in Cl (Int (right_cell (f,i)))
set w = j1 -' 1;
( j1 -' 1 <= (j1 -' 1) + 1 & (j1 -' 1) + 1 <= width (GoB f) ) by A12, A13, NAT_1:11, XREAL_1:235;
then A20: j1 -' 1 <= width (GoB f) by XXREAL_0:2;
(j1 -' 1) + 1 = j1 by A12, XREAL_1:235;
then right_cell (f,i) = cell ((GoB f),i1,(j1 -' 1)) by A2, A5, A6, A7, A8, A19, GOBOARD5:28;
hence p in Cl (Int (right_cell (f,i))) by A4, A14, A20, GOBRD11:35; ::_thesis: verum
end;
caseA21: ( i1 = i2 + 1 & j1 = j2 ) ; ::_thesis: p in Cl (Int (right_cell (f,i)))
set w = j1 -' 1;
A22: (j1 -' 1) + 1 = j1 by A12, XREAL_1:235;
then right_cell (f,i) = cell ((GoB f),i2,((j1 -' 1) + 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; ::_thesis: verum
end;
caseA23: ( i1 = i2 & j1 = j2 + 1 ) ; ::_thesis: p in Cl (Int (right_cell (f,i)))
set z = i1 -' 1;
( i1 -' 1 <= (i1 -' 1) + 1 & (i1 -' 1) + 1 <= len (GoB f) ) by A10, A14, NAT_1:11, XREAL_1:235;
then A24: i1 -' 1 <= len (GoB f) by XXREAL_0:2;
(i1 -' 1) + 1 = i1 by A10, XREAL_1:235;
then right_cell (f,i) = cell ((GoB f),(i1 -' 1),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; ::_thesis: verum
end;
end;
end;
let O be Subset of (TOP-REAL 2); ::_thesis: ( O is open & p in O implies RightComp f meets O )
assume ( O is open & p in O ) ; ::_thesis: RightComp f meets O
then O meets Int (right_cell (f,i)) by A16, PRE_TOPC:def_7;
hence RightComp f meets O by A2, GOBOARD9:25, XBOOLE_1:63; ::_thesis: verum
end;
then A25: p in Cl (RightComp f) by PRE_TOPC:def_7;
not x in RightComp f by A1, Th16;
hence x in (Cl (RightComp f)) \ (RightComp f) by A25, XBOOLE_0:def_5; ::_thesis: verum
end;
assume not (Cl (RightComp f)) \ (RightComp f) c= L~ f ; ::_thesis: contradiction
then consider q being set such that
A26: q in (Cl (RightComp f)) \ (RightComp f) and
A27: not q in L~ f by TARSKI:def_3;
reconsider q = 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; ::_thesis: verum
end;
theorem Th20: :: GOBRD14:20
for f being non constant standard special_circular_sequence holds L~ f = (Cl (LeftComp f)) \ (LeftComp f)
proof
let f be non constant standard special_circular_sequence; ::_thesis: L~ f = (Cl (LeftComp f)) \ (LeftComp f)
thus L~ f c= (Cl (LeftComp f)) \ (LeftComp f) :: according to XBOOLE_0:def_10 ::_thesis: (Cl (LeftComp f)) \ (LeftComp f) c= L~ f
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in L~ f or x in (Cl (LeftComp f)) \ (LeftComp f) )
assume A1: x in L~ f ; ::_thesis: x in (Cl (LeftComp f)) \ (LeftComp f)
then reconsider p = x as Point of (TOP-REAL 2) ;
consider i being Element of NAT 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 & p in O holds
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 Element of 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_1:38;
A11: j2 <= width (GoB f) by A7, MATRIX_1:38;
A12: 1 <= j1 by A5, MATRIX_1:38;
A13: j1 <= width (GoB f) by A5, MATRIX_1:38;
A14: i1 <= len (GoB f) by A5, MATRIX_1:38;
A15: i2 <= len (GoB f) by A7, MATRIX_1:38;
A16: now__::_thesis:_(_(_i1_=_i2_&_j1_+_1_=_j2_&_p_in_Cl_(Int_(left_cell_(f,i)))_)_or_(_i1_+_1_=_i2_&_j1_=_j2_&_p_in_Cl_(Int_(left_cell_(f,i)))_)_or_(_i1_=_i2_+_1_&_j1_=_j2_&_p_in_Cl_(Int_(left_cell_(f,i)))_)_or_(_i1_=_i2_&_j1_=_j2_+_1_&_p_in_Cl_(Int_(left_cell_(f,i)))_)_)
percases ( ( i1 = i2 & j1 + 1 = j2 ) or ( i1 + 1 = i2 & j1 = j2 ) or ( i1 = i2 + 1 & j1 = j2 ) or ( i1 = i2 & j1 = j2 + 1 ) ) by A9;
caseA17: ( i1 = i2 & j1 + 1 = j2 ) ; ::_thesis: p in Cl (Int (left_cell (f,i)))
set w = i1 -' 1;
( i1 -' 1 <= (i1 -' 1) + 1 & (i1 -' 1) + 1 <= len (GoB f) ) by A10, A14, NAT_1:11, XREAL_1:235;
then A18: i1 -' 1 <= len (GoB f) by XXREAL_0:2;
(i1 -' 1) + 1 = i1 by A10, XREAL_1:235;
then left_cell (f,i) = cell ((GoB f),(i1 -' 1),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; ::_thesis: verum
end;
caseA19: ( i1 + 1 = i2 & j1 = j2 ) ; ::_thesis: p in Cl (Int (left_cell (f,i)))
set w = j1 -' 1;
(j1 -' 1) + 1 = j1 by A12, XREAL_1:235;
then A20: left_cell (f,i) = cell ((GoB f),i1,((j1 -' 1) + 1)) by A2, A5, A6, A7, A8, A19, GOBOARD5:28;
(j1 -' 1) + 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; ::_thesis: verum
end;
caseA21: ( i1 = i2 + 1 & j1 = j2 ) ; ::_thesis: p in Cl (Int (left_cell (f,i)))
set w = j1 -' 1;
( j1 -' 1 <= (j1 -' 1) + 1 & (j1 -' 1) + 1 <= width (GoB f) ) by A12, A13, NAT_1:11, XREAL_1:235;
then A22: j1 -' 1 <= width (GoB f) by XXREAL_0:2;
(j1 -' 1) + 1 = j1 by A12, XREAL_1:235;
then left_cell (f,i) = cell ((GoB f),i2,(j1 -' 1)) by A2, A5, A6, A7, A8, A21, GOBOARD5:29;
hence p in Cl (Int (left_cell (f,i))) by A4, A15, A22, GOBRD11:35; ::_thesis: verum
end;
caseA23: ( i1 = i2 & j1 = j2 + 1 ) ; ::_thesis: p in Cl (Int (left_cell (f,i)))
set z = i1 -' 1;
(i1 -' 1) + 1 = i1 by A10, XREAL_1:235;
then A24: left_cell (f,i) = cell ((GoB f),((i1 -' 1) + 1),j2) by A2, A5, A6, A7, A8, A23, GOBOARD5:30;
(i1 -' 1) + 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; ::_thesis: verum
end;
end;
end;
let O be Subset of (TOP-REAL 2); ::_thesis: ( O is open & p in O implies LeftComp f meets O )
assume ( O is open & p in O ) ; ::_thesis: LeftComp f meets O
then O meets Int (left_cell (f,i)) by A16, PRE_TOPC:def_7;
hence LeftComp f meets O by A2, GOBOARD9:21, XBOOLE_1:63; ::_thesis: verum
end;
then A25: p in Cl (LeftComp f) by PRE_TOPC:def_7;
not x in LeftComp f by A1, Th16;
hence x in (Cl (LeftComp f)) \ (LeftComp f) by A25, XBOOLE_0:def_5; ::_thesis: verum
end;
assume not (Cl (LeftComp f)) \ (LeftComp f) c= L~ f ; ::_thesis: contradiction
then consider q being set such that
A26: q in (Cl (LeftComp f)) \ (LeftComp f) and
A27: not q in L~ f by TARSKI:def_3;
reconsider q = 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; ::_thesis: verum
end;
theorem Th21: :: GOBRD14:21
for f being non constant standard special_circular_sequence holds Cl (RightComp f) = (RightComp f) \/ (L~ f)
proof
let f be non constant standard special_circular_sequence; ::_thesis: Cl (RightComp f) = (RightComp f) \/ (L~ f)
thus Cl (RightComp f) c= (RightComp f) \/ (L~ f) :: according to XBOOLE_0:def_10 ::_thesis: (RightComp f) \/ (L~ f) c= Cl (RightComp f)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Cl (RightComp f) or x in (RightComp f) \/ (L~ f) )
assume A1: x in Cl (RightComp f) ; ::_thesis: x in (RightComp f) \/ (L~ f)
now__::_thesis:_(_not_x_in_RightComp_f_implies_x_in_L~_f_)
A2: now__::_thesis:_not_x_in_LeftComp_f
assume x in LeftComp f ; ::_thesis: contradiction
then LeftComp f meets RightComp f by A1, TOPS_1:12;
hence contradiction by Th14; ::_thesis: verum
end;
assume not x in RightComp f ; ::_thesis: x in L~ f
hence x in L~ f by A1, A2, Th16; ::_thesis: verum
end;
hence x in (RightComp f) \/ (L~ f) by XBOOLE_0:def_3; ::_thesis: verum
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 (RightComp f) \/ (L~ f) c= Cl (RightComp f) by XBOOLE_1:8; ::_thesis: verum
end;
theorem :: GOBRD14:22
for f being non constant standard special_circular_sequence holds Cl (LeftComp f) = (LeftComp f) \/ (L~ f)
proof
let f be non constant standard special_circular_sequence; ::_thesis: Cl (LeftComp f) = (LeftComp f) \/ (L~ f)
thus Cl (LeftComp f) c= (LeftComp f) \/ (L~ f) :: according to XBOOLE_0:def_10 ::_thesis: (LeftComp f) \/ (L~ f) c= Cl (LeftComp f)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Cl (LeftComp f) or x in (LeftComp f) \/ (L~ f) )
assume A1: x in Cl (LeftComp f) ; ::_thesis: x in (LeftComp f) \/ (L~ f)
now__::_thesis:_(_not_x_in_LeftComp_f_implies_x_in_L~_f_)
A2: now__::_thesis:_not_x_in_RightComp_f
assume x in RightComp f ; ::_thesis: contradiction
then LeftComp f meets RightComp f by A1, TOPS_1:12;
hence contradiction by Th14; ::_thesis: verum
end;
assume not x in LeftComp f ; ::_thesis: x in L~ f
hence x in L~ f by A1, A2, Th16; ::_thesis: verum
end;
hence x in (LeftComp f) \/ (L~ f) by XBOOLE_0:def_3; ::_thesis: verum
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 (LeftComp f) \/ (L~ f) c= Cl (LeftComp f) by XBOOLE_1:8; ::_thesis: verum
end;
registration
let f be non constant standard special_circular_sequence;
cluster L~ f -> Jordan ;
coherence
L~ f is Jordan
proof
thus (L~ f) ` <> {} ; :: according to SPRECT_1:def_3 ::_thesis: ex b1, b2 being Element of K19( the carrier of (TOP-REAL 2)) st
( (L~ f) ` = b1 \/ b2 & b1 misses b2 & (Cl b1) \ b1 = (Cl b2) \ b2 & b1 is_a_component_of (L~ f) ` & b2 is_a_component_of (L~ f) ` )
take A1 = RightComp f; ::_thesis: ex b1 being Element of K19( the carrier of (TOP-REAL 2)) st
( (L~ f) ` = A1 \/ b1 & A1 misses b1 & (Cl A1) \ A1 = (Cl b1) \ b1 & A1 is_a_component_of (L~ f) ` & b1 is_a_component_of (L~ f) ` )
take A2 = LeftComp f; ::_thesis: ( (L~ f) ` = A1 \/ A2 & A1 misses A2 & (Cl A1) \ A1 = (Cl A2) \ A2 & A1 is_a_component_of (L~ f) ` & A2 is_a_component_of (L~ f) ` )
thus (L~ f) ` = A1 \/ A2 by GOBRD12:10; ::_thesis: ( A1 misses A2 & (Cl A1) \ A1 = (Cl A2) \ A2 & A1 is_a_component_of (L~ f) ` & A2 is_a_component_of (L~ f) ` )
L~ f = (Cl A1) \ A1 by Th19;
hence ( A1 misses A2 & (Cl A1) \ A1 = (Cl A2) \ A2 & A1 is_a_component_of (L~ f) ` & A2 is_a_component_of (L~ f) ` ) by Th14, Th20, GOBOARD9:def_1, GOBOARD9:def_2; ::_thesis: verum
end;
end;
theorem Th23: :: GOBRD14:23
for p being Point of (TOP-REAL 2)
for f being non constant standard clockwise_oriented special_circular_sequence st p in RightComp f holds
W-bound (L~ f) < p `1
proof
let p be Point of (TOP-REAL 2); ::_thesis: for f being non constant standard clockwise_oriented special_circular_sequence st p in RightComp f holds
W-bound (L~ f) < p `1
let f be non constant standard clockwise_oriented special_circular_sequence; ::_thesis: ( p in RightComp f implies W-bound (L~ f) < p `1 )
set g = Rotate (f,(N-min (L~ f)));
A1: L~ f = L~ (Rotate (f,(N-min (L~ f)))) by REVROT_1:33;
reconsider u = p as Point of (Euclid 2) by EUCLID:22;
assume p in RightComp f ; ::_thesis: W-bound (L~ f) < p `1
then p in RightComp (Rotate (f,(N-min (L~ f)))) by REVROT_1:37;
then u in Int (RightComp (Rotate (f,(N-min (L~ f))))) by TOPS_1:23;
then consider r being real number such that
A2: r > 0 and
A3: Ball (u,r) c= RightComp (Rotate (f,(N-min (L~ f)))) by GOBOARD6:5;
reconsider r = r as Real by XREAL_0:def_1;
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)) by EUCLID:52
.= sqrt ((((p `1) - ((p `1) - (r / 2))) ^2) + (((p `2) - (p `2)) ^2)) by EUCLID:52
.= 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 (Rotate (f,(N-min (L~ f)))) misses LeftComp (Rotate (f,(N-min (L~ f)))) by Th14;
then A5: not |[((p `1) - (r / 2)),(p `2)]| in LeftComp (Rotate (f,(N-min (L~ f)))) by A3, A4, XBOOLE_0:3;
set x = |[((p `1) - (r / 2)),(N-bound (L~ (SpStSeq (L~ (Rotate (f,(N-min (L~ f))))))))]|;
A6: LSeg ((NW-corner (L~ (Rotate (f,(N-min (L~ f)))))),(NE-corner (L~ (Rotate (f,(N-min (L~ f))))))) c= L~ (SpStSeq (L~ (Rotate (f,(N-min (L~ f)))))) by SPRECT_3:14;
A7: proj1 . |[((p `1) - (r / 2)),(N-bound (L~ (SpStSeq (L~ (Rotate (f,(N-min (L~ f))))))))]| = |[((p `1) - (r / 2)),(N-bound (L~ (SpStSeq (L~ (Rotate (f,(N-min (L~ f))))))))]| `1 by PSCOMP_1:def_5
.= (p `1) - (r / 2) by EUCLID:52 ;
N-min (L~ f) in rng f by SPRECT_2:39;
then A8: (Rotate (f,(N-min (L~ f)))) /. 1 = N-min (L~ (Rotate (f,(N-min (L~ f))))) by A1, FINSEQ_6:92;
then |[((p `1) - (r / 2)),(p `2)]| `1 <= E-bound (L~ (Rotate (f,(N-min (L~ f))))) by A5, JORDAN2C:111;
then (p `1) - (r / 2) <= E-bound (L~ (Rotate (f,(N-min (L~ f))))) by EUCLID:52;
then A9: |[((p `1) - (r / 2)),(N-bound (L~ (SpStSeq (L~ (Rotate (f,(N-min (L~ f))))))))]| `1 <= E-bound (L~ (Rotate (f,(N-min (L~ f))))) by EUCLID:52;
|[((p `1) - (r / 2)),(N-bound (L~ (SpStSeq (L~ (Rotate (f,(N-min (L~ f))))))))]| `2 = N-bound (L~ (SpStSeq (L~ (Rotate (f,(N-min (L~ f))))))) by EUCLID:52;
then A10: |[((p `1) - (r / 2)),(N-bound (L~ (SpStSeq (L~ (Rotate (f,(N-min (L~ f))))))))]| `2 = N-bound (L~ (Rotate (f,(N-min (L~ f))))) by SPRECT_1:60;
|[((p `1) - (r / 2)),(p `2)]| `1 >= W-bound (L~ (Rotate (f,(N-min (L~ f))))) by A8, A5, JORDAN2C:110;
then (p `1) - (r / 2) >= W-bound (L~ (Rotate (f,(N-min (L~ f))))) by EUCLID:52;
then A11: |[((p `1) - (r / 2)),(N-bound (L~ (SpStSeq (L~ (Rotate (f,(N-min (L~ f))))))))]| `1 >= W-bound (L~ (Rotate (f,(N-min (L~ f))))) by EUCLID:52;
LSeg ((NW-corner (L~ (Rotate (f,(N-min (L~ f)))))),(NE-corner (L~ (Rotate (f,(N-min (L~ f))))))) = { q where q is Point of (TOP-REAL 2) : ( q `1 <= E-bound (L~ (Rotate (f,(N-min (L~ f))))) & q `1 >= W-bound (L~ (Rotate (f,(N-min (L~ f))))) & q `2 = N-bound (L~ (Rotate (f,(N-min (L~ f))))) ) } by SPRECT_1:25;
then |[((p `1) - (r / 2)),(N-bound (L~ (SpStSeq (L~ (Rotate (f,(N-min (L~ f))))))))]| in LSeg ((NW-corner (L~ (Rotate (f,(N-min (L~ f)))))),(NE-corner (L~ (Rotate (f,(N-min (L~ f))))))) by A9, A11, A10;
then ( proj1 .: (L~ (SpStSeq (L~ (Rotate (f,(N-min (L~ f))))))) is bounded_below & (p `1) - (r / 2) in proj1 .: (L~ (SpStSeq (L~ (Rotate (f,(N-min (L~ f))))))) ) by A6, A7, FUNCT_2:35;
then A12: lower_bound (proj1 .: (L~ (SpStSeq (L~ (Rotate (f,(N-min (L~ f)))))))) <= (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~ (Rotate (f,(N-min (L~ f))))))) = W-bound (L~ (Rotate (f,(N-min (L~ f))))) & W-bound (L~ (SpStSeq (L~ (Rotate (f,(N-min (L~ f))))))) = lower_bound (proj1 .: (L~ (SpStSeq (L~ (Rotate (f,(N-min (L~ f)))))))) ) by SPRECT_1:43, SPRECT_1:58;
hence W-bound (L~ f) < p `1 by A1, A12, A13, XXREAL_0:2; ::_thesis: verum
end;
theorem Th24: :: GOBRD14:24
for p being Point of (TOP-REAL 2)
for f being non constant standard clockwise_oriented special_circular_sequence st p in RightComp f holds
E-bound (L~ f) > p `1
proof
let p be Point of (TOP-REAL 2); ::_thesis: for f being non constant standard clockwise_oriented special_circular_sequence st p in RightComp f holds
E-bound (L~ f) > p `1
let f be non constant standard clockwise_oriented special_circular_sequence; ::_thesis: ( p in RightComp f implies E-bound (L~ f) > p `1 )
set g = Rotate (f,(N-min (L~ f)));
A1: L~ f = L~ (Rotate (f,(N-min (L~ f)))) by REVROT_1:33;
reconsider u = p as Point of (Euclid 2) by EUCLID:22;
assume p in RightComp f ; ::_thesis: E-bound (L~ f) > p `1
then p in RightComp (Rotate (f,(N-min (L~ f)))) by REVROT_1:37;
then u in Int (RightComp (Rotate (f,(N-min (L~ f))))) by TOPS_1:23;
then consider r being real number such that
A2: r > 0 and
A3: Ball (u,r) c= RightComp (Rotate (f,(N-min (L~ f)))) by GOBOARD6:5;
reconsider r = r as Real by XREAL_0:def_1;
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)) by EUCLID:52
.= sqrt ((((p `1) - ((p `1) + (r / 2))) ^2) + (((p `2) - (p `2)) ^2)) by EUCLID:52
.= 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 (Rotate (f,(N-min (L~ f)))) misses LeftComp (Rotate (f,(N-min (L~ f)))) by Th14;
then A5: not |[((p `1) + (r / 2)),(p `2)]| in LeftComp (Rotate (f,(N-min (L~ f)))) by A3, A4, XBOOLE_0:3;
set x = |[((p `1) + (r / 2)),(N-bound (L~ (SpStSeq (L~ (Rotate (f,(N-min (L~ f))))))))]|;
A6: LSeg ((NW-corner (L~ (Rotate (f,(N-min (L~ f)))))),(NE-corner (L~ (Rotate (f,(N-min (L~ f))))))) c= L~ (SpStSeq (L~ (Rotate (f,(N-min (L~ f)))))) by SPRECT_3:14;
A7: proj1 . |[((p `1) + (r / 2)),(N-bound (L~ (SpStSeq (L~ (Rotate (f,(N-min (L~ f))))))))]| = |[((p `1) + (r / 2)),(N-bound (L~ (SpStSeq (L~ (Rotate (f,(N-min (L~ f))))))))]| `1 by PSCOMP_1:def_5
.= (p `1) + (r / 2) by EUCLID:52 ;
N-min (L~ f) in rng f by SPRECT_2:39;
then A8: (Rotate (f,(N-min (L~ f)))) /. 1 = N-min (L~ (Rotate (f,(N-min (L~ f))))) by A1, FINSEQ_6:92;
then |[((p `1) + (r / 2)),(p `2)]| `1 <= E-bound (L~ (Rotate (f,(N-min (L~ f))))) by A5, JORDAN2C:111;
then (p `1) + (r / 2) <= E-bound (L~ (Rotate (f,(N-min (L~ f))))) by EUCLID:52;
then A9: |[((p `1) + (r / 2)),(N-bound (L~ (SpStSeq (L~ (Rotate (f,(N-min (L~ f))))))))]| `1 <= E-bound (L~ (Rotate (f,(N-min (L~ f))))) by EUCLID:52;
|[((p `1) + (r / 2)),(N-bound (L~ (SpStSeq (L~ (Rotate (f,(N-min (L~ f))))))))]| `2 = N-bound (L~ (SpStSeq (L~ (Rotate (f,(N-min (L~ f))))))) by EUCLID:52;
then A10: |[((p `1) + (r / 2)),(N-bound (L~ (SpStSeq (L~ (Rotate (f,(N-min (L~ f))))))))]| `2 = N-bound (L~ (Rotate (f,(N-min (L~ f))))) by SPRECT_1:60;
|[((p `1) + (r / 2)),(p `2)]| `1 >= W-bound (L~ (Rotate (f,(N-min (L~ f))))) by A8, A5, JORDAN2C:110;
then (p `1) + (r / 2) >= W-bound (L~ (Rotate (f,(N-min (L~ f))))) by EUCLID:52;
then A11: |[((p `1) + (r / 2)),(N-bound (L~ (SpStSeq (L~ (Rotate (f,(N-min (L~ f))))))))]| `1 >= W-bound (L~ (Rotate (f,(N-min (L~ f))))) by EUCLID:52;
LSeg ((NW-corner (L~ (Rotate (f,(N-min (L~ f)))))),(NE-corner (L~ (Rotate (f,(N-min (L~ f))))))) = { q where q is Point of (TOP-REAL 2) : ( q `1 <= E-bound (L~ (Rotate (f,(N-min (L~ f))))) & q `1 >= W-bound (L~ (Rotate (f,(N-min (L~ f))))) & q `2 = N-bound (L~ (Rotate (f,(N-min (L~ f))))) ) } by SPRECT_1:25;
then |[((p `1) + (r / 2)),(N-bound (L~ (SpStSeq (L~ (Rotate (f,(N-min (L~ f))))))))]| in LSeg ((NW-corner (L~ (Rotate (f,(N-min (L~ f)))))),(NE-corner (L~ (Rotate (f,(N-min (L~ f))))))) by A9, A11, A10;
then ( proj1 .: (L~ (SpStSeq (L~ (Rotate (f,(N-min (L~ f))))))) is bounded_above & (p `1) + (r / 2) in proj1 .: (L~ (SpStSeq (L~ (Rotate (f,(N-min (L~ f))))))) ) by A6, A7, FUNCT_2:35;
then A12: upper_bound (proj1 .: (L~ (SpStSeq (L~ (Rotate (f,(N-min (L~ f)))))))) >= (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~ (Rotate (f,(N-min (L~ f))))))) = E-bound (L~ (Rotate (f,(N-min (L~ f))))) & E-bound (L~ (SpStSeq (L~ (Rotate (f,(N-min (L~ f))))))) = upper_bound (proj1 .: (L~ (SpStSeq (L~ (Rotate (f,(N-min (L~ f)))))))) ) by SPRECT_1:46, SPRECT_1:61;
hence E-bound (L~ f) > p `1 by A1, A12, A13, XXREAL_0:2; ::_thesis: verum
end;
theorem Th25: :: GOBRD14:25
for p being Point of (TOP-REAL 2)
for f being non constant standard clockwise_oriented special_circular_sequence st p in RightComp f holds
N-bound (L~ f) > p `2
proof
let p be Point of (TOP-REAL 2); ::_thesis: for f being non constant standard clockwise_oriented special_circular_sequence st p in RightComp f holds
N-bound (L~ f) > p `2
let f be non constant standard clockwise_oriented special_circular_sequence; ::_thesis: ( p in RightComp f implies N-bound (L~ f) > p `2 )
set g = Rotate (f,(N-min (L~ f)));
A1: L~ f = L~ (Rotate (f,(N-min (L~ f)))) by REVROT_1:33;
reconsider u = p as Point of (Euclid 2) by EUCLID:22;
assume p in RightComp f ; ::_thesis: N-bound (L~ f) > p `2
then p in RightComp (Rotate (f,(N-min (L~ f)))) by REVROT_1:37;
then u in Int (RightComp (Rotate (f,(N-min (L~ f))))) by TOPS_1:23;
then consider r being real number such that
A2: r > 0 and
A3: Ball (u,r) c= RightComp (Rotate (f,(N-min (L~ f)))) by GOBOARD6:5;
reconsider r = r as Real by XREAL_0:def_1;
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)) by EUCLID:52
.= sqrt (((p `2) - ((p `2) + (r / 2))) ^2) by EUCLID:52
.= 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 (Rotate (f,(N-min (L~ f)))) misses LeftComp (Rotate (f,(N-min (L~ f)))) by Th14;
then A5: not |[(p `1),((p `2) + (r / 2))]| in LeftComp (Rotate (f,(N-min (L~ f)))) by A3, A4, XBOOLE_0:3;
set x = |[(E-bound (L~ (SpStSeq (L~ (Rotate (f,(N-min (L~ f)))))))),((p `2) + (r / 2))]|;
A6: LSeg ((SE-corner (L~ (Rotate (f,(N-min (L~ f)))))),(NE-corner (L~ (Rotate (f,(N-min (L~ f))))))) c= L~ (SpStSeq (L~ (Rotate (f,(N-min (L~ f)))))) by TOPREAL6:35;
A7: proj2 . |[(E-bound (L~ (SpStSeq (L~ (Rotate (f,(N-min (L~ f)))))))),((p `2) + (r / 2))]| = |[(E-bound (L~ (SpStSeq (L~ (Rotate (f,(N-min (L~ f)))))))),((p `2) + (r / 2))]| `2 by PSCOMP_1:def_6
.= (p `2) + (r / 2) by EUCLID:52 ;
N-min (L~ f) in rng f by SPRECT_2:39;
then A8: (Rotate (f,(N-min (L~ f)))) /. 1 = N-min (L~ (Rotate (f,(N-min (L~ f))))) by A1, FINSEQ_6:92;
then |[(p `1),((p `2) + (r / 2))]| `2 <= N-bound (L~ (Rotate (f,(N-min (L~ f))))) by A5, JORDAN2C:113;
then (p `2) + (r / 2) <= N-bound (L~ (Rotate (f,(N-min (L~ f))))) by EUCLID:52;
then A9: |[(E-bound (L~ (SpStSeq (L~ (Rotate (f,(N-min (L~ f)))))))),((p `2) + (r / 2))]| `2 <= N-bound (L~ (Rotate (f,(N-min (L~ f))))) by EUCLID:52;
|[(E-bound (L~ (SpStSeq (L~ (Rotate (f,(N-min (L~ f)))))))),((p `2) + (r / 2))]| `1 = E-bound (L~ (SpStSeq (L~ (Rotate (f,(N-min (L~ f))))))) by EUCLID:52;
then A10: |[(E-bound (L~ (SpStSeq (L~ (Rotate (f,(N-min (L~ f)))))))),((p `2) + (r / 2))]| `1 = E-bound (L~ (Rotate (f,(N-min (L~ f))))) by SPRECT_1:61;
|[(p `1),((p `2) + (r / 2))]| `2 >= S-bound (L~ (Rotate (f,(N-min (L~ f))))) by A8, A5, JORDAN2C:112;
then (p `2) + (r / 2) >= S-bound (L~ (Rotate (f,(N-min (L~ f))))) by EUCLID:52;
then A11: |[(E-bound (L~ (SpStSeq (L~ (Rotate (f,(N-min (L~ f)))))))),((p `2) + (r / 2))]| `2 >= S-bound (L~ (Rotate (f,(N-min (L~ f))))) by EUCLID:52;
LSeg ((SE-corner (L~ (Rotate (f,(N-min (L~ f)))))),(NE-corner (L~ (Rotate (f,(N-min (L~ f))))))) = { q where q is Point of (TOP-REAL 2) : ( q `1 = E-bound (L~ (Rotate (f,(N-min (L~ f))))) & q `2 <= N-bound (L~ (Rotate (f,(N-min (L~ f))))) & q `2 >= S-bound (L~ (Rotate (f,(N-min (L~ f))))) ) } by SPRECT_1:23;
then |[(E-bound (L~ (SpStSeq (L~ (Rotate (f,(N-min (L~ f)))))))),((p `2) + (r / 2))]| in LSeg ((SE-corner (L~ (Rotate (f,(N-min (L~ f)))))),(NE-corner (L~ (Rotate (f,(N-min (L~ f))))))) by A9, A11, A10;
then ( proj2 .: (L~ (SpStSeq (L~ (Rotate (f,(N-min (L~ f))))))) is bounded_above & (p `2) + (r / 2) in proj2 .: (L~ (SpStSeq (L~ (Rotate (f,(N-min (L~ f))))))) ) by A6, A7, FUNCT_2:35;
then A12: upper_bound (proj2 .: (L~ (SpStSeq (L~ (Rotate (f,(N-min (L~ f)))))))) >= (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~ (Rotate (f,(N-min (L~ f))))))) = N-bound (L~ (Rotate (f,(N-min (L~ f))))) & N-bound (L~ (SpStSeq (L~ (Rotate (f,(N-min (L~ f))))))) = upper_bound (proj2 .: (L~ (SpStSeq (L~ (Rotate (f,(N-min (L~ f)))))))) ) by SPRECT_1:45, SPRECT_1:60;
hence N-bound (L~ f) > p `2 by A1, A12, A13, XXREAL_0:2; ::_thesis: verum
end;
theorem Th26: :: GOBRD14:26
for p being Point of (TOP-REAL 2)
for f being non constant standard clockwise_oriented special_circular_sequence st p in RightComp f holds
S-bound (L~ f) < p `2
proof
let p be Point of (TOP-REAL 2); ::_thesis: for f being non constant standard clockwise_oriented special_circular_sequence st p in RightComp f holds
S-bound (L~ f) < p `2
let f be non constant standard clockwise_oriented special_circular_sequence; ::_thesis: ( p in RightComp f implies S-bound (L~ f) < p `2 )
set g = Rotate (f,(N-min (L~ f)));
A1: L~ f = L~ (Rotate (f,(N-min (L~ f)))) by REVROT_1:33;
reconsider u = p as Point of (Euclid 2) by EUCLID:22;
assume p in RightComp f ; ::_thesis: S-bound (L~ f) < p `2
then p in RightComp (Rotate (f,(N-min (L~ f)))) by REVROT_1:37;
then u in Int (RightComp (Rotate (f,(N-min (L~ f))))) by TOPS_1:23;
then consider r being real number such that
A2: r > 0 and
A3: Ball (u,r) c= RightComp (Rotate (f,(N-min (L~ f)))) by GOBOARD6:5;
reconsider r = r as Real by XREAL_0:def_1;
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)) by EUCLID:52
.= sqrt (((p `2) - ((p `2) - (r / 2))) ^2) by EUCLID:52
.= 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 (Rotate (f,(N-min (L~ f)))) misses LeftComp (Rotate (f,(N-min (L~ f)))) by Th14;
then A5: not |[(p `1),((p `2) - (r / 2))]| in LeftComp (Rotate (f,(N-min (L~ f)))) by A3, A4, XBOOLE_0:3;
set x = |[(E-bound (L~ (SpStSeq (L~ (Rotate (f,(N-min (L~ f)))))))),((p `2) - (r / 2))]|;
A6: LSeg ((SE-corner (L~ (Rotate (f,(N-min (L~ f)))))),(NE-corner (L~ (Rotate (f,(N-min (L~ f))))))) c= L~ (SpStSeq (L~ (Rotate (f,(N-min (L~ f)))))) by TOPREAL6:35;
A7: proj2 . |[(E-bound (L~ (SpStSeq (L~ (Rotate (f,(N-min (L~ f)))))))),((p `2) - (r / 2))]| = |[(E-bound (L~ (SpStSeq (L~ (Rotate (f,(N-min (L~ f)))))))),((p `2) - (r / 2))]| `2 by PSCOMP_1:def_6
.= (p `2) - (r / 2) by EUCLID:52 ;
N-min (L~ f) in rng f by SPRECT_2:39;
then A8: (Rotate (f,(N-min (L~ f)))) /. 1 = N-min (L~ (Rotate (f,(N-min (L~ f))))) by A1, FINSEQ_6:92;
then |[(p `1),((p `2) - (r / 2))]| `2 <= N-bound (L~ (Rotate (f,(N-min (L~ f))))) by A5, JORDAN2C:113;
then (p `2) - (r / 2) <= N-bound (L~ (Rotate (f,(N-min (L~ f))))) by EUCLID:52;
then A9: |[(E-bound (L~ (SpStSeq (L~ (Rotate (f,(N-min (L~ f)))))))),((p `2) - (r / 2))]| `2 <= N-bound (L~ (Rotate (f,(N-min (L~ f))))) by EUCLID:52;
|[(E-bound (L~ (SpStSeq (L~ (Rotate (f,(N-min (L~ f)))))))),((p `2) - (r / 2))]| `1 = E-bound (L~ (SpStSeq (L~ (Rotate (f,(N-min (L~ f))))))) by EUCLID:52;
then A10: |[(E-bound (L~ (SpStSeq (L~ (Rotate (f,(N-min (L~ f)))))))),((p `2) - (r / 2))]| `1 = E-bound (L~ (Rotate (f,(N-min (L~ f))))) by SPRECT_1:61;
|[(p `1),((p `2) - (r / 2))]| `2 >= S-bound (L~ (Rotate (f,(N-min (L~ f))))) by A8, A5, JORDAN2C:112;
then (p `2) - (r / 2) >= S-bound (L~ (Rotate (f,(N-min (L~ f))))) by EUCLID:52;
then A11: |[(E-bound (L~ (SpStSeq (L~ (Rotate (f,(N-min (L~ f)))))))),((p `2) - (r / 2))]| `2 >= S-bound (L~ (Rotate (f,(N-min (L~ f))))) by EUCLID:52;
LSeg ((SE-corner (L~ (Rotate (f,(N-min (L~ f)))))),(NE-corner (L~ (Rotate (f,(N-min (L~ f))))))) = { q where q is Point of (TOP-REAL 2) : ( q `1 = E-bound (L~ (Rotate (f,(N-min (L~ f))))) & q `2 <= N-bound (L~ (Rotate (f,(N-min (L~ f))))) & q `2 >= S-bound (L~ (Rotate (f,(N-min (L~ f))))) ) } by SPRECT_1:23;
then |[(E-bound (L~ (SpStSeq (L~ (Rotate (f,(N-min (L~ f)))))))),((p `2) - (r / 2))]| in LSeg ((SE-corner (L~ (Rotate (f,(N-min (L~ f)))))),(NE-corner (L~ (Rotate (f,(N-min (L~ f))))))) by A9, A11, A10;
then ( proj2 .: (L~ (SpStSeq (L~ (Rotate (f,(N-min (L~ f))))))) is bounded_below & (p `2) - (r / 2) in proj2 .: (L~ (SpStSeq (L~ (Rotate (f,(N-min (L~ f))))))) ) by A6, A7, FUNCT_2:35;
then A12: lower_bound (proj2 .: (L~ (SpStSeq (L~ (Rotate (f,(N-min (L~ f)))))))) <= (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~ (Rotate (f,(N-min (L~ f))))))) = S-bound (L~ (Rotate (f,(N-min (L~ f))))) & S-bound (L~ (SpStSeq (L~ (Rotate (f,(N-min (L~ f))))))) = lower_bound (proj2 .: (L~ (SpStSeq (L~ (Rotate (f,(N-min (L~ f)))))))) ) by SPRECT_1:44, SPRECT_1:59;
hence S-bound (L~ f) < p `2 by A1, A12, A13, XXREAL_0:2; ::_thesis: verum
end;
theorem Th27: :: GOBRD14:27
for p, q being Point of (TOP-REAL 2)
for f being non constant standard clockwise_oriented special_circular_sequence st p in RightComp f & q in LeftComp f holds
LSeg (p,q) meets L~ f
proof
let p, q be Point of (TOP-REAL 2); ::_thesis: for f being non constant standard clockwise_oriented special_circular_sequence st p in RightComp f & q in LeftComp f holds
LSeg (p,q) meets L~ f
let f be non constant standard clockwise_oriented special_circular_sequence; ::_thesis: ( p in RightComp f & q in LeftComp f implies LSeg (p,q) meets L~ f )
assume that
A1: p in RightComp f and
A2: q in LeftComp f ; ::_thesis: LSeg (p,q) meets L~ f
assume LSeg (p,q) misses L~ f ; ::_thesis: contradiction
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; ::_thesis: verum
end;
theorem Th28: :: GOBRD14:28
for C being compact non horizontal non vertical Subset of (TOP-REAL 2) holds 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
let C be compact non horizontal non vertical Subset of (TOP-REAL 2); ::_thesis: 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))).]))
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 ((1,2) --> ([.(W-bound (L~ (SpStSeq C))),(E-bound (L~ (SpStSeq C))).],[.(S-bound (L~ (SpStSeq C))),(N-bound (L~ (SpStSeq C))).])) = {1,2} by FUNCT_4:62;
A2: Cl (RightComp (SpStSeq C)) = (RightComp (SpStSeq C)) \/ (L~ (SpStSeq C)) by Th21;
hereby :: according to TARSKI:def_3,XBOOLE_0:def_10 ::_thesis: product ((1,2) --> ([.(W-bound (L~ (SpStSeq C))),(E-bound (L~ (SpStSeq C))).],[.(S-bound (L~ (SpStSeq C))),(N-bound (L~ (SpStSeq C))).])) c= Cl (RightComp (SpStSeq C))
let a be set ; ::_thesis: ( a in Cl (RightComp (SpStSeq C)) implies a in product ((1,2) --> ([.(W-bound (L~ (SpStSeq C))),(E-bound (L~ (SpStSeq C))).],[.(S-bound (L~ (SpStSeq C))),(N-bound (L~ (SpStSeq C))).])) )
assume A3: a in Cl (RightComp (SpStSeq C)) ; ::_thesis: a in product ((1,2) --> ([.(W-bound (L~ (SpStSeq C))),(E-bound (L~ (SpStSeq C))).],[.(S-bound (L~ (SpStSeq C))),(N-bound (L~ (SpStSeq C))).]))
then reconsider b = a as Point of (TOP-REAL 2) ;
reconsider h = a as FinSequence by A3;
A4: for x being set st x in {1,2} holds
h . x in ((1,2) --> ([.(W-bound (L~ (SpStSeq C))),(E-bound (L~ (SpStSeq C))).],[.(S-bound (L~ (SpStSeq C))),(N-bound (L~ (SpStSeq C))).])) . x
proof
let x be set ; ::_thesis: ( x in {1,2} implies h . x in ((1,2) --> ([.(W-bound (L~ (SpStSeq C))),(E-bound (L~ (SpStSeq C))).],[.(S-bound (L~ (SpStSeq C))),(N-bound (L~ (SpStSeq C))).])) . x )
assume A5: x in {1,2} ; ::_thesis: h . x in ((1,2) --> ([.(W-bound (L~ (SpStSeq C))),(E-bound (L~ (SpStSeq C))).],[.(S-bound (L~ (SpStSeq C))),(N-bound (L~ (SpStSeq C))).])) . x
percases ( x = 1 or x = 2 ) by A5, TARSKI:def_2;
supposeA6: x = 1 ; ::_thesis: h . x in ((1,2) --> ([.(W-bound (L~ (SpStSeq C))),(E-bound (L~ (SpStSeq C))).],[.(S-bound (L~ (SpStSeq C))),(N-bound (L~ (SpStSeq C))).])) . x
then A7: ((1,2) --> ([.(W-bound (L~ (SpStSeq C))),(E-bound (L~ (SpStSeq C))).],[.(S-bound (L~ (SpStSeq C))),(N-bound (L~ (SpStSeq C))).])) . x = [.(W-bound (L~ (SpStSeq C))),(E-bound (L~ (SpStSeq C))).] by FUNCT_4:63;
now__::_thesis:_(_(_a_in_RightComp_(SpStSeq_C)_&_h_._x_in_((1,2)_-->_([.(W-bound_(L~_(SpStSeq_C))),(E-bound_(L~_(SpStSeq_C))).],[.(S-bound_(L~_(SpStSeq_C))),(N-bound_(L~_(SpStSeq_C))).]))_._x_)_or_(_a_in_L~_(SpStSeq_C)_&_h_._x_in_((1,2)_-->_([.(W-bound_(L~_(SpStSeq_C))),(E-bound_(L~_(SpStSeq_C))).],[.(S-bound_(L~_(SpStSeq_C))),(N-bound_(L~_(SpStSeq_C))).]))_._x_)_)
percases ( a in RightComp (SpStSeq C) or a in L~ (SpStSeq C) ) by A2, A3, XBOOLE_0:def_3;
case a in RightComp (SpStSeq C) ; ::_thesis: h . x in ((1,2) --> ([.(W-bound (L~ (SpStSeq C))),(E-bound (L~ (SpStSeq C))).],[.(S-bound (L~ (SpStSeq C))),(N-bound (L~ (SpStSeq C))).])) . x
then ( W-bound (L~ (SpStSeq C)) < b `1 & E-bound (L~ (SpStSeq C)) > b `1 ) by Th23, Th24;
hence h . x in ((1,2) --> ([.(W-bound (L~ (SpStSeq C))),(E-bound (L~ (SpStSeq C))).],[.(S-bound (L~ (SpStSeq C))),(N-bound (L~ (SpStSeq C))).])) . x by A6, A7, XXREAL_1:1; ::_thesis: verum
end;
case a in L~ (SpStSeq C) ; ::_thesis: h . x in ((1,2) --> ([.(W-bound (L~ (SpStSeq C))),(E-bound (L~ (SpStSeq C))).],[.(S-bound (L~ (SpStSeq C))),(N-bound (L~ (SpStSeq C))).])) . x
then ( W-bound (L~ (SpStSeq C)) <= b `1 & b `1 <= E-bound (L~ (SpStSeq C)) ) by PSCOMP_1:24;
hence h . x in ((1,2) --> ([.(W-bound (L~ (SpStSeq C))),(E-bound (L~ (SpStSeq C))).],[.(S-bound (L~ (SpStSeq C))),(N-bound (L~ (SpStSeq C))).])) . x by A6, A7, XXREAL_1:1; ::_thesis: verum
end;
end;
end;
hence h . x in ((1,2) --> ([.(W-bound (L~ (SpStSeq C))),(E-bound (L~ (SpStSeq C))).],[.(S-bound (L~ (SpStSeq C))),(N-bound (L~ (SpStSeq C))).])) . x ; ::_thesis: verum
end;
supposeA8: x = 2 ; ::_thesis: h . x in ((1,2) --> ([.(W-bound (L~ (SpStSeq C))),(E-bound (L~ (SpStSeq C))).],[.(S-bound (L~ (SpStSeq C))),(N-bound (L~ (SpStSeq C))).])) . x
then A9: ((1,2) --> ([.(W-bound (L~ (SpStSeq C))),(E-bound (L~ (SpStSeq C))).],[.(S-bound (L~ (SpStSeq C))),(N-bound (L~ (SpStSeq C))).])) . x = [.(S-bound (L~ (SpStSeq C))),(N-bound (L~ (SpStSeq C))).] by FUNCT_4:63;
now__::_thesis:_(_(_a_in_RightComp_(SpStSeq_C)_&_h_._x_in_((1,2)_-->_([.(W-bound_(L~_(SpStSeq_C))),(E-bound_(L~_(SpStSeq_C))).],[.(S-bound_(L~_(SpStSeq_C))),(N-bound_(L~_(SpStSeq_C))).]))_._x_)_or_(_a_in_L~_(SpStSeq_C)_&_h_._x_in_((1,2)_-->_([.(W-bound_(L~_(SpStSeq_C))),(E-bound_(L~_(SpStSeq_C))).],[.(S-bound_(L~_(SpStSeq_C))),(N-bound_(L~_(SpStSeq_C))).]))_._x_)_)
percases ( a in RightComp (SpStSeq C) or a in L~ (SpStSeq C) ) by A2, A3, XBOOLE_0:def_3;
case a in RightComp (SpStSeq C) ; ::_thesis: h . x in ((1,2) --> ([.(W-bound (L~ (SpStSeq C))),(E-bound (L~ (SpStSeq C))).],[.(S-bound (L~ (SpStSeq C))),(N-bound (L~ (SpStSeq C))).])) . x
then ( S-bound (L~ (SpStSeq C)) < b `2 & N-bound (L~ (SpStSeq C)) > b `2 ) by Th25, Th26;
hence h . x in ((1,2) --> ([.(W-bound (L~ (SpStSeq C))),(E-bound (L~ (SpStSeq C))).],[.(S-bound (L~ (SpStSeq C))),(N-bound (L~ (SpStSeq C))).])) . x by A8, A9, XXREAL_1:1; ::_thesis: verum
end;
case a in L~ (SpStSeq C) ; ::_thesis: h . x in ((1,2) --> ([.(W-bound (L~ (SpStSeq C))),(E-bound (L~ (SpStSeq C))).],[.(S-bound (L~ (SpStSeq C))),(N-bound (L~ (SpStSeq C))).])) . x
then ( S-bound (L~ (SpStSeq C)) <= b `2 & b `2 <= N-bound (L~ (SpStSeq C)) ) by PSCOMP_1:24;
hence h . x in ((1,2) --> ([.(W-bound (L~ (SpStSeq C))),(E-bound (L~ (SpStSeq C))).],[.(S-bound (L~ (SpStSeq C))),(N-bound (L~ (SpStSeq C))).])) . x by A8, A9, XXREAL_1:1; ::_thesis: verum
end;
end;
end;
hence h . x in ((1,2) --> ([.(W-bound (L~ (SpStSeq C))),(E-bound (L~ (SpStSeq C))).],[.(S-bound (L~ (SpStSeq C))),(N-bound (L~ (SpStSeq C))).])) . x ; ::_thesis: verum
end;
end;
end;
a is Tuple of 2, REAL by A3, Lm1, FINSEQ_2:131;
then ex r, s being Real st a = <*r,s*> by FINSEQ_2:100;
then dom h = {1,2} by FINSEQ_1:2, FINSEQ_1:89;
hence a in product ((1,2) --> ([.(W-bound (L~ (SpStSeq C))),(E-bound (L~ (SpStSeq C))).],[.(S-bound (L~ (SpStSeq C))),(N-bound (L~ (SpStSeq C))).])) by A1, A4, CARD_3:9; ::_thesis: verum
end;
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in product ((1,2) --> ([.(W-bound (L~ (SpStSeq C))),(E-bound (L~ (SpStSeq C))).],[.(S-bound (L~ (SpStSeq C))),(N-bound (L~ (SpStSeq C))).])) or a in Cl (RightComp (SpStSeq C)) )
assume a in product ((1,2) --> ([.(W-bound (L~ (SpStSeq C))),(E-bound (L~ (SpStSeq C))).],[.(S-bound (L~ (SpStSeq C))),(N-bound (L~ (SpStSeq C))).])) ; ::_thesis: a in Cl (RightComp (SpStSeq C))
then consider h being Function such that
A10: a = h and
A11: dom h = dom ((1,2) --> ([.(W-bound (L~ (SpStSeq C))),(E-bound (L~ (SpStSeq C))).],[.(S-bound (L~ (SpStSeq C))),(N-bound (L~ (SpStSeq C))).])) and
A12: for x being set st x in dom ((1,2) --> ([.(W-bound (L~ (SpStSeq C))),(E-bound (L~ (SpStSeq C))).],[.(S-bound (L~ (SpStSeq C))),(N-bound (L~ (SpStSeq C))).])) holds
h . x in ((1,2) --> ([.(W-bound (L~ (SpStSeq C))),(E-bound (L~ (SpStSeq C))).],[.(S-bound (L~ (SpStSeq C))),(N-bound (L~ (SpStSeq C))).])) . 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 ((1,2) --> ([.(W-bound (L~ (SpStSeq C))),(E-bound (L~ (SpStSeq C))).],[.(S-bound (L~ (SpStSeq C))),(N-bound (L~ (SpStSeq C))).])) by A1, TARSKI:def_2;
then h . 2 in ((1,2) --> ([.(W-bound (L~ (SpStSeq C))),(E-bound (L~ (SpStSeq C))).],[.(S-bound (L~ (SpStSeq C))),(N-bound (L~ (SpStSeq C))).])) . 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 ((1,2) --> ([.(W-bound (L~ (SpStSeq C))),(E-bound (L~ (SpStSeq C))).],[.(S-bound (L~ (SpStSeq C))),(N-bound (L~ (SpStSeq C))).])) by A1, TARSKI:def_2;
then h . 1 in ((1,2) --> ([.(W-bound (L~ (SpStSeq C))),(E-bound (L~ (SpStSeq C))).],[.(S-bound (L~ (SpStSeq C))),(N-bound (L~ (SpStSeq C))).])) . 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 where q is Point of (TOP-REAL 2) : ( not W-bound (L~ (SpStSeq C)) <= q `1 or not q `1 <= E-bound (L~ (SpStSeq C)) or not S-bound (L~ (SpStSeq C)) <= q `2 or not q `2 <= N-bound (L~ (SpStSeq C)) ) } by SPRECT_3:37;
A20: for k being set st k in dom h holds
h . k = <*r,s*> . k
proof
let k be set ; ::_thesis: ( k in dom h implies h . k = <*r,s*> . k )
assume k in dom h ; ::_thesis: h . k = <*r,s*> . k
then ( k = 1 or k = 2 ) by A11, TARSKI:def_2;
hence h . k = <*r,s*> . k by A17, A14, FINSEQ_1:44; ::_thesis: verum
end;
dom <*r,s*> = {1,2} by FINSEQ_1:2, FINSEQ_1:89;
then A21: a = |[r,s]| by A10, A11, A20, FUNCT_1:2, FUNCT_4:62;
assume not a in Cl (RightComp (SpStSeq C)) ; ::_thesis: contradiction
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 being Point of (TOP-REAL 2) st
( q = a & ( not W-bound (L~ (SpStSeq C)) <= q `1 or not q `1 <= E-bound (L~ (SpStSeq C)) or not S-bound (L~ (SpStSeq C)) <= q `2 or not q `2 <= N-bound (L~ (SpStSeq C)) ) ) by A19;
hence contradiction by A18, A15, A21, EUCLID:52; ::_thesis: verum
end;
theorem Th29: :: GOBRD14:29
for f being non constant standard clockwise_oriented special_circular_sequence holds proj1 .: (Cl (RightComp f)) = proj1 .: (L~ f)
proof
let f be non constant standard clockwise_oriented special_circular_sequence; ::_thesis: proj1 .: (Cl (RightComp f)) = proj1 .: (L~ f)
set g = Rotate (f,(N-min (L~ f)));
A1: L~ f = L~ (Rotate (f,(N-min (L~ f)))) by REVROT_1:33;
N-min (L~ f) in rng f by SPRECT_2:39;
then A2: (Rotate (f,(N-min (L~ f)))) /. 1 = N-min (L~ (Rotate (f,(N-min (L~ f))))) by A1, FINSEQ_6:92;
thus proj1 .: (Cl (RightComp f)) c= proj1 .: (L~ f) :: according to XBOOLE_0:def_10 ::_thesis: proj1 .: (L~ f) c= proj1 .: (Cl (RightComp f))
proof
A3: Cl (RightComp f) = (RightComp f) \/ (L~ f) by Th21;
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in proj1 .: (Cl (RightComp f)) or a in proj1 .: (L~ f) )
assume a in proj1 .: (Cl (RightComp f)) ; ::_thesis: a in proj1 .: (L~ 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:64;
percases ( x in RightComp f or x in L~ f ) by A5, A3, XBOOLE_0:def_3;
supposeA7: x in RightComp f ; ::_thesis: a in proj1 .: (L~ f)
reconsider x = x as Point of (TOP-REAL 2) by A4;
set b = |[(x `1),((N-bound (L~ f)) + 1)]|;
( |[(x `1),((N-bound (L~ f)) + 1)]| `2 = (N-bound (L~ f)) + 1 & (N-bound (L~ f)) + 1 > (N-bound (L~ f)) + 0 ) by EUCLID:52, XREAL_1:6;
then |[(x `1),((N-bound (L~ f)) + 1)]| in LeftComp (Rotate (f,(N-min (L~ f)))) by A1, A2, JORDAN2C:113;
then |[(x `1),((N-bound (L~ f)) + 1)]| in LeftComp f by REVROT_1:36;
then LSeg (x,|[(x `1),((N-bound (L~ f)) + 1)]|) meets L~ f by A7, Th27;
then consider c being set such that
A8: c in LSeg (x,|[(x `1),((N-bound (L~ f)) + 1)]|) and
A9: c in L~ f by XBOOLE_0:3;
reconsider c = c as Point of (TOP-REAL 2) by A8;
A10: |[(x `1),((N-bound (L~ f)) + 1)]| `1 = x `1 by EUCLID:52;
proj1 . c = c `1 by PSCOMP_1:def_5
.= x `1 by A8, A10, GOBOARD7:5
.= a by A6, PSCOMP_1:def_5 ;
hence a in proj1 .: (L~ f) by A9, FUNCT_2:35; ::_thesis: verum
end;
suppose x in L~ f ; ::_thesis: a in proj1 .: (L~ f)
hence a in proj1 .: (L~ f) by A6, FUNCT_2:35; ::_thesis: verum
end;
end;
end;
L~ f = (Cl (RightComp f)) \ (RightComp f) by Th19;
hence proj1 .: (L~ f) c= proj1 .: (Cl (RightComp f)) by RELAT_1:123, XBOOLE_1:36; ::_thesis: verum
end;
theorem Th30: :: GOBRD14:30
for f being non constant standard clockwise_oriented special_circular_sequence holds proj2 .: (Cl (RightComp f)) = proj2 .: (L~ f)
proof
let f be non constant standard clockwise_oriented special_circular_sequence; ::_thesis: proj2 .: (Cl (RightComp f)) = proj2 .: (L~ f)
set g = Rotate (f,(N-min (L~ f)));
A1: L~ f = L~ (Rotate (f,(N-min (L~ f)))) by REVROT_1:33;
N-min (L~ f) in rng f by SPRECT_2:39;
then A2: (Rotate (f,(N-min (L~ f)))) /. 1 = N-min (L~ (Rotate (f,(N-min (L~ f))))) by A1, FINSEQ_6:92;
thus proj2 .: (Cl (RightComp f)) c= proj2 .: (L~ f) :: according to XBOOLE_0:def_10 ::_thesis: proj2 .: (L~ f) c= proj2 .: (Cl (RightComp f))
proof
A3: Cl (RightComp f) = (RightComp f) \/ (L~ f) by Th21;
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in proj2 .: (Cl (RightComp f)) or a in proj2 .: (L~ f) )
assume a in proj2 .: (Cl (RightComp f)) ; ::_thesis: a in proj2 .: (L~ 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:64;
percases ( x in RightComp f or x in L~ f ) by A5, A3, XBOOLE_0:def_3;
supposeA7: x in RightComp f ; ::_thesis: a in proj2 .: (L~ f)
reconsider x = x as Point of (TOP-REAL 2) by A4;
set b = |[((E-bound (L~ f)) + 1),(x `2)]|;
( |[((E-bound (L~ f)) + 1),(x `2)]| `1 = (E-bound (L~ f)) + 1 & (E-bound (L~ f)) + 1 > (E-bound (L~ f)) + 0 ) by EUCLID:52, XREAL_1:6;
then |[((E-bound (L~ f)) + 1),(x `2)]| in LeftComp (Rotate (f,(N-min (L~ f)))) by A1, A2, JORDAN2C:111;
then |[((E-bound (L~ f)) + 1),(x `2)]| in LeftComp f by REVROT_1:36;
then LSeg (x,|[((E-bound (L~ f)) + 1),(x `2)]|) meets L~ f by A7, Th27;
then consider c being set such that
A8: c in LSeg (x,|[((E-bound (L~ f)) + 1),(x `2)]|) and
A9: c in L~ f by XBOOLE_0:3;
reconsider c = c as Point of (TOP-REAL 2) by A8;
A10: |[((E-bound (L~ f)) + 1),(x `2)]| `2 = x `2 by EUCLID:52;
proj2 . c = c `2 by PSCOMP_1:def_6
.= x `2 by A8, A10, GOBOARD7:6
.= a by A6, PSCOMP_1:def_6 ;
hence a in proj2 .: (L~ f) by A9, FUNCT_2:35; ::_thesis: verum
end;
suppose x in L~ f ; ::_thesis: a in proj2 .: (L~ f)
hence a in proj2 .: (L~ f) by A6, FUNCT_2:35; ::_thesis: verum
end;
end;
end;
L~ f = (Cl (RightComp f)) \ (RightComp f) by Th19;
hence proj2 .: (L~ f) c= proj2 .: (Cl (RightComp f)) by RELAT_1:123, XBOOLE_1:36; ::_thesis: verum
end;
theorem Th31: :: GOBRD14:31
for g being non constant standard clockwise_oriented special_circular_sequence holds RightComp g c= RightComp (SpStSeq (L~ g))
proof
let g be non constant standard clockwise_oriented special_circular_sequence; ::_thesis: RightComp g c= RightComp (SpStSeq (L~ g))
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in RightComp g or a in RightComp (SpStSeq (L~ g)) )
assume A1: a in RightComp g ; ::_thesis: a in RightComp (SpStSeq (L~ 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 where q is Point of (TOP-REAL 2) : ( 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 a in RightComp (SpStSeq (L~ g)) by A2, A4, A3, A5; ::_thesis: verum
end;
theorem Th32: :: GOBRD14:32
for g being non constant standard clockwise_oriented special_circular_sequence holds Cl (RightComp g) is compact
proof
let g be non constant standard clockwise_oriented special_circular_sequence; ::_thesis: Cl (RightComp g) is compact
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 Cl (RightComp g) is compact by A1, COMPTS_1:9, PRE_TOPC:19; ::_thesis: verum
end;
theorem Th33: :: GOBRD14:33
for g being non constant standard clockwise_oriented special_circular_sequence holds not LeftComp g is bounded
proof
let g be non constant standard clockwise_oriented special_circular_sequence; ::_thesis: not LeftComp g is bounded
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 not LeftComp g is bounded by A1, TOPREAL6:66; ::_thesis: verum
end;
theorem Th34: :: GOBRD14:34
for g being non constant standard clockwise_oriented special_circular_sequence holds LeftComp g is_outside_component_of L~ g
proof
let g be non constant standard clockwise_oriented special_circular_sequence; ::_thesis: LeftComp g is_outside_component_of L~ g
thus LeftComp g is_a_component_of (L~ g) ` by GOBOARD9:def_1; :: according to JORDAN2C:def_3 ::_thesis: not LeftComp g is bounded
thus not LeftComp g is bounded by Th33; ::_thesis: verum
end;
theorem :: GOBRD14:35
for g being non constant standard clockwise_oriented special_circular_sequence holds RightComp g is_inside_component_of L~ g
proof
let g be non constant standard clockwise_oriented special_circular_sequence; ::_thesis: RightComp g is_inside_component_of L~ g
thus RightComp g is_a_component_of (L~ g) ` by GOBOARD9:def_2; :: according to JORDAN2C:def_2 ::_thesis: RightComp g is bounded
Cl (RightComp g) is compact by Th32;
hence RightComp g is bounded by PRE_TOPC:18, RLTOPSP1:42; ::_thesis: verum
end;
theorem Th36: :: GOBRD14:36
for g being non constant standard clockwise_oriented special_circular_sequence holds UBD (L~ g) = LeftComp g
proof
let g be non constant standard clockwise_oriented special_circular_sequence; ::_thesis: UBD (L~ g) = LeftComp g
( UBD (L~ g) is_outside_component_of L~ g & LeftComp g is_outside_component_of L~ g ) by Th34, JORDAN2C:68;
hence UBD (L~ g) = LeftComp g by JORDAN2C:119; ::_thesis: verum
end;
theorem Th37: :: GOBRD14:37
for g being non constant standard clockwise_oriented special_circular_sequence holds BDD (L~ g) = RightComp g
proof
let g be non constant standard clockwise_oriented special_circular_sequence; ::_thesis: BDD (L~ g) = RightComp g
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 BDD (L~ g) = RightComp g by A2, A1, XBOOLE_1:71; ::_thesis: verum
end;
theorem :: GOBRD14:38
for g being non constant standard clockwise_oriented special_circular_sequence
for P being Subset of (TOP-REAL 2) st P is_outside_component_of L~ g holds
P = LeftComp g
proof
let g be non constant standard clockwise_oriented special_circular_sequence; ::_thesis: for P being Subset of (TOP-REAL 2) st P is_outside_component_of L~ g holds
P = LeftComp g
let P be Subset of (TOP-REAL 2); ::_thesis: ( P is_outside_component_of L~ g implies P = LeftComp g )
assume A1: P is_outside_component_of L~ g ; ::_thesis: P = LeftComp g
UBD (L~ g) is_outside_component_of L~ g by JORDAN2C:68;
then P = UBD (L~ g) by A1, JORDAN2C:119;
hence P = LeftComp g by Th36; ::_thesis: verum
end;
theorem Th39: :: GOBRD14:39
for g being non constant standard clockwise_oriented special_circular_sequence
for P being Subset of (TOP-REAL 2) st P is_inside_component_of L~ g holds
P meets RightComp g
proof
let g be non constant standard clockwise_oriented special_circular_sequence; ::_thesis: for P being Subset of (TOP-REAL 2) st P is_inside_component_of L~ g holds
P meets RightComp g
let P be Subset of (TOP-REAL 2); ::_thesis: ( P is_inside_component_of L~ g implies P meets RightComp g )
assume P is_inside_component_of L~ g ; ::_thesis: P meets RightComp g
then A1: ( P c= BDD (L~ g) & P is_a_component_of (L~ g) ` ) by JORDAN2C:22, JORDAN2C:def_2;
BDD (L~ g) = RightComp g by Th37;
hence P meets RightComp g by A1, SPRECT_1:4, XBOOLE_1:67; ::_thesis: verum
end;
theorem :: GOBRD14:40
for g being non constant standard clockwise_oriented special_circular_sequence
for P being Subset of (TOP-REAL 2) st P is_inside_component_of L~ g holds
P = BDD (L~ g)
proof
let g be non constant standard clockwise_oriented special_circular_sequence; ::_thesis: for P being Subset of (TOP-REAL 2) st P is_inside_component_of L~ g holds
P = BDD (L~ g)
let P be Subset of (TOP-REAL 2); ::_thesis: ( P is_inside_component_of L~ g implies P = BDD (L~ g) )
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) ` by JORDAN2C:def_2;
assume A3: P is_inside_component_of L~ g ; ::_thesis: P = BDD (L~ g)
then P is_a_component_of (L~ g) ` by JORDAN2C:def_2;
hence P = BDD (L~ g) by A3, A1, A2, Th39, GOBOARD9:1; ::_thesis: verum
end;
theorem :: GOBRD14:41
for g being non constant standard clockwise_oriented special_circular_sequence holds W-bound (L~ g) = W-bound (RightComp g)
proof
let g be non constant standard clockwise_oriented special_circular_sequence; ::_thesis: W-bound (L~ g) = W-bound (RightComp g)
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 = (Cl (RightComp g)) \ (RightComp g) by Th19;
Cl (RightComp g) is compact by Th32;
then A3: RightComp g is bounded by PRE_TOPC:18, RLTOPSP1:42;
reconsider A = (Cl (RightComp g)) \ (RightComp g) 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 W-bound (L~ g) = W-bound (RightComp g) by A2, A3, A1, TOPREAL6:85; ::_thesis: verum
end;
theorem :: GOBRD14:42
for g being non constant standard clockwise_oriented special_circular_sequence holds E-bound (L~ g) = E-bound (RightComp g)
proof
let g be non constant standard clockwise_oriented special_circular_sequence; ::_thesis: E-bound (L~ g) = E-bound (RightComp g)
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 = (Cl (RightComp g)) \ (RightComp g) by Th19;
Cl (RightComp g) is compact by Th32;
then A3: RightComp g is bounded by PRE_TOPC:18, RLTOPSP1:42;
reconsider A = (Cl (RightComp g)) \ (RightComp g) 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 E-bound (L~ g) = E-bound (RightComp g) by A2, A3, A1, TOPREAL6:86; ::_thesis: verum
end;
theorem :: GOBRD14:43
for g being non constant standard clockwise_oriented special_circular_sequence holds N-bound (L~ g) = N-bound (RightComp g)
proof
let g be non constant standard clockwise_oriented special_circular_sequence; ::_thesis: N-bound (L~ g) = N-bound (RightComp g)
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 = (Cl (RightComp g)) \ (RightComp g) by Th19;
Cl (RightComp g) is compact by Th32;
then A3: RightComp g is bounded by PRE_TOPC:18, RLTOPSP1:42;
reconsider A = (Cl (RightComp g)) \ (RightComp g) 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 N-bound (L~ g) = N-bound (RightComp g) by A2, A3, A1, TOPREAL6:87; ::_thesis: verum
end;
theorem :: GOBRD14:44
for g being non constant standard clockwise_oriented special_circular_sequence holds S-bound (L~ g) = S-bound (RightComp g)
proof
let g be non constant standard clockwise_oriented special_circular_sequence; ::_thesis: S-bound (L~ g) = S-bound (RightComp g)
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 = (Cl (RightComp g)) \ (RightComp g) by Th19;
Cl (RightComp g) is compact by Th32;
then A3: RightComp g is bounded by PRE_TOPC:18, RLTOPSP1:42;
reconsider A = (Cl (RightComp g)) \ (RightComp g) 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 S-bound (L~ g) = S-bound (RightComp g) by A2, A3, A1, TOPREAL6:88; ::_thesis: verum
end;