:: JORDAN14 semantic presentation
begin
theorem Th1: :: JORDAN14:1
for f being non constant standard special_circular_sequence holds
( BDD (L~ f) = RightComp f or BDD (L~ f) = LeftComp f )
proof
let f be non constant standard special_circular_sequence; ::_thesis: ( BDD (L~ f) = RightComp f or BDD (L~ f) = LeftComp f )
BDD (L~ f) is_inside_component_of L~ f by JORDAN2C:108;
then BDD (L~ f) is_a_component_of (L~ f) ` by JORDAN2C:def_2;
hence ( BDD (L~ f) = RightComp f or BDD (L~ f) = LeftComp f ) by JORDAN1H:24; ::_thesis: verum
end;
theorem :: JORDAN14:2
for f being non constant standard special_circular_sequence holds
( UBD (L~ f) = RightComp f or UBD (L~ f) = LeftComp f )
proof
let f be non constant standard special_circular_sequence; ::_thesis: ( UBD (L~ f) = RightComp f or UBD (L~ f) = LeftComp f )
UBD (L~ f) is_outside_component_of L~ f by JORDAN2C:68;
then UBD (L~ f) is_a_component_of (L~ f) ` by JORDAN2C:def_3;
hence ( UBD (L~ f) = RightComp f or UBD (L~ f) = LeftComp f ) by JORDAN1H:24; ::_thesis: verum
end;
theorem :: JORDAN14:3
for G being Go-board
for f being FinSequence of (TOP-REAL 2)
for k being Element of NAT st 1 <= k & k + 1 <= len f & f is_sequence_on G holds
left_cell (f,k,G) is closed
proof
let G be Go-board; ::_thesis: for f being FinSequence of (TOP-REAL 2)
for k being Element of NAT st 1 <= k & k + 1 <= len f & f is_sequence_on G holds
left_cell (f,k,G) is closed
let f be FinSequence of (TOP-REAL 2); ::_thesis: for k being Element of NAT st 1 <= k & k + 1 <= len f & f is_sequence_on G holds
left_cell (f,k,G) is closed
let k be Element of NAT ; ::_thesis: ( 1 <= k & k + 1 <= len f & f is_sequence_on G implies left_cell (f,k,G) is closed )
assume that
A1: 1 <= k and
A2: k + 1 <= len f and
A3: f is_sequence_on G ; ::_thesis: left_cell (f,k,G) is closed
consider i1, j1, i2, j2 being Element of NAT such that
A4: [i1,j1] in Indices G and
A5: f /. k = G * (i1,j1) and
A6: [i2,j2] in Indices G and
A7: f /. (k + 1) = G * (i2,j2) and
A8: ( ( i1 = i2 & j1 + 1 = j2 ) or ( i1 + 1 = i2 & j1 = j2 ) or ( i1 = i2 + 1 & j1 = j2 ) or ( i1 = i2 & j1 = j2 + 1 ) ) by A1, A2, A3, JORDAN8:3;
( ( i1 = i2 & j1 + 1 = j2 & left_cell (f,k,G) = cell (G,(i1 -' 1),j1) ) or ( i1 + 1 = i2 & j1 = j2 & left_cell (f,k,G) = cell (G,i1,j1) ) or ( i1 = i2 + 1 & j1 = j2 & left_cell (f,k,G) = cell (G,i2,(j2 -' 1)) ) or ( i1 = i2 & j1 = j2 + 1 & left_cell (f,k,G) = cell (G,i1,j2) ) ) by A1, A2, A3, A4, A5, A6, A7, A8, GOBRD13:def_3;
hence left_cell (f,k,G) is closed by GOBRD11:33; ::_thesis: verum
end;
theorem Th4: :: JORDAN14:4
for G being Go-board
for p being Point of (TOP-REAL 2)
for i, j being Element of NAT st 1 <= i & i + 1 <= len G & 1 <= j & j + 1 <= width G holds
( p in Int (cell (G,i,j)) iff ( (G * (i,j)) `1 < p `1 & p `1 < (G * ((i + 1),j)) `1 & (G * (i,j)) `2 < p `2 & p `2 < (G * (i,(j + 1))) `2 ) )
proof
let G be Go-board; ::_thesis: for p being Point of (TOP-REAL 2)
for i, j being Element of NAT st 1 <= i & i + 1 <= len G & 1 <= j & j + 1 <= width G holds
( p in Int (cell (G,i,j)) iff ( (G * (i,j)) `1 < p `1 & p `1 < (G * ((i + 1),j)) `1 & (G * (i,j)) `2 < p `2 & p `2 < (G * (i,(j + 1))) `2 ) )
let p be Point of (TOP-REAL 2); ::_thesis: for i, j being Element of NAT st 1 <= i & i + 1 <= len G & 1 <= j & j + 1 <= width G holds
( p in Int (cell (G,i,j)) iff ( (G * (i,j)) `1 < p `1 & p `1 < (G * ((i + 1),j)) `1 & (G * (i,j)) `2 < p `2 & p `2 < (G * (i,(j + 1))) `2 ) )
let i, j be Element of NAT ; ::_thesis: ( 1 <= i & i + 1 <= len G & 1 <= j & j + 1 <= width G implies ( p in Int (cell (G,i,j)) iff ( (G * (i,j)) `1 < p `1 & p `1 < (G * ((i + 1),j)) `1 & (G * (i,j)) `2 < p `2 & p `2 < (G * (i,(j + 1))) `2 ) ) )
assume that
A1: 1 <= i and
A2: i + 1 <= len G and
A3: 1 <= j and
A4: j + 1 <= width G ; ::_thesis: ( p in Int (cell (G,i,j)) iff ( (G * (i,j)) `1 < p `1 & p `1 < (G * ((i + 1),j)) `1 & (G * (i,j)) `2 < p `2 & p `2 < (G * (i,(j + 1))) `2 ) )
set Z = { |[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 ) } ;
A5: j < width G by A4, NAT_1:13;
i + 1 >= 1 by NAT_1:11;
then A6: (G * ((i + 1),1)) `1 = (G * ((i + 1),j)) `1 by A2, A3, A5, GOBOARD5:2;
A7: i < len G by A2, NAT_1:13;
then A8: (G * (1,j)) `2 = (G * (i,j)) `2 by A1, A3, A5, GOBOARD5:1;
j + 1 >= 1 by NAT_1:11;
then A9: (G * (1,(j + 1))) `2 = (G * (i,(j + 1))) `2 by A1, A4, A7, GOBOARD5:1;
A10: (G * (i,1)) `1 = (G * (i,j)) `1 by A1, A3, A7, A5, GOBOARD5:2;
thus ( p in Int (cell (G,i,j)) implies ( (G * (i,j)) `1 < p `1 & p `1 < (G * ((i + 1),j)) `1 & (G * (i,j)) `2 < p `2 & p `2 < (G * (i,(j + 1))) `2 ) ) ::_thesis: ( (G * (i,j)) `1 < p `1 & p `1 < (G * ((i + 1),j)) `1 & (G * (i,j)) `2 < p `2 & p `2 < (G * (i,(j + 1))) `2 implies p in Int (cell (G,i,j)) )
proof
assume p in Int (cell (G,i,j)) ; ::_thesis: ( (G * (i,j)) `1 < p `1 & p `1 < (G * ((i + 1),j)) `1 & (G * (i,j)) `2 < p `2 & p `2 < (G * (i,(j + 1))) `2 )
then p in { |[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 A1, A3, A7, A5, GOBOARD6:26;
then ex r, s being Real st
( p = |[r,s]| & (G * (i,1)) `1 < r & r < (G * ((i + 1),1)) `1 & (G * (1,j)) `2 < s & s < (G * (1,(j + 1))) `2 ) ;
hence ( (G * (i,j)) `1 < p `1 & p `1 < (G * ((i + 1),j)) `1 & (G * (i,j)) `2 < p `2 & p `2 < (G * (i,(j + 1))) `2 ) by A10, A6, A8, A9, EUCLID:52; ::_thesis: verum
end;
assume that
A11: (G * (i,j)) `1 < p `1 and
A12: p `1 < (G * ((i + 1),j)) `1 and
A13: (G * (i,j)) `2 < p `2 and
A14: p `2 < (G * (i,(j + 1))) `2 ; ::_thesis: p in Int (cell (G,i,j))
p = |[(p `1),(p `2)]| by EUCLID:53;
then p in { |[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 A10, A6, A8, A9, A11, A12, A13, A14;
hence p in Int (cell (G,i,j)) by A1, A3, A7, A5, GOBOARD6:26; ::_thesis: verum
end;
theorem Th5: :: JORDAN14:5
for f being non constant standard special_circular_sequence holds BDD (L~ f) is connected
proof
let f be non constant standard special_circular_sequence; ::_thesis: BDD (L~ f) is connected
( BDD (L~ f) = RightComp f or BDD (L~ f) = LeftComp f ) by Th1;
hence BDD (L~ f) is connected ; ::_thesis: verum
end;
registration
let f be non constant standard special_circular_sequence;
cluster BDD (L~ f) -> connected ;
coherence
BDD (L~ f) is connected by Th5;
end;
definition
let C be Simple_closed_curve;
let n be Element of NAT ;
func SpanStart (C,n) -> Point of (TOP-REAL 2) equals :: JORDAN14:def 1
(Gauge (C,n)) * ((X-SpanStart (C,n)),(Y-SpanStart (C,n)));
coherence
(Gauge (C,n)) * ((X-SpanStart (C,n)),(Y-SpanStart (C,n))) is Point of (TOP-REAL 2) ;
end;
:: deftheorem defines SpanStart JORDAN14:def_1_:_
for C being Simple_closed_curve
for n being Element of NAT holds SpanStart (C,n) = (Gauge (C,n)) * ((X-SpanStart (C,n)),(Y-SpanStart (C,n)));
theorem Th6: :: JORDAN14:6
for C being Simple_closed_curve
for n being Element of NAT st n is_sufficiently_large_for C holds
SpanStart (C,n) in BDD C
proof
let C be Simple_closed_curve; ::_thesis: for n being Element of NAT st n is_sufficiently_large_for C holds
SpanStart (C,n) in BDD C
let n be Element of NAT ; ::_thesis: ( n is_sufficiently_large_for C implies SpanStart (C,n) in BDD C )
A1: 1 <= (X-SpanStart (C,n)) -' 1 by JORDAN1H:50;
A2: (X-SpanStart (C,n)) -' 1 < len (Gauge (C,n)) by JORDAN1H:50;
assume A3: n is_sufficiently_large_for C ; ::_thesis: SpanStart (C,n) in BDD C
then A4: cell ((Gauge (C,n)),((X-SpanStart (C,n)) -' 1),(Y-SpanStart (C,n))) c= BDD C by JORDAN11:6;
A5: Y-SpanStart (C,n) <= width (Gauge (C,n)) by A3, JORDAN11:7;
1 < Y-SpanStart (C,n) by A3, JORDAN11:7;
then LSeg (((Gauge (C,n)) * (((X-SpanStart (C,n)) -' 1),(Y-SpanStart (C,n)))),((Gauge (C,n)) * ((((X-SpanStart (C,n)) -' 1) + 1),(Y-SpanStart (C,n))))) c= cell ((Gauge (C,n)),((X-SpanStart (C,n)) -' 1),(Y-SpanStart (C,n))) by A1, A2, A5, GOBOARD5:22;
then A6: LSeg (((Gauge (C,n)) * (((X-SpanStart (C,n)) -' 1),(Y-SpanStart (C,n)))),((Gauge (C,n)) * ((((X-SpanStart (C,n)) -' 1) + 1),(Y-SpanStart (C,n))))) c= BDD C by A4, XBOOLE_1:1;
A7: 2 < X-SpanStart (C,n) by JORDAN1H:49;
(Gauge (C,n)) * ((((X-SpanStart (C,n)) -' 1) + 1),(Y-SpanStart (C,n))) in LSeg (((Gauge (C,n)) * (((X-SpanStart (C,n)) -' 1),(Y-SpanStart (C,n)))),((Gauge (C,n)) * ((((X-SpanStart (C,n)) -' 1) + 1),(Y-SpanStart (C,n))))) by RLTOPSP1:68;
then (Gauge (C,n)) * ((((X-SpanStart (C,n)) -' 1) + 1),(Y-SpanStart (C,n))) in BDD C by A6;
hence SpanStart (C,n) in BDD C by A7, XREAL_1:235, XXREAL_0:2; ::_thesis: verum
end;
theorem Th7: :: JORDAN14:7
for C being Simple_closed_curve
for n, k being Element of NAT st n is_sufficiently_large_for C & 1 <= k & k + 1 <= len (Span (C,n)) holds
( right_cell ((Span (C,n)),k,(Gauge (C,n))) misses C & left_cell ((Span (C,n)),k,(Gauge (C,n))) meets C )
proof
let C be Simple_closed_curve; ::_thesis: for n, k being Element of NAT st n is_sufficiently_large_for C & 1 <= k & k + 1 <= len (Span (C,n)) holds
( right_cell ((Span (C,n)),k,(Gauge (C,n))) misses C & left_cell ((Span (C,n)),k,(Gauge (C,n))) meets C )
let n, k be Element of NAT ; ::_thesis: ( n is_sufficiently_large_for C & 1 <= k & k + 1 <= len (Span (C,n)) implies ( right_cell ((Span (C,n)),k,(Gauge (C,n))) misses C & left_cell ((Span (C,n)),k,(Gauge (C,n))) meets C ) )
set G = Gauge (C,n);
set f = Span (C,n);
defpred S1[ Element of NAT ] means for m being Element of NAT st 1 <= m & m + 1 <= len ((Span (C,n)) | $1) holds
( right_cell (((Span (C,n)) | $1),m,(Gauge (C,n))) misses C & left_cell (((Span (C,n)) | $1),m,(Gauge (C,n))) meets C );
A1: (Span (C,n)) | (len (Span (C,n))) = Span (C,n) by FINSEQ_1:58;
assume A2: n is_sufficiently_large_for C ; ::_thesis: ( not 1 <= k or not k + 1 <= len (Span (C,n)) or ( right_cell ((Span (C,n)),k,(Gauge (C,n))) misses C & left_cell ((Span (C,n)),k,(Gauge (C,n))) meets C ) )
then A3: Span (C,n) is_sequence_on Gauge (C,n) by JORDAN13:def_1;
A4: (Span (C,n)) /. 2 = (Gauge (C,n)) * (((X-SpanStart (C,n)) -' 1),(Y-SpanStart (C,n))) by A2, JORDAN13:def_1;
A5: (Span (C,n)) /. 1 = (Gauge (C,n)) * ((X-SpanStart (C,n)),(Y-SpanStart (C,n))) by A2, JORDAN13:def_1;
A6: for k being Element of NAT st S1[k] holds
S1[k + 1]
proof
let k be Element of NAT ; ::_thesis: ( S1[k] implies S1[k + 1] )
assume A7: for m being Element of NAT st 1 <= m & m + 1 <= len ((Span (C,n)) | k) holds
( right_cell (((Span (C,n)) | k),m,(Gauge (C,n))) misses C & left_cell (((Span (C,n)) | k),m,(Gauge (C,n))) meets C ) ; ::_thesis: S1[k + 1]
A8: (Span (C,n)) | (k + 1) is_sequence_on Gauge (C,n) by A3, GOBOARD1:22;
A9: (Span (C,n)) | k is_sequence_on Gauge (C,n) by A3, GOBOARD1:22;
percases ( k >= len (Span (C,n)) or k < len (Span (C,n)) ) ;
supposeA10: k >= len (Span (C,n)) ; ::_thesis: S1[k + 1]
then A11: (Span (C,n)) | (k + 1) = Span (C,n) by FINSEQ_1:58, NAT_1:12;
(Span (C,n)) | k = Span (C,n) by A10, FINSEQ_1:58;
hence S1[k + 1] by A7, A11; ::_thesis: verum
end;
supposeA12: k < len (Span (C,n)) ; ::_thesis: S1[k + 1]
let m be Element of NAT ; ::_thesis: ( 1 <= m & m + 1 <= len ((Span (C,n)) | (k + 1)) implies ( right_cell (((Span (C,n)) | (k + 1)),m,(Gauge (C,n))) misses C & left_cell (((Span (C,n)) | (k + 1)),m,(Gauge (C,n))) meets C ) )
assume that
A13: 1 <= m and
A14: m + 1 <= len ((Span (C,n)) | (k + 1)) ; ::_thesis: ( right_cell (((Span (C,n)) | (k + 1)),m,(Gauge (C,n))) misses C & left_cell (((Span (C,n)) | (k + 1)),m,(Gauge (C,n))) meets C )
A15: k + 1 <= len (Span (C,n)) by A12, NAT_1:13;
then A16: len ((Span (C,n)) | (k + 1)) = k + 1 by FINSEQ_1:59;
A17: len ((Span (C,n)) | k) = k by A12, FINSEQ_1:59;
now__::_thesis:_(_right_cell_(((Span_(C,n))_|_(k_+_1)),m,(Gauge_(C,n)))_misses_C_&_left_cell_(((Span_(C,n))_|_(k_+_1)),m,(Gauge_(C,n)))_meets_C_)
percases ( k = 0 or k = 1 or k > 1 ) by NAT_1:25;
supposeA18: k = 0 ; ::_thesis: ( right_cell (((Span (C,n)) | (k + 1)),m,(Gauge (C,n))) misses C & left_cell (((Span (C,n)) | (k + 1)),m,(Gauge (C,n))) meets C )
1 <= m + 1 by NAT_1:12;
then m + 1 = 0 + 1 by A16, A14, A18, XXREAL_0:1;
hence ( right_cell (((Span (C,n)) | (k + 1)),m,(Gauge (C,n))) misses C & left_cell (((Span (C,n)) | (k + 1)),m,(Gauge (C,n))) meets C ) by A13; ::_thesis: verum
end;
supposeA19: k = 1 ; ::_thesis: ( right_cell (((Span (C,n)) | (k + 1)),m,(Gauge (C,n))) misses C & left_cell (((Span (C,n)) | (k + 1)),m,(Gauge (C,n))) meets C )
set j = Y-SpanStart (C,n);
set i = X-SpanStart (C,n);
A20: (Span (C,n)) | (k + 1) = <*((Gauge (C,n)) * ((X-SpanStart (C,n)),(Y-SpanStart (C,n)))),((Gauge (C,n)) * (((X-SpanStart (C,n)) -' 1),(Y-SpanStart (C,n))))*> by A5, A4, A15, A19, FINSEQ_5:81;
then A21: ((Span (C,n)) | (k + 1)) /. 1 = (Gauge (C,n)) * ((X-SpanStart (C,n)),(Y-SpanStart (C,n))) by FINSEQ_4:17;
1 + 1 <= m + 1 by A13, XREAL_1:6;
then A22: m + 1 = 1 + 1 by A16, A14, A19, XXREAL_0:1;
A23: [((X-SpanStart (C,n)) -' 1),(Y-SpanStart (C,n))] in Indices (Gauge (C,n)) by A2, JORDAN11:9;
A24: [(X-SpanStart (C,n)),(Y-SpanStart (C,n))] in Indices (Gauge (C,n)) by A2, JORDAN11:8;
(X-SpanStart (C,n)) -' 1 <= X-SpanStart (C,n) by NAT_D:35;
then A25: (X-SpanStart (C,n)) + 1 <> (X-SpanStart (C,n)) -' 1 by NAT_1:13;
A26: Y-SpanStart (C,n) <> (Y-SpanStart (C,n)) + 1 ;
A27: ((Span (C,n)) | (k + 1)) /. 2 = (Gauge (C,n)) * (((X-SpanStart (C,n)) -' 1),(Y-SpanStart (C,n))) by A20, FINSEQ_4:17;
then right_cell (((Span (C,n)) | (k + 1)),m,(Gauge (C,n))) = cell ((Gauge (C,n)),((X-SpanStart (C,n)) -' 1),(Y-SpanStart (C,n))) by A8, A14, A21, A24, A23, A22, A26, A25, GOBRD13:def_2;
hence right_cell (((Span (C,n)) | (k + 1)),m,(Gauge (C,n))) misses C by A2, JORDAN11:11; ::_thesis: left_cell (((Span (C,n)) | (k + 1)),m,(Gauge (C,n))) meets C
left_cell (((Span (C,n)) | (k + 1)),m,(Gauge (C,n))) = cell ((Gauge (C,n)),((X-SpanStart (C,n)) -' 1),((Y-SpanStart (C,n)) -' 1)) by A8, A14, A21, A27, A24, A23, A22, A26, A25, GOBRD13:def_3;
hence left_cell (((Span (C,n)) | (k + 1)),m,(Gauge (C,n))) meets C by A2, JORDAN11:10; ::_thesis: verum
end;
supposeA28: k > 1 ; ::_thesis: ( right_cell (((Span (C,n)) | (k + 1)),m,(Gauge (C,n))) misses C & left_cell (((Span (C,n)) | (k + 1)),m,(Gauge (C,n))) meets C )
A29: len ((Span (C,n)) | k) <= len (Span (C,n)) by FINSEQ_5:16;
A30: 1 <= (len ((Span (C,n)) | k)) -' 1 by A17, A28, NAT_D:49;
A31: ((len ((Span (C,n)) | k)) -' 1) + 1 = len ((Span (C,n)) | k) by A17, A28, XREAL_1:235;
then A32: ((len ((Span (C,n)) | k)) -' 1) + (1 + 1) = (len ((Span (C,n)) | k)) + 1 ;
now__::_thesis:_(_right_cell_(((Span_(C,n))_|_(k_+_1)),m,(Gauge_(C,n)))_misses_C_&_left_cell_(((Span_(C,n))_|_(k_+_1)),m,(Gauge_(C,n)))_meets_C_)
percases ( m + 1 = len ((Span (C,n)) | (k + 1)) or m + 1 <> len ((Span (C,n)) | (k + 1)) ) ;
supposeA33: m + 1 = len ((Span (C,n)) | (k + 1)) ; ::_thesis: ( right_cell (((Span (C,n)) | (k + 1)),m,(Gauge (C,n))) misses C & left_cell (((Span (C,n)) | (k + 1)),m,(Gauge (C,n))) meets C )
left_cell (((Span (C,n)) | k),((len ((Span (C,n)) | k)) -' 1),(Gauge (C,n))) meets C by A7, A30, A31;
then A34: left_cell ((Span (C,n)),((len ((Span (C,n)) | k)) -' 1),(Gauge (C,n))) meets C by A3, A17, A30, A31, A29, GOBRD13:31;
consider i1, j1, i2, j2 being Element of NAT such that
A35: [i1,j1] in Indices (Gauge (C,n)) and
A36: (Span (C,n)) /. ((len ((Span (C,n)) | k)) -' 1) = (Gauge (C,n)) * (i1,j1) and
A37: [i2,j2] in Indices (Gauge (C,n)) and
A38: (Span (C,n)) /. (len ((Span (C,n)) | k)) = (Gauge (C,n)) * (i2,j2) and
( ( i1 = i2 & j1 + 1 = j2 ) or ( i1 + 1 = i2 & j1 = j2 ) or ( i1 = i2 + 1 & j1 = j2 ) or ( i1 = i2 & j1 = j2 + 1 ) ) by A3, A12, A17, A30, A31, JORDAN8:3;
1 <= i2 by A37, MATRIX_1:38;
then A39: (i2 -' 1) + 1 = i2 by XREAL_1:235;
A40: 1 <= j2 by A37, MATRIX_1:38;
then A41: (j2 -' 1) + 1 = j2 by XREAL_1:235;
right_cell (((Span (C,n)) | k),((len ((Span (C,n)) | k)) -' 1),(Gauge (C,n))) misses C by A7, A30, A31;
then A42: right_cell ((Span (C,n)),((len ((Span (C,n)) | k)) -' 1),(Gauge (C,n))) misses C by A3, A17, A30, A31, A29, GOBRD13:31;
now__::_thesis:_(_right_cell_(((Span_(C,n))_|_(k_+_1)),m,(Gauge_(C,n)))_misses_C_&_left_cell_(((Span_(C,n))_|_(k_+_1)),m,(Gauge_(C,n)))_meets_C_)
percases ( ( front_right_cell ((Span (C,n)),((len ((Span (C,n)) | k)) -' 1),(Gauge (C,n))) misses C & front_left_cell ((Span (C,n)),((len ((Span (C,n)) | k)) -' 1),(Gauge (C,n))) misses C ) or ( front_right_cell ((Span (C,n)),((len ((Span (C,n)) | k)) -' 1),(Gauge (C,n))) misses C & front_left_cell ((Span (C,n)),((len ((Span (C,n)) | k)) -' 1),(Gauge (C,n))) meets C ) or front_right_cell ((Span (C,n)),((len ((Span (C,n)) | k)) -' 1),(Gauge (C,n))) meets C ) ;
supposeA43: ( front_right_cell ((Span (C,n)),((len ((Span (C,n)) | k)) -' 1),(Gauge (C,n))) misses C & front_left_cell ((Span (C,n)),((len ((Span (C,n)) | k)) -' 1),(Gauge (C,n))) misses C ) ; ::_thesis: ( right_cell (((Span (C,n)) | (k + 1)),m,(Gauge (C,n))) misses C & left_cell (((Span (C,n)) | (k + 1)),m,(Gauge (C,n))) meets C )
then A44: Span (C,n) turns_left (len ((Span (C,n)) | k)) -' 1, Gauge (C,n) by A2, A15, A17, A30, A32, JORDAN13:def_1;
now__::_thesis:_(_right_cell_(((Span_(C,n))_|_(k_+_1)),m,(Gauge_(C,n)))_misses_C_&_left_cell_(((Span_(C,n))_|_(k_+_1)),m,(Gauge_(C,n)))_meets_C_)
percases ( ( i1 = i2 & j1 + 1 = j2 & [(i2 -' 1),j2] in Indices (Gauge (C,n)) & (Span (C,n)) /. (((len ((Span (C,n)) | k)) -' 1) + 2) = (Gauge (C,n)) * ((i2 -' 1),j2) ) or ( i1 + 1 = i2 & j1 = j2 & [i2,(j2 + 1)] in Indices (Gauge (C,n)) & (Span (C,n)) /. (((len ((Span (C,n)) | k)) -' 1) + 2) = (Gauge (C,n)) * (i2,(j2 + 1)) ) or ( i1 = i2 + 1 & j1 = j2 & [i2,(j2 -' 1)] in Indices (Gauge (C,n)) & (Span (C,n)) /. (((len ((Span (C,n)) | k)) -' 1) + 2) = (Gauge (C,n)) * (i2,(j2 -' 1)) ) or ( i1 = i2 & j1 = j2 + 1 & [(i2 + 1),j2] in Indices (Gauge (C,n)) & (Span (C,n)) /. (((len ((Span (C,n)) | k)) -' 1) + 2) = (Gauge (C,n)) * ((i2 + 1),j2) ) ) by A31, A35, A36, A37, A38, A44, GOBRD13:def_7;
supposethat A45: ( i1 = i2 & j1 + 1 = j2 ) and
A46: [(i2 -' 1),j2] in Indices (Gauge (C,n)) and
A47: (Span (C,n)) /. (((len ((Span (C,n)) | k)) -' 1) + 2) = (Gauge (C,n)) * ((i2 -' 1),j2) ; ::_thesis: ( right_cell (((Span (C,n)) | (k + 1)),m,(Gauge (C,n))) misses C & left_cell (((Span (C,n)) | (k + 1)),m,(Gauge (C,n))) meets C )
cell ((Gauge (C,n)),(i1 -' 1),(j1 + 1)) misses C by A3, A30, A31, A29, A35, A36, A37, A38, A43, A45, GOBRD13:34;
then right_cell ((Span (C,n)),m,(Gauge (C,n))) misses C by A3, A15, A16, A17, A28, A31, A33, A37, A38, A39, A45, A46, A47, GOBRD13:26;
hence right_cell (((Span (C,n)) | (k + 1)),m,(Gauge (C,n))) misses C by A3, A15, A16, A13, A33, GOBRD13:31; ::_thesis: left_cell (((Span (C,n)) | (k + 1)),m,(Gauge (C,n))) meets C
A48: (j1 + 1) -' 1 = j1 by NAT_D:34;
cell ((Gauge (C,n)),(i1 -' 1),j1) meets C by A3, A12, A17, A30, A31, A35, A36, A37, A38, A34, A45, GOBRD13:21;
then left_cell ((Span (C,n)),m,(Gauge (C,n))) meets C by A3, A15, A16, A17, A28, A31, A33, A37, A38, A39, A45, A46, A47, A48, GOBRD13:25;
hence left_cell (((Span (C,n)) | (k + 1)),m,(Gauge (C,n))) meets C by A3, A15, A16, A13, A33, GOBRD13:31; ::_thesis: verum
end;
supposethat A49: ( i1 + 1 = i2 & j1 = j2 ) and
A50: [i2,(j2 + 1)] in Indices (Gauge (C,n)) and
A51: (Span (C,n)) /. (((len ((Span (C,n)) | k)) -' 1) + 2) = (Gauge (C,n)) * (i2,(j2 + 1)) ; ::_thesis: ( right_cell (((Span (C,n)) | (k + 1)),m,(Gauge (C,n))) misses C & left_cell (((Span (C,n)) | (k + 1)),m,(Gauge (C,n))) meets C )
cell ((Gauge (C,n)),i2,j2) misses C by A3, A30, A31, A29, A35, A36, A37, A38, A43, A49, GOBRD13:36;
then right_cell ((Span (C,n)),m,(Gauge (C,n))) misses C by A3, A15, A16, A17, A28, A31, A33, A37, A38, A50, A51, GOBRD13:22;
hence right_cell (((Span (C,n)) | (k + 1)),m,(Gauge (C,n))) misses C by A3, A15, A16, A13, A33, GOBRD13:31; ::_thesis: left_cell (((Span (C,n)) | (k + 1)),m,(Gauge (C,n))) meets C
A52: (i1 + 1) -' 1 = i1 by NAT_D:34;
cell ((Gauge (C,n)),i1,j2) meets C by A3, A12, A17, A30, A31, A35, A36, A37, A38, A34, A49, GOBRD13:23;
then left_cell ((Span (C,n)),m,(Gauge (C,n))) meets C by A3, A15, A16, A17, A28, A31, A33, A37, A38, A49, A50, A51, A52, GOBRD13:21;
hence left_cell (((Span (C,n)) | (k + 1)),m,(Gauge (C,n))) meets C by A3, A15, A16, A13, A33, GOBRD13:31; ::_thesis: verum
end;
supposethat A53: ( i1 = i2 + 1 & j1 = j2 ) and
A54: [i2,(j2 -' 1)] in Indices (Gauge (C,n)) and
A55: (Span (C,n)) /. (((len ((Span (C,n)) | k)) -' 1) + 2) = (Gauge (C,n)) * (i2,(j2 -' 1)) ; ::_thesis: ( right_cell (((Span (C,n)) | (k + 1)),m,(Gauge (C,n))) misses C & left_cell (((Span (C,n)) | (k + 1)),m,(Gauge (C,n))) meets C )
cell ((Gauge (C,n)),(i2 -' 1),(j2 -' 1)) misses C by A3, A30, A31, A29, A35, A36, A37, A38, A43, A53, GOBRD13:38;
then right_cell ((Span (C,n)),m,(Gauge (C,n))) misses C by A3, A15, A16, A17, A28, A31, A33, A37, A38, A41, A54, A55, GOBRD13:28;
hence right_cell (((Span (C,n)) | (k + 1)),m,(Gauge (C,n))) misses C by A3, A15, A16, A13, A33, GOBRD13:31; ::_thesis: left_cell (((Span (C,n)) | (k + 1)),m,(Gauge (C,n))) meets C
cell ((Gauge (C,n)),i2,(j2 -' 1)) meets C by A3, A12, A17, A30, A31, A35, A36, A37, A38, A34, A53, GOBRD13:25;
then left_cell ((Span (C,n)),m,(Gauge (C,n))) meets C by A3, A15, A16, A17, A28, A31, A33, A37, A38, A41, A54, A55, GOBRD13:27;
hence left_cell (((Span (C,n)) | (k + 1)),m,(Gauge (C,n))) meets C by A3, A15, A16, A13, A33, GOBRD13:31; ::_thesis: verum
end;
supposethat A56: ( i1 = i2 & j1 = j2 + 1 ) and
A57: [(i2 + 1),j2] in Indices (Gauge (C,n)) and
A58: (Span (C,n)) /. (((len ((Span (C,n)) | k)) -' 1) + 2) = (Gauge (C,n)) * ((i2 + 1),j2) ; ::_thesis: ( right_cell (((Span (C,n)) | (k + 1)),m,(Gauge (C,n))) misses C & left_cell (((Span (C,n)) | (k + 1)),m,(Gauge (C,n))) meets C )
cell ((Gauge (C,n)),i1,(j2 -' 1)) misses C by A3, A30, A31, A29, A35, A36, A37, A38, A43, A56, GOBRD13:40;
then right_cell ((Span (C,n)),m,(Gauge (C,n))) misses C by A3, A15, A16, A17, A28, A31, A33, A37, A38, A56, A57, A58, GOBRD13:24;
hence right_cell (((Span (C,n)) | (k + 1)),m,(Gauge (C,n))) misses C by A3, A15, A16, A13, A33, GOBRD13:31; ::_thesis: left_cell (((Span (C,n)) | (k + 1)),m,(Gauge (C,n))) meets C
cell ((Gauge (C,n)),i1,j2) meets C by A3, A12, A17, A30, A31, A35, A36, A37, A38, A34, A56, GOBRD13:27;
then left_cell ((Span (C,n)),m,(Gauge (C,n))) meets C by A3, A15, A16, A17, A28, A31, A33, A37, A38, A56, A57, A58, GOBRD13:23;
hence left_cell (((Span (C,n)) | (k + 1)),m,(Gauge (C,n))) meets C by A3, A15, A16, A13, A33, GOBRD13:31; ::_thesis: verum
end;
end;
end;
hence ( right_cell (((Span (C,n)) | (k + 1)),m,(Gauge (C,n))) misses C & left_cell (((Span (C,n)) | (k + 1)),m,(Gauge (C,n))) meets C ) ; ::_thesis: verum
end;
supposeA59: ( front_right_cell ((Span (C,n)),((len ((Span (C,n)) | k)) -' 1),(Gauge (C,n))) misses C & front_left_cell ((Span (C,n)),((len ((Span (C,n)) | k)) -' 1),(Gauge (C,n))) meets C ) ; ::_thesis: ( right_cell (((Span (C,n)) | (k + 1)),m,(Gauge (C,n))) misses C & left_cell (((Span (C,n)) | (k + 1)),m,(Gauge (C,n))) meets C )
then A60: Span (C,n) goes_straight (len ((Span (C,n)) | k)) -' 1, Gauge (C,n) by A2, A15, A17, A30, A32, JORDAN13:def_1;
now__::_thesis:_(_right_cell_(((Span_(C,n))_|_(k_+_1)),m,(Gauge_(C,n)))_misses_C_&_left_cell_(((Span_(C,n))_|_(k_+_1)),m,(Gauge_(C,n)))_meets_C_)
percases ( ( i1 = i2 & j1 + 1 = j2 & [i2,(j2 + 1)] in Indices (Gauge (C,n)) & (Span (C,n)) /. (((len ((Span (C,n)) | k)) -' 1) + 2) = (Gauge (C,n)) * (i2,(j2 + 1)) ) or ( i1 + 1 = i2 & j1 = j2 & [(i2 + 1),j2] in Indices (Gauge (C,n)) & (Span (C,n)) /. (((len ((Span (C,n)) | k)) -' 1) + 2) = (Gauge (C,n)) * ((i2 + 1),j2) ) or ( i1 = i2 + 1 & j1 = j2 & [(i2 -' 1),j2] in Indices (Gauge (C,n)) & (Span (C,n)) /. (((len ((Span (C,n)) | k)) -' 1) + 2) = (Gauge (C,n)) * ((i2 -' 1),j2) ) or ( i1 = i2 & j1 = j2 + 1 & [i2,(j2 -' 1)] in Indices (Gauge (C,n)) & (Span (C,n)) /. (((len ((Span (C,n)) | k)) -' 1) + 2) = (Gauge (C,n)) * (i2,(j2 -' 1)) ) ) by A31, A35, A36, A37, A38, A60, GOBRD13:def_8;
supposethat A61: ( i1 = i2 & j1 + 1 = j2 ) and
A62: [i2,(j2 + 1)] in Indices (Gauge (C,n)) and
A63: (Span (C,n)) /. (((len ((Span (C,n)) | k)) -' 1) + 2) = (Gauge (C,n)) * (i2,(j2 + 1)) ; ::_thesis: ( right_cell (((Span (C,n)) | (k + 1)),m,(Gauge (C,n))) misses C & left_cell (((Span (C,n)) | (k + 1)),m,(Gauge (C,n))) meets C )
cell ((Gauge (C,n)),i1,(j1 + 1)) misses C by A3, A30, A31, A29, A35, A36, A37, A38, A59, A61, GOBRD13:35;
then right_cell ((Span (C,n)),m,(Gauge (C,n))) misses C by A3, A15, A16, A17, A28, A31, A33, A37, A38, A61, A62, A63, GOBRD13:22;
hence right_cell (((Span (C,n)) | (k + 1)),m,(Gauge (C,n))) misses C by A3, A15, A16, A13, A33, GOBRD13:31; ::_thesis: left_cell (((Span (C,n)) | (k + 1)),m,(Gauge (C,n))) meets C
cell ((Gauge (C,n)),(i2 -' 1),j2) meets C by A3, A12, A17, A30, A31, A35, A36, A37, A38, A59, A61, GOBRD13:34;
then left_cell ((Span (C,n)),m,(Gauge (C,n))) meets C by A3, A15, A16, A17, A28, A31, A33, A37, A38, A62, A63, GOBRD13:21;
hence left_cell (((Span (C,n)) | (k + 1)),m,(Gauge (C,n))) meets C by A3, A15, A16, A13, A33, GOBRD13:31; ::_thesis: verum
end;
supposethat A64: ( i1 + 1 = i2 & j1 = j2 ) and
A65: [(i2 + 1),j2] in Indices (Gauge (C,n)) and
A66: (Span (C,n)) /. (((len ((Span (C,n)) | k)) -' 1) + 2) = (Gauge (C,n)) * ((i2 + 1),j2) ; ::_thesis: ( right_cell (((Span (C,n)) | (k + 1)),m,(Gauge (C,n))) misses C & left_cell (((Span (C,n)) | (k + 1)),m,(Gauge (C,n))) meets C )
cell ((Gauge (C,n)),(i1 + 1),(j1 -' 1)) misses C by A3, A30, A31, A29, A35, A36, A37, A38, A59, A64, GOBRD13:37;
then right_cell ((Span (C,n)),m,(Gauge (C,n))) misses C by A3, A15, A16, A17, A28, A31, A33, A37, A38, A64, A65, A66, GOBRD13:24;
hence right_cell (((Span (C,n)) | (k + 1)),m,(Gauge (C,n))) misses C by A3, A15, A16, A13, A33, GOBRD13:31; ::_thesis: left_cell (((Span (C,n)) | (k + 1)),m,(Gauge (C,n))) meets C
cell ((Gauge (C,n)),(i1 + 1),j1) meets C by A3, A12, A17, A30, A31, A35, A36, A37, A38, A59, A64, GOBRD13:36;
then left_cell ((Span (C,n)),m,(Gauge (C,n))) meets C by A3, A15, A16, A17, A28, A31, A33, A37, A38, A64, A65, A66, GOBRD13:23;
hence left_cell (((Span (C,n)) | (k + 1)),m,(Gauge (C,n))) meets C by A3, A15, A16, A13, A33, GOBRD13:31; ::_thesis: verum
end;
supposethat A67: ( i1 = i2 + 1 & j1 = j2 ) and
A68: [(i2 -' 1),j2] in Indices (Gauge (C,n)) and
A69: (Span (C,n)) /. (((len ((Span (C,n)) | k)) -' 1) + 2) = (Gauge (C,n)) * ((i2 -' 1),j2) ; ::_thesis: ( right_cell (((Span (C,n)) | (k + 1)),m,(Gauge (C,n))) misses C & left_cell (((Span (C,n)) | (k + 1)),m,(Gauge (C,n))) meets C )
cell ((Gauge (C,n)),(i2 -' 1),j2) misses C by A3, A30, A31, A29, A35, A36, A37, A38, A59, A67, GOBRD13:39;
then right_cell ((Span (C,n)),m,(Gauge (C,n))) misses C by A3, A15, A16, A17, A28, A31, A33, A37, A38, A39, A68, A69, GOBRD13:26;
hence right_cell (((Span (C,n)) | (k + 1)),m,(Gauge (C,n))) misses C by A3, A15, A16, A13, A33, GOBRD13:31; ::_thesis: left_cell (((Span (C,n)) | (k + 1)),m,(Gauge (C,n))) meets C
cell ((Gauge (C,n)),(i2 -' 1),(j2 -' 1)) meets C by A3, A12, A17, A30, A31, A35, A36, A37, A38, A59, A67, GOBRD13:38;
then left_cell ((Span (C,n)),m,(Gauge (C,n))) meets C by A3, A15, A16, A17, A28, A31, A33, A37, A38, A39, A68, A69, GOBRD13:25;
hence left_cell (((Span (C,n)) | (k + 1)),m,(Gauge (C,n))) meets C by A3, A15, A16, A13, A33, GOBRD13:31; ::_thesis: verum
end;
supposethat A70: ( i1 = i2 & j1 = j2 + 1 ) and
A71: [i2,(j2 -' 1)] in Indices (Gauge (C,n)) and
A72: (Span (C,n)) /. (((len ((Span (C,n)) | k)) -' 1) + 2) = (Gauge (C,n)) * (i2,(j2 -' 1)) ; ::_thesis: ( right_cell (((Span (C,n)) | (k + 1)),m,(Gauge (C,n))) misses C & left_cell (((Span (C,n)) | (k + 1)),m,(Gauge (C,n))) meets C )
A73: (j2 -' 1) + 1 = j2 by A40, XREAL_1:235;
cell ((Gauge (C,n)),(i2 -' 1),(j2 -' 1)) misses C by A3, A30, A31, A29, A35, A36, A37, A38, A59, A70, GOBRD13:41;
then right_cell ((Span (C,n)),m,(Gauge (C,n))) misses C by A3, A15, A16, A17, A28, A31, A33, A37, A38, A71, A72, A73, GOBRD13:28;
hence right_cell (((Span (C,n)) | (k + 1)),m,(Gauge (C,n))) misses C by A3, A15, A16, A13, A33, GOBRD13:31; ::_thesis: left_cell (((Span (C,n)) | (k + 1)),m,(Gauge (C,n))) meets C
cell ((Gauge (C,n)),i2,(j2 -' 1)) meets C by A3, A12, A17, A30, A31, A35, A36, A37, A38, A59, A70, GOBRD13:40;
then left_cell ((Span (C,n)),m,(Gauge (C,n))) meets C by A3, A15, A16, A17, A28, A31, A33, A37, A38, A41, A71, A72, GOBRD13:27;
hence left_cell (((Span (C,n)) | (k + 1)),m,(Gauge (C,n))) meets C by A3, A15, A16, A13, A33, GOBRD13:31; ::_thesis: verum
end;
end;
end;
hence ( right_cell (((Span (C,n)) | (k + 1)),m,(Gauge (C,n))) misses C & left_cell (((Span (C,n)) | (k + 1)),m,(Gauge (C,n))) meets C ) ; ::_thesis: verum
end;
supposeA74: front_right_cell ((Span (C,n)),((len ((Span (C,n)) | k)) -' 1),(Gauge (C,n))) meets C ; ::_thesis: ( right_cell (((Span (C,n)) | (k + 1)),m,(Gauge (C,n))) misses C & left_cell (((Span (C,n)) | (k + 1)),m,(Gauge (C,n))) meets C )
then A75: Span (C,n) turns_right (len ((Span (C,n)) | k)) -' 1, Gauge (C,n) by A2, A15, A17, A30, A32, JORDAN13:def_1;
now__::_thesis:_(_right_cell_(((Span_(C,n))_|_(k_+_1)),m,(Gauge_(C,n)))_misses_C_&_left_cell_(((Span_(C,n))_|_(k_+_1)),m,(Gauge_(C,n)))_meets_C_)
percases ( ( i1 = i2 & j1 + 1 = j2 & [(i2 + 1),j2] in Indices (Gauge (C,n)) & (Span (C,n)) /. (((len ((Span (C,n)) | k)) -' 1) + 2) = (Gauge (C,n)) * ((i2 + 1),j2) ) or ( i1 + 1 = i2 & j1 = j2 & [i2,(j2 -' 1)] in Indices (Gauge (C,n)) & (Span (C,n)) /. (((len ((Span (C,n)) | k)) -' 1) + 2) = (Gauge (C,n)) * (i2,(j2 -' 1)) ) or ( i1 = i2 + 1 & j1 = j2 & [i2,(j2 + 1)] in Indices (Gauge (C,n)) & (Span (C,n)) /. (((len ((Span (C,n)) | k)) -' 1) + 2) = (Gauge (C,n)) * (i2,(j2 + 1)) ) or ( i1 = i2 & j1 = j2 + 1 & [(i2 -' 1),j2] in Indices (Gauge (C,n)) & (Span (C,n)) /. (((len ((Span (C,n)) | k)) -' 1) + 2) = (Gauge (C,n)) * ((i2 -' 1),j2) ) ) by A31, A35, A36, A37, A38, A75, GOBRD13:def_6;
supposethat A76: ( i1 = i2 & j1 + 1 = j2 ) and
A77: [(i2 + 1),j2] in Indices (Gauge (C,n)) and
A78: (Span (C,n)) /. (((len ((Span (C,n)) | k)) -' 1) + 2) = (Gauge (C,n)) * ((i2 + 1),j2) ; ::_thesis: ( right_cell (((Span (C,n)) | (k + 1)),m,(Gauge (C,n))) misses C & left_cell (((Span (C,n)) | (k + 1)),m,(Gauge (C,n))) meets C )
A79: (j1 + 1) -' 1 = j1 by NAT_D:34;
cell ((Gauge (C,n)),i1,j1) misses C by A3, A30, A31, A29, A35, A36, A37, A38, A42, A76, GOBRD13:22;
then right_cell ((Span (C,n)),m,(Gauge (C,n))) misses C by A3, A15, A16, A17, A28, A31, A33, A37, A38, A76, A77, A78, A79, GOBRD13:24;
hence right_cell (((Span (C,n)) | (k + 1)),m,(Gauge (C,n))) misses C by A3, A15, A16, A13, A33, GOBRD13:31; ::_thesis: left_cell (((Span (C,n)) | (k + 1)),m,(Gauge (C,n))) meets C
cell ((Gauge (C,n)),i2,j2) meets C by A3, A12, A17, A30, A31, A35, A36, A37, A38, A74, A76, GOBRD13:35;
then left_cell ((Span (C,n)),m,(Gauge (C,n))) meets C by A3, A15, A16, A17, A28, A31, A33, A37, A38, A77, A78, GOBRD13:23;
hence left_cell (((Span (C,n)) | (k + 1)),m,(Gauge (C,n))) meets C by A3, A15, A16, A13, A33, GOBRD13:31; ::_thesis: verum
end;
supposethat A80: ( i1 + 1 = i2 & j1 = j2 ) and
A81: [i2,(j2 -' 1)] in Indices (Gauge (C,n)) and
A82: (Span (C,n)) /. (((len ((Span (C,n)) | k)) -' 1) + 2) = (Gauge (C,n)) * (i2,(j2 -' 1)) ; ::_thesis: ( right_cell (((Span (C,n)) | (k + 1)),m,(Gauge (C,n))) misses C & left_cell (((Span (C,n)) | (k + 1)),m,(Gauge (C,n))) meets C )
A83: (i1 + 1) -' 1 = i1 by NAT_D:34;
cell ((Gauge (C,n)),i1,(j1 -' 1)) misses C by A3, A30, A31, A29, A35, A36, A37, A38, A42, A80, GOBRD13:24;
then right_cell ((Span (C,n)),m,(Gauge (C,n))) misses C by A3, A15, A16, A17, A28, A31, A33, A37, A38, A41, A80, A81, A82, A83, GOBRD13:28;
hence right_cell (((Span (C,n)) | (k + 1)),m,(Gauge (C,n))) misses C by A3, A15, A16, A13, A33, GOBRD13:31; ::_thesis: left_cell (((Span (C,n)) | (k + 1)),m,(Gauge (C,n))) meets C
cell ((Gauge (C,n)),i2,(j2 -' 1)) meets C by A3, A12, A17, A30, A31, A35, A36, A37, A38, A74, A80, GOBRD13:37;
then left_cell ((Span (C,n)),m,(Gauge (C,n))) meets C by A3, A15, A16, A17, A28, A31, A33, A37, A38, A41, A81, A82, GOBRD13:27;
hence left_cell (((Span (C,n)) | (k + 1)),m,(Gauge (C,n))) meets C by A3, A15, A16, A13, A33, GOBRD13:31; ::_thesis: verum
end;
supposethat A84: ( i1 = i2 + 1 & j1 = j2 ) and
A85: [i2,(j2 + 1)] in Indices (Gauge (C,n)) and
A86: (Span (C,n)) /. (((len ((Span (C,n)) | k)) -' 1) + 2) = (Gauge (C,n)) * (i2,(j2 + 1)) ; ::_thesis: ( right_cell (((Span (C,n)) | (k + 1)),m,(Gauge (C,n))) misses C & left_cell (((Span (C,n)) | (k + 1)),m,(Gauge (C,n))) meets C )
cell ((Gauge (C,n)),i2,j2) misses C by A3, A30, A31, A29, A35, A36, A37, A38, A42, A84, GOBRD13:26;
then right_cell ((Span (C,n)),m,(Gauge (C,n))) misses C by A3, A15, A16, A17, A28, A31, A33, A37, A38, A85, A86, GOBRD13:22;
hence right_cell (((Span (C,n)) | (k + 1)),m,(Gauge (C,n))) misses C by A3, A15, A16, A13, A33, GOBRD13:31; ::_thesis: left_cell (((Span (C,n)) | (k + 1)),m,(Gauge (C,n))) meets C
cell ((Gauge (C,n)),(i2 -' 1),j2) meets C by A3, A12, A17, A30, A31, A35, A36, A37, A38, A74, A84, GOBRD13:39;
then left_cell ((Span (C,n)),m,(Gauge (C,n))) meets C by A3, A15, A16, A17, A28, A31, A33, A37, A38, A85, A86, GOBRD13:21;
hence left_cell (((Span (C,n)) | (k + 1)),m,(Gauge (C,n))) meets C by A3, A15, A16, A13, A33, GOBRD13:31; ::_thesis: verum
end;
supposethat A87: ( i1 = i2 & j1 = j2 + 1 ) and
A88: [(i2 -' 1),j2] in Indices (Gauge (C,n)) and
A89: (Span (C,n)) /. (((len ((Span (C,n)) | k)) -' 1) + 2) = (Gauge (C,n)) * ((i2 -' 1),j2) ; ::_thesis: ( right_cell (((Span (C,n)) | (k + 1)),m,(Gauge (C,n))) misses C & left_cell (((Span (C,n)) | (k + 1)),m,(Gauge (C,n))) meets C )
cell ((Gauge (C,n)),(i2 -' 1),j2) misses C by A3, A30, A31, A29, A35, A36, A37, A38, A42, A87, GOBRD13:28;
then right_cell ((Span (C,n)),m,(Gauge (C,n))) misses C by A3, A15, A16, A17, A28, A31, A33, A37, A38, A39, A88, A89, GOBRD13:26;
hence right_cell (((Span (C,n)) | (k + 1)),m,(Gauge (C,n))) misses C by A3, A15, A16, A13, A33, GOBRD13:31; ::_thesis: left_cell (((Span (C,n)) | (k + 1)),m,(Gauge (C,n))) meets C
cell ((Gauge (C,n)),(i2 -' 1),(j2 -' 1)) meets C by A3, A12, A17, A30, A31, A35, A36, A37, A38, A74, A87, GOBRD13:41;
then left_cell ((Span (C,n)),m,(Gauge (C,n))) meets C by A3, A15, A16, A17, A28, A31, A33, A37, A38, A39, A88, A89, GOBRD13:25;
hence left_cell (((Span (C,n)) | (k + 1)),m,(Gauge (C,n))) meets C by A3, A15, A16, A13, A33, GOBRD13:31; ::_thesis: verum
end;
end;
end;
hence ( right_cell (((Span (C,n)) | (k + 1)),m,(Gauge (C,n))) misses C & left_cell (((Span (C,n)) | (k + 1)),m,(Gauge (C,n))) meets C ) ; ::_thesis: verum
end;
end;
end;
hence ( right_cell (((Span (C,n)) | (k + 1)),m,(Gauge (C,n))) misses C & left_cell (((Span (C,n)) | (k + 1)),m,(Gauge (C,n))) meets C ) ; ::_thesis: verum
end;
suppose m + 1 <> len ((Span (C,n)) | (k + 1)) ; ::_thesis: ( right_cell (((Span (C,n)) | (k + 1)),m,(Gauge (C,n))) misses C & left_cell (((Span (C,n)) | (k + 1)),m,(Gauge (C,n))) meets C )
then m + 1 < len ((Span (C,n)) | (k + 1)) by A14, XXREAL_0:1;
then A90: m + 1 <= len ((Span (C,n)) | k) by A16, A17, NAT_1:13;
then consider i1, j1, i2, j2 being Element of NAT such that
A91: [i1,j1] in Indices (Gauge (C,n)) and
A92: ((Span (C,n)) | k) /. m = (Gauge (C,n)) * (i1,j1) and
A93: [i2,j2] in Indices (Gauge (C,n)) and
A94: ((Span (C,n)) | k) /. (m + 1) = (Gauge (C,n)) * (i2,j2) and
A95: ( ( 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, A13, JORDAN8:3;
A96: right_cell (((Span (C,n)) | k),m,(Gauge (C,n))) misses C by A7, A13, A90;
A97: (Span (C,n)) | (k + 1) = ((Span (C,n)) | k) ^ <*((Span (C,n)) /. (k + 1))*> by A15, FINSEQ_5:82;
1 <= m + 1 by NAT_1:12;
then m + 1 in dom ((Span (C,n)) | k) by A90, FINSEQ_3:25;
then A98: ((Span (C,n)) | (k + 1)) /. (m + 1) = (Gauge (C,n)) * (i2,j2) by A94, A97, FINSEQ_4:68;
A99: left_cell (((Span (C,n)) | k),m,(Gauge (C,n))) meets C by A7, A13, A90;
m <= len ((Span (C,n)) | k) by A90, NAT_1:13;
then m in dom ((Span (C,n)) | k) by A13, FINSEQ_3:25;
then A100: ((Span (C,n)) | (k + 1)) /. m = (Gauge (C,n)) * (i1,j1) by A92, A97, FINSEQ_4:68;
now__::_thesis:_(_right_cell_(((Span_(C,n))_|_(k_+_1)),m,(Gauge_(C,n)))_misses_C_&_left_cell_(((Span_(C,n))_|_(k_+_1)),m,(Gauge_(C,n)))_meets_C_)
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 A95;
supposeA101: ( i1 = i2 & j1 + 1 = j2 ) ; ::_thesis: ( right_cell (((Span (C,n)) | (k + 1)),m,(Gauge (C,n))) misses C & left_cell (((Span (C,n)) | (k + 1)),m,(Gauge (C,n))) meets C )
then A102: left_cell (((Span (C,n)) | k),m,(Gauge (C,n))) = cell ((Gauge (C,n)),(i1 -' 1),j1) by A9, A13, A90, A91, A92, A93, A94, GOBRD13:21;
right_cell (((Span (C,n)) | k),m,(Gauge (C,n))) = cell ((Gauge (C,n)),i1,j1) by A9, A13, A90, A91, A92, A93, A94, A101, GOBRD13:22;
hence ( right_cell (((Span (C,n)) | (k + 1)),m,(Gauge (C,n))) misses C & left_cell (((Span (C,n)) | (k + 1)),m,(Gauge (C,n))) meets C ) by A8, A13, A14, A91, A93, A96, A99, A100, A98, A101, A102, GOBRD13:21, GOBRD13:22; ::_thesis: verum
end;
supposeA103: ( i1 + 1 = i2 & j1 = j2 ) ; ::_thesis: ( right_cell (((Span (C,n)) | (k + 1)),m,(Gauge (C,n))) misses C & left_cell (((Span (C,n)) | (k + 1)),m,(Gauge (C,n))) meets C )
then A104: left_cell (((Span (C,n)) | k),m,(Gauge (C,n))) = cell ((Gauge (C,n)),i1,j1) by A9, A13, A90, A91, A92, A93, A94, GOBRD13:23;
right_cell (((Span (C,n)) | k),m,(Gauge (C,n))) = cell ((Gauge (C,n)),i1,(j1 -' 1)) by A9, A13, A90, A91, A92, A93, A94, A103, GOBRD13:24;
hence ( right_cell (((Span (C,n)) | (k + 1)),m,(Gauge (C,n))) misses C & left_cell (((Span (C,n)) | (k + 1)),m,(Gauge (C,n))) meets C ) by A8, A13, A14, A91, A93, A96, A99, A100, A98, A103, A104, GOBRD13:23, GOBRD13:24; ::_thesis: verum
end;
supposeA105: ( i1 = i2 + 1 & j1 = j2 ) ; ::_thesis: ( right_cell (((Span (C,n)) | (k + 1)),m,(Gauge (C,n))) misses C & left_cell (((Span (C,n)) | (k + 1)),m,(Gauge (C,n))) meets C )
then A106: left_cell (((Span (C,n)) | k),m,(Gauge (C,n))) = cell ((Gauge (C,n)),i2,(j2 -' 1)) by A9, A13, A90, A91, A92, A93, A94, GOBRD13:25;
right_cell (((Span (C,n)) | k),m,(Gauge (C,n))) = cell ((Gauge (C,n)),i2,j2) by A9, A13, A90, A91, A92, A93, A94, A105, GOBRD13:26;
hence ( right_cell (((Span (C,n)) | (k + 1)),m,(Gauge (C,n))) misses C & left_cell (((Span (C,n)) | (k + 1)),m,(Gauge (C,n))) meets C ) by A8, A13, A14, A91, A93, A96, A99, A100, A98, A105, A106, GOBRD13:25, GOBRD13:26; ::_thesis: verum
end;
supposeA107: ( i1 = i2 & j1 = j2 + 1 ) ; ::_thesis: ( right_cell (((Span (C,n)) | (k + 1)),m,(Gauge (C,n))) misses C & left_cell (((Span (C,n)) | (k + 1)),m,(Gauge (C,n))) meets C )
then A108: left_cell (((Span (C,n)) | k),m,(Gauge (C,n))) = cell ((Gauge (C,n)),i1,j2) by A9, A13, A90, A91, A92, A93, A94, GOBRD13:27;
right_cell (((Span (C,n)) | k),m,(Gauge (C,n))) = cell ((Gauge (C,n)),(i2 -' 1),j2) by A9, A13, A90, A91, A92, A93, A94, A107, GOBRD13:28;
hence ( right_cell (((Span (C,n)) | (k + 1)),m,(Gauge (C,n))) misses C & left_cell (((Span (C,n)) | (k + 1)),m,(Gauge (C,n))) meets C ) by A8, A13, A14, A91, A93, A96, A99, A100, A98, A107, A108, GOBRD13:27, GOBRD13:28; ::_thesis: verum
end;
end;
end;
hence ( right_cell (((Span (C,n)) | (k + 1)),m,(Gauge (C,n))) misses C & left_cell (((Span (C,n)) | (k + 1)),m,(Gauge (C,n))) meets C ) ; ::_thesis: verum
end;
end;
end;
hence ( right_cell (((Span (C,n)) | (k + 1)),m,(Gauge (C,n))) misses C & left_cell (((Span (C,n)) | (k + 1)),m,(Gauge (C,n))) meets C ) ; ::_thesis: verum
end;
end;
end;
hence ( right_cell (((Span (C,n)) | (k + 1)),m,(Gauge (C,n))) misses C & left_cell (((Span (C,n)) | (k + 1)),m,(Gauge (C,n))) meets C ) ; ::_thesis: verum
end;
end;
end;
A109: S1[ 0 ]
proof
let m be Element of NAT ; ::_thesis: ( 1 <= m & m + 1 <= len ((Span (C,n)) | 0) implies ( right_cell (((Span (C,n)) | 0),m,(Gauge (C,n))) misses C & left_cell (((Span (C,n)) | 0),m,(Gauge (C,n))) meets C ) )
assume that
1 <= m and
A110: m + 1 <= len ((Span (C,n)) | 0) ; ::_thesis: ( right_cell (((Span (C,n)) | 0),m,(Gauge (C,n))) misses C & left_cell (((Span (C,n)) | 0),m,(Gauge (C,n))) meets C )
1 <= m + 1 by NAT_1:12;
hence ( right_cell (((Span (C,n)) | 0),m,(Gauge (C,n))) misses C & left_cell (((Span (C,n)) | 0),m,(Gauge (C,n))) meets C ) by A110, CARD_1:27, XXREAL_0:2; ::_thesis: verum
end;
for k being Element of NAT holds S1[k] from NAT_1:sch_1(A109, A6);
hence ( not 1 <= k or not k + 1 <= len (Span (C,n)) or ( right_cell ((Span (C,n)),k,(Gauge (C,n))) misses C & left_cell ((Span (C,n)),k,(Gauge (C,n))) meets C ) ) by A1; ::_thesis: verum
end;
theorem Th8: :: JORDAN14:8
for C being Simple_closed_curve
for n being Element of NAT st n is_sufficiently_large_for C holds
C misses L~ (Span (C,n))
proof
let C be Simple_closed_curve; ::_thesis: for n being Element of NAT st n is_sufficiently_large_for C holds
C misses L~ (Span (C,n))
let n be Element of NAT ; ::_thesis: ( n is_sufficiently_large_for C implies C misses L~ (Span (C,n)) )
assume A1: n is_sufficiently_large_for C ; ::_thesis: C misses L~ (Span (C,n))
set G = Gauge (C,n);
set f = Span (C,n);
assume not C misses L~ (Span (C,n)) ; ::_thesis: contradiction
then consider c being set such that
A2: c in C and
A3: c in L~ (Span (C,n)) by XBOOLE_0:3;
L~ (Span (C,n)) = union { (LSeg ((Span (C,n)),i)) where i is Element of NAT : ( 1 <= i & i + 1 <= len (Span (C,n)) ) } by TOPREAL1:def_4;
then consider Z being set such that
A4: c in Z and
A5: Z in { (LSeg ((Span (C,n)),i)) where i is Element of NAT : ( 1 <= i & i + 1 <= len (Span (C,n)) ) } by A3, TARSKI:def_4;
consider i being Element of NAT such that
A6: Z = LSeg ((Span (C,n)),i) and
A7: 1 <= i and
A8: i + 1 <= len (Span (C,n)) by A5;
Span (C,n) is_sequence_on Gauge (C,n) by A1, JORDAN13:def_1;
then LSeg ((Span (C,n)),i) = (left_cell ((Span (C,n)),i,(Gauge (C,n)))) /\ (right_cell ((Span (C,n)),i,(Gauge (C,n)))) by A7, A8, GOBRD13:29;
then A9: c in right_cell ((Span (C,n)),i,(Gauge (C,n))) by A4, A6, XBOOLE_0:def_4;
right_cell ((Span (C,n)),i,(Gauge (C,n))) misses C by A1, A7, A8, Th7;
hence contradiction by A2, A9, XBOOLE_0:3; ::_thesis: verum
end;
registration
let C be Simple_closed_curve;
let n be Element of NAT ;
cluster Cl (RightComp (Span (C,n))) -> compact ;
coherence
Cl (RightComp (Span (C,n))) is compact by GOBRD14:32;
end;
theorem Th9: :: JORDAN14:9
for C being Simple_closed_curve
for n being Element of NAT st n is_sufficiently_large_for C holds
C meets LeftComp (Span (C,n))
proof
let C be Simple_closed_curve; ::_thesis: for n being Element of NAT st n is_sufficiently_large_for C holds
C meets LeftComp (Span (C,n))
let n be Element of NAT ; ::_thesis: ( n is_sufficiently_large_for C implies C meets LeftComp (Span (C,n)) )
assume A1: n is_sufficiently_large_for C ; ::_thesis: C meets LeftComp (Span (C,n))
then A2: Span (C,n) is_sequence_on Gauge (C,n) by JORDAN13:def_1;
A3: 1 + 1 <= len (Span (C,n)) by GOBOARD7:34, XXREAL_0:2;
then left_cell ((Span (C,n)),1,(Gauge (C,n))) meets C by A1, Th7;
then (left_cell ((Span (C,n)),1,(Gauge (C,n)))) \ (L~ (Span (C,n))) meets C by A1, Th8, XBOOLE_1:84;
hence C meets LeftComp (Span (C,n)) by A3, A2, JORDAN9:27, XBOOLE_1:63; ::_thesis: verum
end;
theorem Th10: :: JORDAN14:10
for C being Simple_closed_curve
for n being Element of NAT st n is_sufficiently_large_for C holds
C misses RightComp (Span (C,n))
proof
let C be Simple_closed_curve; ::_thesis: for n being Element of NAT st n is_sufficiently_large_for C holds
C misses RightComp (Span (C,n))
let n be Element of NAT ; ::_thesis: ( n is_sufficiently_large_for C implies C misses RightComp (Span (C,n)) )
set f = Span (C,n);
RightComp (Span (C,n)) is_a_component_of (L~ (Span (C,n))) ` by GOBOARD9:def_2;
then A1: ex L being Subset of ((TOP-REAL 2) | ((L~ (Span (C,n))) `)) st
( L = RightComp (Span (C,n)) & L is a_component ) by CONNSP_1:def_6;
LeftComp (Span (C,n)) is_a_component_of (L~ (Span (C,n))) ` by GOBOARD9:def_1;
then A2: ex R being Subset of ((TOP-REAL 2) | ((L~ (Span (C,n))) `)) st
( R = LeftComp (Span (C,n)) & R is a_component ) by CONNSP_1:def_6;
assume A3: n is_sufficiently_large_for C ; ::_thesis: C misses RightComp (Span (C,n))
then A4: C misses L~ (Span (C,n)) by Th8;
C c= the carrier of ((TOP-REAL 2) | ((L~ (Span (C,n))) `))
proof
let c be set ; :: according to TARSKI:def_3 ::_thesis: ( not c in C or c in the carrier of ((TOP-REAL 2) | ((L~ (Span (C,n))) `)) )
assume A5: c in C ; ::_thesis: c in the carrier of ((TOP-REAL 2) | ((L~ (Span (C,n))) `))
then not c in L~ (Span (C,n)) by A4, XBOOLE_0:3;
then c in (L~ (Span (C,n))) ` by A5, SUBSET_1:29;
hence c in the carrier of ((TOP-REAL 2) | ((L~ (Span (C,n))) `)) by PRE_TOPC:8; ::_thesis: verum
end;
then reconsider C1 = C as Subset of ((TOP-REAL 2) | ((L~ (Span (C,n))) `)) ;
assume A6: C meets RightComp (Span (C,n)) ; ::_thesis: contradiction
A7: C1 is connected by CONNSP_1:23;
C meets LeftComp (Span (C,n)) by A3, Th9;
hence contradiction by A6, A1, A2, A7, JORDAN2C:92, SPRECT_4:6; ::_thesis: verum
end;
theorem Th11: :: JORDAN14:11
for C being Simple_closed_curve
for n being Element of NAT st n is_sufficiently_large_for C holds
C c= LeftComp (Span (C,n))
proof
let C be Simple_closed_curve; ::_thesis: for n being Element of NAT st n is_sufficiently_large_for C holds
C c= LeftComp (Span (C,n))
let n be Element of NAT ; ::_thesis: ( n is_sufficiently_large_for C implies C c= LeftComp (Span (C,n)) )
assume A1: n is_sufficiently_large_for C ; ::_thesis: C c= LeftComp (Span (C,n))
let c be set ; :: according to TARSKI:def_3 ::_thesis: ( not c in C or c in LeftComp (Span (C,n)) )
set f = Span (C,n);
assume A2: c in C ; ::_thesis: c in LeftComp (Span (C,n))
C misses L~ (Span (C,n)) by A1, Th8;
then A3: not c in L~ (Span (C,n)) by A2, XBOOLE_0:3;
C misses RightComp (Span (C,n)) by A1, Th10;
then not c in RightComp (Span (C,n)) by A2, XBOOLE_0:3;
hence c in LeftComp (Span (C,n)) by A2, A3, GOBRD14:18; ::_thesis: verum
end;
theorem Th12: :: JORDAN14:12
for C being Simple_closed_curve
for n being Element of NAT st n is_sufficiently_large_for C holds
C c= UBD (L~ (Span (C,n)))
proof
let C be Simple_closed_curve; ::_thesis: for n being Element of NAT st n is_sufficiently_large_for C holds
C c= UBD (L~ (Span (C,n)))
let n be Element of NAT ; ::_thesis: ( n is_sufficiently_large_for C implies C c= UBD (L~ (Span (C,n))) )
assume n is_sufficiently_large_for C ; ::_thesis: C c= UBD (L~ (Span (C,n)))
then A1: C c= LeftComp (Span (C,n)) by Th11;
LeftComp (Span (C,n)) c= UBD (L~ (Span (C,n))) by GOBRD14:34, JORDAN2C:23;
hence C c= UBD (L~ (Span (C,n))) by A1, XBOOLE_1:1; ::_thesis: verum
end;
theorem Th13: :: JORDAN14:13
for C being Simple_closed_curve
for n being Element of NAT st n is_sufficiently_large_for C holds
BDD (L~ (Span (C,n))) c= BDD C
proof
let C be Simple_closed_curve; ::_thesis: for n being Element of NAT st n is_sufficiently_large_for C holds
BDD (L~ (Span (C,n))) c= BDD C
let n be Element of NAT ; ::_thesis: ( n is_sufficiently_large_for C implies BDD (L~ (Span (C,n))) c= BDD C )
assume that
A1: n is_sufficiently_large_for C and
A2: not BDD (L~ (Span (C,n))) c= BDD C ; ::_thesis: contradiction
set f = Span (C,n);
A3: Cl (BDD (L~ (Span (C,n)))) = Cl (RightComp (Span (C,n))) by GOBRD14:37
.= (RightComp (Span (C,n))) \/ (L~ (Span (C,n))) by GOBRD14:21 ;
len (Span (C,n)) >= 1 by GOBOARD7:34, XXREAL_0:2;
then A4: 1 in dom (Span (C,n)) by FINSEQ_3:25;
len (Span (C,n)) > 4 by GOBOARD7:34;
then (Span (C,n)) /. 1 in L~ (Span (C,n)) by A4, GOBOARD1:1, XXREAL_0:2;
then SpanStart (C,n) in L~ (Span (C,n)) by A1, JORDAN13:def_1;
then A5: SpanStart (C,n) in Cl (BDD (L~ (Span (C,n)))) by A3, XBOOLE_0:def_3;
SpanStart (C,n) in BDD C by A1, Th6;
then A6: BDD (L~ (Span (C,n))) meets BDD C by A5, PRE_TOPC:def_7;
BDD C misses UBD C by JORDAN2C:24;
then A7: BDD C, UBD C are_separated by TSEP_1:37;
BDD (L~ (Span (C,n))) misses UBD (L~ (Span (C,n))) by JORDAN2C:24;
then C misses BDD (L~ (Span (C,n))) by A1, Th12, XBOOLE_1:63;
then A8: BDD (L~ (Span (C,n))) c= C ` by SUBSET_1:23;
(BDD C) \/ (UBD C) = C ` by JORDAN2C:27;
then BDD (L~ (Span (C,n))) c= UBD C by A2, A8, A7, CONNSP_1:16;
then BDD C meets UBD C by A6, XBOOLE_1:63;
hence contradiction by JORDAN2C:24; ::_thesis: verum
end;
theorem Th14: :: JORDAN14:14
for C being Simple_closed_curve
for n being Element of NAT st n is_sufficiently_large_for C holds
UBD C c= UBD (L~ (Span (C,n)))
proof
let C be Simple_closed_curve; ::_thesis: for n being Element of NAT st n is_sufficiently_large_for C holds
UBD C c= UBD (L~ (Span (C,n)))
let n be Element of NAT ; ::_thesis: ( n is_sufficiently_large_for C implies UBD C c= UBD (L~ (Span (C,n))) )
assume A1: n is_sufficiently_large_for C ; ::_thesis: UBD C c= UBD (L~ (Span (C,n)))
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in UBD C or x in UBD (L~ (Span (C,n))) )
A2: BDD C misses UBD C by JORDAN2C:24;
assume A3: x in UBD C ; ::_thesis: x in UBD (L~ (Span (C,n)))
then reconsider p = x as Point of (TOP-REAL 2) ;
A4: Cl (BDD (L~ (Span (C,n)))) c= Cl (BDD C) by A1, Th13, PRE_TOPC:19;
A5: now__::_thesis:_not_x_in_L~_(Span_(C,n))
assume x in L~ (Span (C,n)) ; ::_thesis: contradiction
then p in (RightComp (Span (C,n))) \/ (L~ (Span (C,n))) by XBOOLE_0:def_3;
then p in Cl (RightComp (Span (C,n))) by GOBRD14:21;
then p in Cl (BDD (L~ (Span (C,n)))) by GOBRD14:37;
hence contradiction by A4, A2, A3, PRE_TOPC:def_7; ::_thesis: verum
end;
BDD (L~ (Span (C,n))) c= BDD C by A1, Th13;
then not x in BDD (L~ (Span (C,n))) by A2, A3, XBOOLE_0:3;
then not x in RightComp (Span (C,n)) by GOBRD14:37;
then p in LeftComp (Span (C,n)) by A5, GOBRD14:17;
hence x in UBD (L~ (Span (C,n))) by GOBRD14:36; ::_thesis: verum
end;
theorem :: JORDAN14:15
for C being Simple_closed_curve
for n being Element of NAT st n is_sufficiently_large_for C holds
RightComp (Span (C,n)) c= BDD C
proof
let C be Simple_closed_curve; ::_thesis: for n being Element of NAT st n is_sufficiently_large_for C holds
RightComp (Span (C,n)) c= BDD C
let n be Element of NAT ; ::_thesis: ( n is_sufficiently_large_for C implies RightComp (Span (C,n)) c= BDD C )
assume n is_sufficiently_large_for C ; ::_thesis: RightComp (Span (C,n)) c= BDD C
then BDD (L~ (Span (C,n))) c= BDD C by Th13;
hence RightComp (Span (C,n)) c= BDD C by GOBRD14:37; ::_thesis: verum
end;
theorem Th16: :: JORDAN14:16
for C being Simple_closed_curve
for n being Element of NAT st n is_sufficiently_large_for C holds
UBD C c= LeftComp (Span (C,n))
proof
let C be Simple_closed_curve; ::_thesis: for n being Element of NAT st n is_sufficiently_large_for C holds
UBD C c= LeftComp (Span (C,n))
let n be Element of NAT ; ::_thesis: ( n is_sufficiently_large_for C implies UBD C c= LeftComp (Span (C,n)) )
assume n is_sufficiently_large_for C ; ::_thesis: UBD C c= LeftComp (Span (C,n))
then UBD C c= UBD (L~ (Span (C,n))) by Th14;
hence UBD C c= LeftComp (Span (C,n)) by GOBRD14:36; ::_thesis: verum
end;
theorem Th17: :: JORDAN14:17
for C being Simple_closed_curve
for n being Element of NAT st n is_sufficiently_large_for C holds
UBD C misses BDD (L~ (Span (C,n)))
proof
let C be Simple_closed_curve; ::_thesis: for n being Element of NAT st n is_sufficiently_large_for C holds
UBD C misses BDD (L~ (Span (C,n)))
let n be Element of NAT ; ::_thesis: ( n is_sufficiently_large_for C implies UBD C misses BDD (L~ (Span (C,n))) )
assume that
A1: n is_sufficiently_large_for C and
A2: UBD C meets BDD (L~ (Span (C,n))) ; ::_thesis: contradiction
UBD (L~ (Span (C,n))) meets BDD (L~ (Span (C,n))) by A1, A2, Th14, XBOOLE_1:63;
hence contradiction by JORDAN2C:24; ::_thesis: verum
end;
theorem :: JORDAN14:18
for C being Simple_closed_curve
for n being Element of NAT st n is_sufficiently_large_for C holds
UBD C misses RightComp (Span (C,n))
proof
let C be Simple_closed_curve; ::_thesis: for n being Element of NAT st n is_sufficiently_large_for C holds
UBD C misses RightComp (Span (C,n))
let n be Element of NAT ; ::_thesis: ( n is_sufficiently_large_for C implies UBD C misses RightComp (Span (C,n)) )
assume n is_sufficiently_large_for C ; ::_thesis: UBD C misses RightComp (Span (C,n))
then UBD C misses BDD (L~ (Span (C,n))) by Th17;
hence UBD C misses RightComp (Span (C,n)) by GOBRD14:37; ::_thesis: verum
end;
theorem Th19: :: JORDAN14:19
for C being Simple_closed_curve
for P being Subset of (TOP-REAL 2)
for n being Element of NAT st n is_sufficiently_large_for C & P is_outside_component_of C holds
P misses L~ (Span (C,n))
proof
let C be Simple_closed_curve; ::_thesis: for P being Subset of (TOP-REAL 2)
for n being Element of NAT st n is_sufficiently_large_for C & P is_outside_component_of C holds
P misses L~ (Span (C,n))
let P be Subset of (TOP-REAL 2); ::_thesis: for n being Element of NAT st n is_sufficiently_large_for C & P is_outside_component_of C holds
P misses L~ (Span (C,n))
let n be Element of NAT ; ::_thesis: ( n is_sufficiently_large_for C & P is_outside_component_of C implies P misses L~ (Span (C,n)) )
assume that
A1: n is_sufficiently_large_for C and
A2: P is_outside_component_of C and
A3: P meets L~ (Span (C,n)) ; ::_thesis: contradiction
A4: UBD C c= LeftComp (Span (C,n)) by A1, Th16;
consider x being set such that
A5: x in P and
A6: x in L~ (Span (C,n)) by A3, XBOOLE_0:3;
P c= UBD C by A2, JORDAN2C:23;
then x in UBD C by A5;
hence contradiction by A6, A4, GOBRD14:17; ::_thesis: verum
end;
theorem Th20: :: JORDAN14:20
for C being Simple_closed_curve
for n being Element of NAT st n is_sufficiently_large_for C holds
UBD C misses L~ (Span (C,n))
proof
let C be Simple_closed_curve; ::_thesis: for n being Element of NAT st n is_sufficiently_large_for C holds
UBD C misses L~ (Span (C,n))
let n be Element of NAT ; ::_thesis: ( n is_sufficiently_large_for C implies UBD C misses L~ (Span (C,n)) )
assume A1: n is_sufficiently_large_for C ; ::_thesis: UBD C misses L~ (Span (C,n))
assume UBD C meets L~ (Span (C,n)) ; ::_thesis: contradiction
then consider x being set such that
A2: x in UBD C and
A3: x in L~ (Span (C,n)) by XBOOLE_0:3;
UBD C = union { B where B is Subset of (TOP-REAL 2) : B is_outside_component_of C } by JORDAN2C:def_5;
then consider Z being set such that
A4: x in Z and
A5: Z in { B where B is Subset of (TOP-REAL 2) : B is_outside_component_of C } by A2, TARSKI:def_4;
consider B being Subset of (TOP-REAL 2) such that
A6: Z = B and
A7: B is_outside_component_of C by A5;
B misses L~ (Span (C,n)) by A1, A7, Th19;
hence contradiction by A3, A4, A6, XBOOLE_0:3; ::_thesis: verum
end;
theorem Th21: :: JORDAN14:21
for C being Simple_closed_curve
for n being Element of NAT st n is_sufficiently_large_for C holds
L~ (Span (C,n)) c= BDD C
proof
let C be Simple_closed_curve; ::_thesis: for n being Element of NAT st n is_sufficiently_large_for C holds
L~ (Span (C,n)) c= BDD C
let n be Element of NAT ; ::_thesis: ( n is_sufficiently_large_for C implies L~ (Span (C,n)) c= BDD C )
assume A1: n is_sufficiently_large_for C ; ::_thesis: L~ (Span (C,n)) c= BDD C
then C misses L~ (Span (C,n)) by Th8;
then L~ (Span (C,n)) c= C ` by SUBSET_1:23;
then A2: L~ (Span (C,n)) c= (BDD C) \/ (UBD C) by JORDAN2C:27;
UBD C misses L~ (Span (C,n)) by A1, Th20;
hence L~ (Span (C,n)) c= BDD C by A2, XBOOLE_1:73; ::_thesis: verum
end;
theorem Th22: :: JORDAN14:22
for C being Simple_closed_curve
for i, j, k, n being Element of NAT st n is_sufficiently_large_for C & 1 <= k & k <= len (Span (C,n)) & [i,j] in Indices (Gauge (C,n)) & (Span (C,n)) /. k = (Gauge (C,n)) * (i,j) holds
i > 1
proof
let C be Simple_closed_curve; ::_thesis: for i, j, k, n being Element of NAT st n is_sufficiently_large_for C & 1 <= k & k <= len (Span (C,n)) & [i,j] in Indices (Gauge (C,n)) & (Span (C,n)) /. k = (Gauge (C,n)) * (i,j) holds
i > 1
let i, j, k, n be Element of NAT ; ::_thesis: ( n is_sufficiently_large_for C & 1 <= k & k <= len (Span (C,n)) & [i,j] in Indices (Gauge (C,n)) & (Span (C,n)) /. k = (Gauge (C,n)) * (i,j) implies i > 1 )
assume that
A1: n is_sufficiently_large_for C and
A2: 1 <= k and
A3: k <= len (Span (C,n)) and
A4: [i,j] in Indices (Gauge (C,n)) and
A5: (Span (C,n)) /. k = (Gauge (C,n)) * (i,j) ; ::_thesis: i > 1
A6: len (Span (C,n)) > 4 by GOBOARD7:34;
SpanStart (C,n) in BDD C by A1, Th6;
then A7: W-bound C <= W-bound (BDD C) by JORDAN1C:6;
A8: j <= width (Gauge (C,n)) by A4, MATRIX_1:38;
k in dom (Span (C,n)) by A2, A3, FINSEQ_3:25;
then (Span (C,n)) /. k in L~ (Span (C,n)) by A6, GOBOARD1:1, XXREAL_0:2;
then A9: W-bound (L~ (Span (C,n))) <= ((Gauge (C,n)) * (i,j)) `1 by A5, PSCOMP_1:24;
A10: BDD C c= Cl (BDD C) by PRE_TOPC:18;
A11: BDD C is bounded by JORDAN2C:106;
then A12: Cl (BDD C) is compact by TOPREAL6:79;
SpanStart (C,n) in BDD C by A1, Th6;
then A13: W-bound (BDD C) = W-bound (Cl (BDD C)) by A11, TOPREAL6:85;
L~ (Span (C,n)) c= BDD C by A1, Th21;
then W-bound (L~ (Span (C,n))) >= W-bound (Cl (BDD C)) by A12, A10, PSCOMP_1:69, XBOOLE_1:1;
then A14: W-bound (BDD C) <= ((Gauge (C,n)) * (i,j)) `1 by A13, A9, XXREAL_0:2;
len (Gauge (C,n)) >= 4 by JORDAN8:10;
then A15: len (Gauge (C,n)) >= 2 by XXREAL_0:2;
A16: 1 <= i by A4, MATRIX_1:38;
A17: 1 <= j by A4, MATRIX_1:38;
len (Gauge (C,n)) = width (Gauge (C,n)) by JORDAN8:def_1;
then ((Gauge (C,n)) * (2,j)) `1 = W-bound C by A17, A8, JORDAN8:11;
then ((Gauge (C,n)) * (2,j)) `1 <= ((Gauge (C,n)) * (i,j)) `1 by A7, A14, XXREAL_0:2;
then i >= 1 + 1 by A16, A17, A8, A15, GOBOARD5:3;
hence i > 1 by NAT_1:13; ::_thesis: verum
end;
theorem Th23: :: JORDAN14:23
for C being Simple_closed_curve
for i, j, k, n being Element of NAT st n is_sufficiently_large_for C & 1 <= k & k <= len (Span (C,n)) & [i,j] in Indices (Gauge (C,n)) & (Span (C,n)) /. k = (Gauge (C,n)) * (i,j) holds
i < len (Gauge (C,n))
proof
let C be Simple_closed_curve; ::_thesis: for i, j, k, n being Element of NAT st n is_sufficiently_large_for C & 1 <= k & k <= len (Span (C,n)) & [i,j] in Indices (Gauge (C,n)) & (Span (C,n)) /. k = (Gauge (C,n)) * (i,j) holds
i < len (Gauge (C,n))
let i, j, k, n be Element of NAT ; ::_thesis: ( n is_sufficiently_large_for C & 1 <= k & k <= len (Span (C,n)) & [i,j] in Indices (Gauge (C,n)) & (Span (C,n)) /. k = (Gauge (C,n)) * (i,j) implies i < len (Gauge (C,n)) )
assume that
A1: n is_sufficiently_large_for C and
A2: 1 <= k and
A3: k <= len (Span (C,n)) and
A4: [i,j] in Indices (Gauge (C,n)) and
A5: (Span (C,n)) /. k = (Gauge (C,n)) * (i,j) ; ::_thesis: i < len (Gauge (C,n))
A6: len (Span (C,n)) > 4 by GOBOARD7:34;
SpanStart (C,n) in BDD C by A1, Th6;
then A7: E-bound C >= E-bound (BDD C) by JORDAN1C:7;
A8: 1 <= j by A4, MATRIX_1:38;
k in dom (Span (C,n)) by A2, A3, FINSEQ_3:25;
then (Span (C,n)) /. k in L~ (Span (C,n)) by A6, GOBOARD1:1, XXREAL_0:2;
then A9: E-bound (L~ (Span (C,n))) >= ((Gauge (C,n)) * (i,j)) `1 by A5, PSCOMP_1:24;
A10: BDD C c= Cl (BDD C) by PRE_TOPC:18;
A11: BDD C is bounded by JORDAN2C:106;
then A12: Cl (BDD C) is compact by TOPREAL6:79;
SpanStart (C,n) in BDD C by A1, Th6;
then A13: E-bound (BDD C) = E-bound (Cl (BDD C)) by A11, TOPREAL6:86;
L~ (Span (C,n)) c= BDD C by A1, Th21;
then E-bound (L~ (Span (C,n))) <= E-bound (Cl (BDD C)) by A12, A10, PSCOMP_1:67, XBOOLE_1:1;
then A14: E-bound (BDD C) >= ((Gauge (C,n)) * (i,j)) `1 by A13, A9, XXREAL_0:2;
A15: len (Gauge (C,n)) >= 4 by JORDAN8:10;
then len (Gauge (C,n)) >= 1 + 1 by XXREAL_0:2;
then A16: (len (Gauge (C,n))) - 1 >= 1 by XREAL_1:19;
len (Gauge (C,n)) >= 0 + 1 by A15, XXREAL_0:2;
then (len (Gauge (C,n))) - 1 >= 0 by XREAL_1:19;
then A17: (len (Gauge (C,n))) -' 1 >= 1 by A16, XREAL_0:def_2;
A18: j <= width (Gauge (C,n)) by A4, MATRIX_1:38;
len (Gauge (C,n)) = width (Gauge (C,n)) by JORDAN8:def_1;
then ((Gauge (C,n)) * (((len (Gauge (C,n))) -' 1),j)) `1 = E-bound C by A8, A18, JORDAN8:12;
then A19: ((Gauge (C,n)) * (((len (Gauge (C,n))) -' 1),j)) `1 >= ((Gauge (C,n)) * (i,j)) `1 by A7, A14, XXREAL_0:2;
i <= len (Gauge (C,n)) by A4, MATRIX_1:38;
then i <= (len (Gauge (C,n))) -' 1 by A8, A18, A17, A19, GOBOARD5:3;
then i < ((len (Gauge (C,n))) -' 1) + 1 by NAT_1:13;
hence i < len (Gauge (C,n)) by A15, XREAL_1:235, XXREAL_0:2; ::_thesis: verum
end;
theorem Th24: :: JORDAN14:24
for C being Simple_closed_curve
for i, j, k, n being Element of NAT st n is_sufficiently_large_for C & 1 <= k & k <= len (Span (C,n)) & [i,j] in Indices (Gauge (C,n)) & (Span (C,n)) /. k = (Gauge (C,n)) * (i,j) holds
j > 1
proof
let C be Simple_closed_curve; ::_thesis: for i, j, k, n being Element of NAT st n is_sufficiently_large_for C & 1 <= k & k <= len (Span (C,n)) & [i,j] in Indices (Gauge (C,n)) & (Span (C,n)) /. k = (Gauge (C,n)) * (i,j) holds
j > 1
let i, j, k, n be Element of NAT ; ::_thesis: ( n is_sufficiently_large_for C & 1 <= k & k <= len (Span (C,n)) & [i,j] in Indices (Gauge (C,n)) & (Span (C,n)) /. k = (Gauge (C,n)) * (i,j) implies j > 1 )
assume that
A1: n is_sufficiently_large_for C and
A2: 1 <= k and
A3: k <= len (Span (C,n)) and
A4: [i,j] in Indices (Gauge (C,n)) and
A5: (Span (C,n)) /. k = (Gauge (C,n)) * (i,j) ; ::_thesis: j > 1
A6: len (Span (C,n)) > 4 by GOBOARD7:34;
SpanStart (C,n) in BDD C by A1, Th6;
then A7: S-bound C <= S-bound (BDD C) by JORDAN1C:8;
A8: i <= len (Gauge (C,n)) by A4, MATRIX_1:38;
k in dom (Span (C,n)) by A2, A3, FINSEQ_3:25;
then (Span (C,n)) /. k in L~ (Span (C,n)) by A6, GOBOARD1:1, XXREAL_0:2;
then A9: S-bound (L~ (Span (C,n))) <= ((Gauge (C,n)) * (i,j)) `2 by A5, PSCOMP_1:24;
A10: BDD C c= Cl (BDD C) by PRE_TOPC:18;
A11: BDD C is bounded by JORDAN2C:106;
then A12: Cl (BDD C) is compact by TOPREAL6:79;
SpanStart (C,n) in BDD C by A1, Th6;
then A13: S-bound (BDD C) = S-bound (Cl (BDD C)) by A11, TOPREAL6:88;
L~ (Span (C,n)) c= BDD C by A1, Th21;
then S-bound (L~ (Span (C,n))) >= S-bound (Cl (BDD C)) by A12, A10, PSCOMP_1:68, XBOOLE_1:1;
then A14: S-bound (BDD C) <= ((Gauge (C,n)) * (i,j)) `2 by A13, A9, XXREAL_0:2;
len (Gauge (C,n)) >= 4 by JORDAN8:10;
then A15: len (Gauge (C,n)) >= 2 by XXREAL_0:2;
A16: len (Gauge (C,n)) = width (Gauge (C,n)) by JORDAN8:def_1;
A17: 1 <= i by A4, MATRIX_1:38;
then ((Gauge (C,n)) * (i,2)) `2 = S-bound C by A8, JORDAN8:13;
then A18: ((Gauge (C,n)) * (i,2)) `2 <= ((Gauge (C,n)) * (i,j)) `2 by A7, A14, XXREAL_0:2;
1 <= j by A4, MATRIX_1:38;
then j >= 1 + 1 by A17, A8, A16, A15, A18, GOBOARD5:4;
hence j > 1 by NAT_1:13; ::_thesis: verum
end;
theorem Th25: :: JORDAN14:25
for C being Simple_closed_curve
for i, j, k, n being Element of NAT st n is_sufficiently_large_for C & 1 <= k & k <= len (Span (C,n)) & [i,j] in Indices (Gauge (C,n)) & (Span (C,n)) /. k = (Gauge (C,n)) * (i,j) holds
j < width (Gauge (C,n))
proof
let C be Simple_closed_curve; ::_thesis: for i, j, k, n being Element of NAT st n is_sufficiently_large_for C & 1 <= k & k <= len (Span (C,n)) & [i,j] in Indices (Gauge (C,n)) & (Span (C,n)) /. k = (Gauge (C,n)) * (i,j) holds
j < width (Gauge (C,n))
let i, j, k, n be Element of NAT ; ::_thesis: ( n is_sufficiently_large_for C & 1 <= k & k <= len (Span (C,n)) & [i,j] in Indices (Gauge (C,n)) & (Span (C,n)) /. k = (Gauge (C,n)) * (i,j) implies j < width (Gauge (C,n)) )
assume that
A1: n is_sufficiently_large_for C and
A2: 1 <= k and
A3: k <= len (Span (C,n)) and
A4: [i,j] in Indices (Gauge (C,n)) and
A5: (Span (C,n)) /. k = (Gauge (C,n)) * (i,j) ; ::_thesis: j < width (Gauge (C,n))
A6: len (Span (C,n)) > 4 by GOBOARD7:34;
k in dom (Span (C,n)) by A2, A3, FINSEQ_3:25;
then (Span (C,n)) /. k in L~ (Span (C,n)) by A6, GOBOARD1:1, XXREAL_0:2;
then A7: N-bound (L~ (Span (C,n))) >= ((Gauge (C,n)) * (i,j)) `2 by A5, PSCOMP_1:24;
A8: BDD C c= Cl (BDD C) by PRE_TOPC:18;
A9: BDD C is bounded by JORDAN2C:106;
then A10: Cl (BDD C) is compact by TOPREAL6:79;
SpanStart (C,n) in BDD C by A1, Th6;
then A11: N-bound (BDD C) = N-bound (Cl (BDD C)) by A9, TOPREAL6:87;
L~ (Span (C,n)) c= BDD C by A1, Th21;
then N-bound (L~ (Span (C,n))) <= N-bound (Cl (BDD C)) by A10, A8, PSCOMP_1:66, XBOOLE_1:1;
then A12: N-bound (BDD C) >= ((Gauge (C,n)) * (i,j)) `2 by A11, A7, XXREAL_0:2;
A13: len (Gauge (C,n)) = width (Gauge (C,n)) by JORDAN8:def_1;
A14: len (Gauge (C,n)) >= 4 by JORDAN8:10;
then len (Gauge (C,n)) >= 1 + 1 by XXREAL_0:2;
then A15: (len (Gauge (C,n))) - 1 >= 1 by XREAL_1:19;
SpanStart (C,n) in BDD C by A1, Th6;
then A16: N-bound C >= N-bound (BDD C) by JORDAN1C:9;
A17: i <= len (Gauge (C,n)) by A4, MATRIX_1:38;
A18: 1 <= i by A4, MATRIX_1:38;
then ((Gauge (C,n)) * (i,((len (Gauge (C,n))) -' 1))) `2 = N-bound C by A17, JORDAN8:14;
then A19: ((Gauge (C,n)) * (i,((len (Gauge (C,n))) -' 1))) `2 >= ((Gauge (C,n)) * (i,j)) `2 by A16, A12, XXREAL_0:2;
len (Gauge (C,n)) >= 0 + 1 by A14, XXREAL_0:2;
then (len (Gauge (C,n))) - 1 >= 0 by XREAL_1:19;
then A20: (len (Gauge (C,n))) -' 1 >= 1 by A15, XREAL_0:def_2;
j <= width (Gauge (C,n)) by A4, MATRIX_1:38;
then j <= (len (Gauge (C,n))) -' 1 by A18, A17, A20, A19, GOBOARD5:4;
then j < ((len (Gauge (C,n))) -' 1) + 1 by NAT_1:13;
hence j < width (Gauge (C,n)) by A13, A14, XREAL_1:235, XXREAL_0:2; ::_thesis: verum
end;
theorem :: JORDAN14:26
for C being Simple_closed_curve
for n being Element of NAT st n is_sufficiently_large_for C holds
Y-SpanStart (C,n) < width (Gauge (C,n))
proof
let C be Simple_closed_curve; ::_thesis: for n being Element of NAT st n is_sufficiently_large_for C holds
Y-SpanStart (C,n) < width (Gauge (C,n))
let n be Element of NAT ; ::_thesis: ( n is_sufficiently_large_for C implies Y-SpanStart (C,n) < width (Gauge (C,n)) )
A1: len (Span (C,n)) > 1 by GOBOARD7:34, XXREAL_0:2;
assume A2: n is_sufficiently_large_for C ; ::_thesis: Y-SpanStart (C,n) < width (Gauge (C,n))
then A3: (Span (C,n)) /. 1 = (Gauge (C,n)) * ((X-SpanStart (C,n)),(Y-SpanStart (C,n))) by JORDAN13:def_1;
[(X-SpanStart (C,n)),(Y-SpanStart (C,n))] in Indices (Gauge (C,n)) by A2, JORDAN11:8;
hence Y-SpanStart (C,n) < width (Gauge (C,n)) by A2, A1, A3, Th25; ::_thesis: verum
end;
theorem Th27: :: JORDAN14:27
for C being compact non horizontal non vertical Subset of (TOP-REAL 2)
for n, m being Element of NAT st m >= n & n >= 1 holds
X-SpanStart (C,m) = ((2 |^ (m -' n)) * ((X-SpanStart (C,n)) - 2)) + 2
proof
let C be compact non horizontal non vertical Subset of (TOP-REAL 2); ::_thesis: for n, m being Element of NAT st m >= n & n >= 1 holds
X-SpanStart (C,m) = ((2 |^ (m -' n)) * ((X-SpanStart (C,n)) - 2)) + 2
let n, m be Element of NAT ; ::_thesis: ( m >= n & n >= 1 implies X-SpanStart (C,m) = ((2 |^ (m -' n)) * ((X-SpanStart (C,n)) - 2)) + 2 )
A1: X-SpanStart (C,n) = (2 |^ (n -' 1)) + 2 by JORDAN1H:def_2;
assume A2: m >= n ; ::_thesis: ( not n >= 1 or X-SpanStart (C,m) = ((2 |^ (m -' n)) * ((X-SpanStart (C,n)) - 2)) + 2 )
assume A3: n >= 1 ; ::_thesis: X-SpanStart (C,m) = ((2 |^ (m -' n)) * ((X-SpanStart (C,n)) - 2)) + 2
then (m -' n) + (n -' 1) = (m -' n) + (n - 1) by XREAL_1:233
.= ((m -' n) + n) - 1
.= m - 1 by A2, XREAL_1:235
.= m -' 1 by A2, A3, XREAL_1:233, XXREAL_0:2 ;
then 2 |^ (m -' 1) = (2 |^ (m -' n)) * ((X-SpanStart (C,n)) - 2) by A1, NEWTON:8;
hence X-SpanStart (C,m) = ((2 |^ (m -' n)) * ((X-SpanStart (C,n)) - 2)) + 2 by JORDAN1H:def_2; ::_thesis: verum
end;
theorem Th28: :: JORDAN14:28
for C being compact non horizontal non vertical Subset of (TOP-REAL 2)
for n, m being Element of NAT st n <= m & n is_sufficiently_large_for C holds
m is_sufficiently_large_for C
proof
let C be compact non horizontal non vertical Subset of (TOP-REAL 2); ::_thesis: for n, m being Element of NAT st n <= m & n is_sufficiently_large_for C holds
m is_sufficiently_large_for C
let n, m be Element of NAT ; ::_thesis: ( n <= m & n is_sufficiently_large_for C implies m is_sufficiently_large_for C )
assume that
A1: n <= m and
A2: n is_sufficiently_large_for C ; ::_thesis: m is_sufficiently_large_for C
consider j being Element of NAT such that
A3: j < width (Gauge (C,n)) and
A4: cell ((Gauge (C,n)),((X-SpanStart (C,n)) -' 1),j) c= BDD C by A2, JORDAN1H:def_3;
set iin = X-SpanStart (C,n);
set iim = X-SpanStart (C,m);
n >= 1 by A2, JORDAN1H:51;
then A5: X-SpanStart (C,m) = ((2 |^ (m -' n)) * ((X-SpanStart (C,n)) - 2)) + 2 by A1, Th27;
A6: j > 1
proof
A7: (X-SpanStart (C,n)) -' 1 <= len (Gauge (C,n)) by JORDAN1H:50;
assume A8: j <= 1 ; ::_thesis: contradiction
percases ( j = 0 or j = 1 ) by A8, NAT_1:25;
supposeA9: j = 0 ; ::_thesis: contradiction
width (Gauge (C,n)) >= 0 by NAT_1:2;
then A10: not cell ((Gauge (C,n)),((X-SpanStart (C,n)) -' 1),0) is empty by A7, JORDAN1A:24;
cell ((Gauge (C,n)),((X-SpanStart (C,n)) -' 1),0) c= UBD C by A7, JORDAN1A:49;
hence contradiction by A4, A9, A10, JORDAN2C:24, XBOOLE_1:68; ::_thesis: verum
end;
supposeA11: j = 1 ; ::_thesis: contradiction
set i1 = X-SpanStart (C,n);
A12: (X-SpanStart (C,n)) -' 1 <= X-SpanStart (C,n) by NAT_D:44;
X-SpanStart (C,n) < len (Gauge (C,n)) by JORDAN1H:49;
then A13: (X-SpanStart (C,n)) -' 1 < len (Gauge (C,n)) by A12, XXREAL_0:2;
BDD C c= C ` by JORDAN2C:25;
then A14: cell ((Gauge (C,n)),((X-SpanStart (C,n)) -' 1),1) c= C ` by A4, A11, XBOOLE_1:1;
UBD C is_outside_component_of C by JORDAN2C:68;
then A15: UBD C is_a_component_of C ` by JORDAN2C:def_3;
width (Gauge (C,n)) <> 0 by GOBOARD1:def_3;
then A16: 0 + 1 <= width (Gauge (C,n)) by NAT_1:14;
then A17: not cell ((Gauge (C,n)),((X-SpanStart (C,n)) -' 1),1) is empty by A7, JORDAN1A:24;
A18: 1 <= (X-SpanStart (C,n)) -' 1 by JORDAN1H:50;
0 < width (Gauge (C,n)) by A16, NAT_1:13;
then (cell ((Gauge (C,n)),((X-SpanStart (C,n)) -' 1),0)) /\ (cell ((Gauge (C,n)),((X-SpanStart (C,n)) -' 1),(0 + 1))) = LSeg (((Gauge (C,n)) * (((X-SpanStart (C,n)) -' 1),(0 + 1))),((Gauge (C,n)) * ((((X-SpanStart (C,n)) -' 1) + 1),(0 + 1)))) by A13, A18, GOBOARD5:26;
then A19: cell ((Gauge (C,n)),((X-SpanStart (C,n)) -' 1),0) meets cell ((Gauge (C,n)),((X-SpanStart (C,n)) -' 1),(0 + 1)) by XBOOLE_0:def_7;
cell ((Gauge (C,n)),((X-SpanStart (C,n)) -' 1),0) c= UBD C by A7, JORDAN1A:49;
then cell ((Gauge (C,n)),((X-SpanStart (C,n)) -' 1),1) c= UBD C by A16, A13, A19, A15, A14, GOBOARD9:4, JORDAN1A:25;
hence contradiction by A4, A11, A17, JORDAN2C:24, XBOOLE_1:68; ::_thesis: verum
end;
end;
end;
then ((2 |^ (m -' n)) * (j - 2)) + 2 > 1 by A1, A3, JORDAN1A:32;
then reconsider j1 = ((2 |^ (m -' n)) * (j - 2)) + 2 as Element of NAT by INT_1:3, XXREAL_0:2;
X-SpanStart (C,n) > 2 by JORDAN1H:49;
then A20: X-SpanStart (C,n) >= 2 + 1 by NAT_1:13;
A21: j + 1 < width (Gauge (C,n))
proof
assume j + 1 >= width (Gauge (C,n)) ; ::_thesis: contradiction
then A22: ( j + 1 > width (Gauge (C,n)) or j + 1 = width (Gauge (C,n)) ) by XXREAL_0:1;
A23: (X-SpanStart (C,n)) -' 1 <= len (Gauge (C,n)) by JORDAN1H:50;
percases ( j = width (Gauge (C,n)) or j + 1 = width (Gauge (C,n)) ) by A3, A22, NAT_1:13;
supposeA24: j = width (Gauge (C,n)) ; ::_thesis: contradiction
A25: cell ((Gauge (C,n)),((X-SpanStart (C,n)) -' 1),(width (Gauge (C,n)))) c= UBD C by A23, JORDAN1A:50;
not cell ((Gauge (C,n)),((X-SpanStart (C,n)) -' 1),j) is empty by A23, A24, JORDAN1A:24;
hence contradiction by A4, A24, A25, JORDAN2C:24, XBOOLE_1:68; ::_thesis: verum
end;
suppose j + 1 = width (Gauge (C,n)) ; ::_thesis: contradiction
then A26: cell ((Gauge (C,n)),((X-SpanStart (C,n)) -' 1),((width (Gauge (C,n))) -' 1)) c= BDD C by A4, NAT_D:34;
BDD C c= C ` by JORDAN2C:25;
then A27: cell ((Gauge (C,n)),((X-SpanStart (C,n)) -' 1),((width (Gauge (C,n))) -' 1)) c= C ` by A26, XBOOLE_1:1;
A28: cell ((Gauge (C,n)),((X-SpanStart (C,n)) -' 1),(width (Gauge (C,n)))) c= UBD C by A23, JORDAN1A:50;
set i1 = X-SpanStart (C,n);
A29: (X-SpanStart (C,n)) -' 1 <= X-SpanStart (C,n) by NAT_D:44;
X-SpanStart (C,n) < len (Gauge (C,n)) by JORDAN1H:49;
then A30: (X-SpanStart (C,n)) -' 1 < len (Gauge (C,n)) by A29, XXREAL_0:2;
UBD C is_outside_component_of C by JORDAN2C:68;
then A31: UBD C is_a_component_of C ` by JORDAN2C:def_3;
(width (Gauge (C,n))) -' 1 <= width (Gauge (C,n)) by NAT_D:44;
then A32: not cell ((Gauge (C,n)),((X-SpanStart (C,n)) -' 1),((width (Gauge (C,n))) -' 1)) is empty by A23, JORDAN1A:24;
A33: (width (Gauge (C,n))) - 1 < width (Gauge (C,n)) by XREAL_1:146;
A34: 1 <= (X-SpanStart (C,n)) -' 1 by JORDAN1H:50;
A35: width (Gauge (C,n)) <> 0 by GOBOARD1:def_3;
then ((width (Gauge (C,n))) -' 1) + 1 = width (Gauge (C,n)) by NAT_1:14, XREAL_1:235;
then (cell ((Gauge (C,n)),((X-SpanStart (C,n)) -' 1),(width (Gauge (C,n))))) /\ (cell ((Gauge (C,n)),((X-SpanStart (C,n)) -' 1),((width (Gauge (C,n))) -' 1))) = LSeg (((Gauge (C,n)) * (((X-SpanStart (C,n)) -' 1),(width (Gauge (C,n))))),((Gauge (C,n)) * ((((X-SpanStart (C,n)) -' 1) + 1),(width (Gauge (C,n)))))) by A30, A33, A34, GOBOARD5:26;
then A36: cell ((Gauge (C,n)),((X-SpanStart (C,n)) -' 1),(width (Gauge (C,n)))) meets cell ((Gauge (C,n)),((X-SpanStart (C,n)) -' 1),((width (Gauge (C,n))) -' 1)) by XBOOLE_0:def_7;
(width (Gauge (C,n))) -' 1 < width (Gauge (C,n)) by A35, A33, NAT_1:14, XREAL_1:233;
then cell ((Gauge (C,n)),((X-SpanStart (C,n)) -' 1),((width (Gauge (C,n))) -' 1)) c= UBD C by A28, A30, A36, A31, A27, GOBOARD9:4, JORDAN1A:25;
hence contradiction by A26, A32, JORDAN2C:24, XBOOLE_1:68; ::_thesis: verum
end;
end;
end;
X-SpanStart (C,n) < len (Gauge (C,n)) by JORDAN1H:49;
then cell ((Gauge (C,m)),((X-SpanStart (C,m)) -' 1),j1) c= cell ((Gauge (C,n)),((X-SpanStart (C,n)) -' 1),j) by A1, A5, A20, A6, A21, JORDAN1A:48;
then A37: cell ((Gauge (C,m)),((X-SpanStart (C,m)) -' 1),j1) c= BDD C by A4, XBOOLE_1:1;
j1 < width (Gauge (C,m)) by A1, A3, A6, JORDAN1A:32;
hence m is_sufficiently_large_for C by A37, JORDAN1H:def_3; ::_thesis: verum
end;
theorem Th29: :: JORDAN14:29
for G being Go-board
for f being FinSequence of (TOP-REAL 2)
for i, j being Element of NAT st f is_sequence_on G & f is special & i <= len G & j <= width G holds
(cell (G,i,j)) \ (L~ f) is connected
proof
let G be Go-board; ::_thesis: for f being FinSequence of (TOP-REAL 2)
for i, j being Element of NAT st f is_sequence_on G & f is special & i <= len G & j <= width G holds
(cell (G,i,j)) \ (L~ f) is connected
let f be FinSequence of (TOP-REAL 2); ::_thesis: for i, j being Element of NAT st f is_sequence_on G & f is special & i <= len G & j <= width G holds
(cell (G,i,j)) \ (L~ f) is connected
let i, j be Element of NAT ; ::_thesis: ( f is_sequence_on G & f is special & i <= len G & j <= width G implies (cell (G,i,j)) \ (L~ f) is connected )
assume that
A1: f is_sequence_on G and
A2: f is special and
A3: i <= len G and
A4: j <= width G ; ::_thesis: (cell (G,i,j)) \ (L~ f) is connected
Int (cell (G,i,j)) misses L~ f by A1, A2, A3, A4, JORDAN9:14;
then A5: Int (cell (G,i,j)) c= (L~ f) ` by SUBSET_1:23;
(cell (G,i,j)) \ (L~ f) c= cell (G,i,j) by XBOOLE_1:36;
then A6: (cell (G,i,j)) \ (L~ f) c= Cl (Int (cell (G,i,j))) by A3, A4, GOBRD11:35;
A7: Int (cell (G,i,j)) c= cell (G,i,j) by TOPS_1:16;
A8: Int (cell (G,i,j)) is convex by A3, A4, GOBOARD9:17;
(cell (G,i,j)) \ (L~ f) = (cell (G,i,j)) /\ ((L~ f) `) by SUBSET_1:13;
then Int (cell (G,i,j)) c= (cell (G,i,j)) \ (L~ f) by A5, A7, XBOOLE_1:19;
hence (cell (G,i,j)) \ (L~ f) is connected by A6, A8, CONNSP_1:18; ::_thesis: verum
end;
theorem Th30: :: JORDAN14:30
for C being Simple_closed_curve
for n, k being Element of NAT st n is_sufficiently_large_for C & Y-SpanStart (C,n) <= k & k <= ((2 |^ (n -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2 holds
(cell ((Gauge (C,n)),((X-SpanStart (C,n)) -' 1),k)) \ (L~ (Span (C,n))) c= BDD (L~ (Span (C,n)))
proof
let C be Simple_closed_curve; ::_thesis: for n, k being Element of NAT st n is_sufficiently_large_for C & Y-SpanStart (C,n) <= k & k <= ((2 |^ (n -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2 holds
(cell ((Gauge (C,n)),((X-SpanStart (C,n)) -' 1),k)) \ (L~ (Span (C,n))) c= BDD (L~ (Span (C,n)))
let n, k be Element of NAT ; ::_thesis: ( n is_sufficiently_large_for C & Y-SpanStart (C,n) <= k & k <= ((2 |^ (n -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2 implies (cell ((Gauge (C,n)),((X-SpanStart (C,n)) -' 1),k)) \ (L~ (Span (C,n))) c= BDD (L~ (Span (C,n))) )
set G = Gauge (C,n);
set f = Span (C,n);
set AI = ApproxIndex C;
set YI = Y-InitStart C;
set XS = X-SpanStart (C,n);
set YS = Y-SpanStart (C,n);
assume that
A1: n is_sufficiently_large_for C and
A2: Y-SpanStart (C,n) <= k and
A3: k <= ((2 |^ (n -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2 ; ::_thesis: (cell ((Gauge (C,n)),((X-SpanStart (C,n)) -' 1),k)) \ (L~ (Span (C,n))) c= BDD (L~ (Span (C,n)))
A4: Span (C,n) is_sequence_on Gauge (C,n) by A1, JORDAN13:def_1;
reconsider ro = k - (Y-SpanStart (C,n)) as Element of NAT by A2, INT_1:5;
A5: ro <= (((2 |^ (n -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2) - (Y-SpanStart (C,n)) by A3, XREAL_1:9;
A6: k = (Y-SpanStart (C,n)) + ro ;
defpred S1[ Element of NAT ] means ( $1 <= (((2 |^ (n -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2) - (Y-SpanStart (C,n)) implies (cell ((Gauge (C,n)),((X-SpanStart (C,n)) -' 1),((Y-SpanStart (C,n)) + $1))) \ (L~ (Span (C,n))) c= BDD (L~ (Span (C,n))) );
A7: 1 <= (X-SpanStart (C,n)) -' 1 by JORDAN1H:50;
X-SpanStart (C,n) > 2 by JORDAN1H:49;
then A8: ((X-SpanStart (C,n)) -' 1) + 1 = X-SpanStart (C,n) by XREAL_1:235, XXREAL_0:2;
A9: (X-SpanStart (C,n)) -' 1 < len (Gauge (C,n)) by JORDAN1H:50;
A10: for t being Element of NAT st S1[t] holds
S1[t + 1]
proof
let t be Element of NAT ; ::_thesis: ( S1[t] implies S1[t + 1] )
assume A11: ( t <= (((2 |^ (n -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2) - (Y-SpanStart (C,n)) implies (cell ((Gauge (C,n)),((X-SpanStart (C,n)) -' 1),((Y-SpanStart (C,n)) + t))) \ (L~ (Span (C,n))) c= BDD (L~ (Span (C,n))) ) ; ::_thesis: S1[t + 1]
set Ls = LSeg (((Gauge (C,n)) * (((X-SpanStart (C,n)) -' 1),((Y-SpanStart (C,n)) + (t + 1)))),((Gauge (C,n)) * ((X-SpanStart (C,n)),((Y-SpanStart (C,n)) + (t + 1)))));
A12: t < t + 1 by NAT_1:13;
set p = (1 / 2) * (((Gauge (C,n)) * (((X-SpanStart (C,n)) -' 1),((Y-SpanStart (C,n)) + (t + 1)))) + ((Gauge (C,n)) * ((X-SpanStart (C,n)),((Y-SpanStart (C,n)) + (t + 1)))));
A13: (cell ((Gauge (C,n)),((X-SpanStart (C,n)) -' 1),((Y-SpanStart (C,n)) + (t + 1)))) \ (L~ (Span (C,n))) c= (L~ (Span (C,n))) `
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in (cell ((Gauge (C,n)),((X-SpanStart (C,n)) -' 1),((Y-SpanStart (C,n)) + (t + 1)))) \ (L~ (Span (C,n))) or y in (L~ (Span (C,n))) ` )
assume A14: y in (cell ((Gauge (C,n)),((X-SpanStart (C,n)) -' 1),((Y-SpanStart (C,n)) + (t + 1)))) \ (L~ (Span (C,n))) ; ::_thesis: y in (L~ (Span (C,n))) `
then not y in L~ (Span (C,n)) by XBOOLE_0:def_5;
hence y in (L~ (Span (C,n))) ` by A14, SUBSET_1:29; ::_thesis: verum
end;
A15: (1 / 2) * (((Gauge (C,n)) * (((X-SpanStart (C,n)) -' 1),((Y-SpanStart (C,n)) + (t + 1)))) + ((Gauge (C,n)) * ((X-SpanStart (C,n)),((Y-SpanStart (C,n)) + (t + 1))))) in LSeg (((Gauge (C,n)) * (((X-SpanStart (C,n)) -' 1),((Y-SpanStart (C,n)) + (t + 1)))),((Gauge (C,n)) * ((X-SpanStart (C,n)),((Y-SpanStart (C,n)) + (t + 1))))) by RLTOPSP1:69;
A16: ((Y-SpanStart (C,n)) + t) + 1 = (Y-SpanStart (C,n)) + (t + 1) ;
then A17: 1 <= (Y-SpanStart (C,n)) + (t + 1) by NAT_1:11;
A18: Y-InitStart C > 1 by JORDAN11:2;
then Y-InitStart C >= (1 + 1) + 0 by NAT_1:13;
then (Y-InitStart C) - 2 >= 0 by XREAL_1:19;
then A19: (Y-InitStart C) -' 2 = (Y-InitStart C) - 2 by XREAL_0:def_2;
assume A20: t + 1 <= (((2 |^ (n -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2) - (Y-SpanStart (C,n)) ; ::_thesis: (cell ((Gauge (C,n)),((X-SpanStart (C,n)) -' 1),((Y-SpanStart (C,n)) + (t + 1)))) \ (L~ (Span (C,n))) c= BDD (L~ (Span (C,n)))
then A21: (t + 1) + (Y-SpanStart (C,n)) <= ((2 |^ (n -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2 by XREAL_1:19;
assume not (cell ((Gauge (C,n)),((X-SpanStart (C,n)) -' 1),((Y-SpanStart (C,n)) + (t + 1)))) \ (L~ (Span (C,n))) c= BDD (L~ (Span (C,n))) ; ::_thesis: contradiction
then consider x being set such that
A22: x in (cell ((Gauge (C,n)),((X-SpanStart (C,n)) -' 1),((Y-SpanStart (C,n)) + (t + 1)))) \ (L~ (Span (C,n))) and
A23: not x in BDD (L~ (Span (C,n))) by TARSKI:def_3;
not x in L~ (Span (C,n)) by A22, XBOOLE_0:def_5;
then x in (L~ (Span (C,n))) ` by A22, SUBSET_1:29;
then x in (BDD (L~ (Span (C,n)))) \/ (UBD (L~ (Span (C,n)))) by JORDAN2C:27;
then x in UBD (L~ (Span (C,n))) by A23, XBOOLE_0:def_3;
then A24: (cell ((Gauge (C,n)),((X-SpanStart (C,n)) -' 1),((Y-SpanStart (C,n)) + (t + 1)))) \ (L~ (Span (C,n))) meets UBD (L~ (Span (C,n))) by A22, XBOOLE_0:3;
A25: Y-InitStart C < width (Gauge (C,(ApproxIndex C))) by JORDAN11:def_2;
ApproxIndex C <= n by A1, JORDAN11:def_1;
then ((2 |^ (n -' (ApproxIndex C))) * ((Y-InitStart C) - 2)) + 2 < width (Gauge (C,n)) by A18, A25, JORDAN1A:32;
then A26: ((Y-SpanStart (C,n)) + t) + 1 <= width (Gauge (C,n)) by A19, A21, XXREAL_0:2;
A27: ((Y-SpanStart (C,n)) + t) + 1 <= ((2 |^ (n -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2 by A21;
A28: now__::_thesis:_not_(1_/_2)_*_(((Gauge_(C,n))_*_(((X-SpanStart_(C,n))_-'_1),((Y-SpanStart_(C,n))_+_(t_+_1))))_+_((Gauge_(C,n))_*_((X-SpanStart_(C,n)),((Y-SpanStart_(C,n))_+_(t_+_1)))))_in_L~_(Span_(C,n))
A29: Y-SpanStart (C,n) <= (Y-SpanStart (C,n)) + (t + 1) by NAT_1:11;
A30: X-SpanStart (C,n) < len (Gauge (C,n)) by JORDAN1H:49;
assume (1 / 2) * (((Gauge (C,n)) * (((X-SpanStart (C,n)) -' 1),((Y-SpanStart (C,n)) + (t + 1)))) + ((Gauge (C,n)) * ((X-SpanStart (C,n)),((Y-SpanStart (C,n)) + (t + 1))))) in L~ (Span (C,n)) ; ::_thesis: contradiction
then consider i being Element of NAT such that
A31: 1 <= i and
A32: i + 1 <= len (Span (C,n)) and
A33: (1 / 2) * (((Gauge (C,n)) * (((X-SpanStart (C,n)) -' 1),((Y-SpanStart (C,n)) + (t + 1)))) + ((Gauge (C,n)) * ((X-SpanStart (C,n)),((Y-SpanStart (C,n)) + (t + 1))))) in LSeg ((Span (C,n)),i) by SPPOL_2:13;
A34: LSeg ((Span (C,n)),i) = LSeg (((Span (C,n)) /. i),((Span (C,n)) /. (i + 1))) by A31, A32, TOPREAL1:def_3;
consider i1, j1, i2, j2 being Element of NAT such that
A35: [i1,j1] in Indices (Gauge (C,n)) and
A36: (Span (C,n)) /. i = (Gauge (C,n)) * (i1,j1) and
A37: [i2,j2] in Indices (Gauge (C,n)) and
A38: (Span (C,n)) /. (i + 1) = (Gauge (C,n)) * (i2,j2) and
A39: ( ( i1 = i2 & j1 + 1 = j2 ) or ( i1 + 1 = i2 & j1 = j2 ) or ( i1 = i2 + 1 & j1 = j2 ) or ( i1 = i2 & j1 = j2 + 1 ) ) by A4, A31, A32, JORDAN8:3;
A40: 1 <= i1 by A35, MATRIX_1:38;
A41: i2 <= len (Gauge (C,n)) by A37, MATRIX_1:38;
A42: 1 <= i2 by A37, MATRIX_1:38;
A43: j1 <= width (Gauge (C,n)) by A35, MATRIX_1:38;
A44: 1 <= j2 by A37, MATRIX_1:38;
A45: i1 <= len (Gauge (C,n)) by A35, MATRIX_1:38;
A46: j2 <= width (Gauge (C,n)) by A37, MATRIX_1:38;
A47: 1 <= j1 by A35, MATRIX_1:38;
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 A39;
suppose ( i1 = i2 & j1 + 1 = j2 ) ; ::_thesis: contradiction
hence contradiction by A7, A8, A26, A17, A33, A34, A36, A38, A40, A45, A47, A46, A30, GOBOARD7:27; ::_thesis: verum
end;
supposeA48: ( i1 + 1 = i2 & j1 = j2 ) ; ::_thesis: contradiction
then A49: (Y-SpanStart (C,n)) + (t + 1) = j1 by A7, A8, A26, A17, A33, A34, A36, A38, A40, A47, A43, A41, A30, GOBOARD7:26;
A50: cell ((Gauge (C,n)),((X-SpanStart (C,n)) -' 1),((Y-SpanStart (C,n)) + (t + 1))) c= BDD C by A1, A21, A29, JORDAN11:def_3;
A51: left_cell ((Span (C,n)),i,(Gauge (C,n))) = cell ((Gauge (C,n)),i1,j1) by A4, A31, A32, A35, A36, A37, A38, A48, GOBRD13:23;
(X-SpanStart (C,n)) -' 1 = i1 by A7, A8, A26, A17, A33, A34, A36, A38, A40, A47, A43, A41, A30, A48, GOBOARD7:26;
then cell ((Gauge (C,n)),((X-SpanStart (C,n)) -' 1),((Y-SpanStart (C,n)) + (t + 1))) meets C by A1, A31, A32, A49, A51, Th7;
hence contradiction by A50, JORDAN1A:7, XBOOLE_1:63; ::_thesis: verum
end;
supposeA52: ( i1 = i2 + 1 & j1 = j2 ) ; ::_thesis: contradiction
then A53: left_cell ((Span (C,n)),i,(Gauge (C,n))) = cell ((Gauge (C,n)),i2,(j2 -' 1)) by A4, A31, A32, A35, A36, A37, A38, GOBRD13:25;
A54: (Y-SpanStart (C,n)) + (t + 1) = j2 by A7, A8, A26, A17, A33, A34, A36, A38, A45, A47, A43, A42, A30, A52, GOBOARD7:26;
(X-SpanStart (C,n)) -' 1 = i2 by A7, A8, A26, A17, A33, A34, A36, A38, A45, A47, A43, A42, A30, A52, GOBOARD7:26;
then cell ((Gauge (C,n)),((X-SpanStart (C,n)) -' 1),(((Y-SpanStart (C,n)) + (t + 1)) -' 1)) meets C by A1, A31, A32, A54, A53, Th7;
then A55: cell ((Gauge (C,n)),((X-SpanStart (C,n)) -' 1),((Y-SpanStart (C,n)) + t)) meets C by A16, NAT_D:34;
A56: Y-SpanStart (C,n) <= (Y-SpanStart (C,n)) + t by NAT_1:11;
(Y-SpanStart (C,n)) + t <= ((2 |^ (n -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2 by A27, NAT_1:13;
then cell ((Gauge (C,n)),((X-SpanStart (C,n)) -' 1),((Y-SpanStart (C,n)) + t)) c= BDD C by A1, A56, JORDAN11:def_3;
hence contradiction by A55, JORDAN1A:7, XBOOLE_1:63; ::_thesis: verum
end;
suppose ( i1 = i2 & j1 = j2 + 1 ) ; ::_thesis: contradiction
hence contradiction by A7, A8, A26, A17, A33, A34, A36, A38, A40, A45, A43, A44, A30, GOBOARD7:27; ::_thesis: verum
end;
end;
end;
(Y-SpanStart (C,n)) + t < width (Gauge (C,n)) by A26, NAT_1:13;
then LSeg (((Gauge (C,n)) * (((X-SpanStart (C,n)) -' 1),((Y-SpanStart (C,n)) + (t + 1)))),((Gauge (C,n)) * ((X-SpanStart (C,n)),((Y-SpanStart (C,n)) + (t + 1))))) c= cell ((Gauge (C,n)),((X-SpanStart (C,n)) -' 1),((Y-SpanStart (C,n)) + t)) by A7, A9, A8, A16, GOBOARD5:21;
then A57: (1 / 2) * (((Gauge (C,n)) * (((X-SpanStart (C,n)) -' 1),((Y-SpanStart (C,n)) + (t + 1)))) + ((Gauge (C,n)) * ((X-SpanStart (C,n)),((Y-SpanStart (C,n)) + (t + 1))))) in (cell ((Gauge (C,n)),((X-SpanStart (C,n)) -' 1),((Y-SpanStart (C,n)) + t))) \ (L~ (Span (C,n))) by A28, A15, XBOOLE_0:def_5;
LSeg (((Gauge (C,n)) * (((X-SpanStart (C,n)) -' 1),((Y-SpanStart (C,n)) + (t + 1)))),((Gauge (C,n)) * ((X-SpanStart (C,n)),((Y-SpanStart (C,n)) + (t + 1))))) c= cell ((Gauge (C,n)),((X-SpanStart (C,n)) -' 1),((Y-SpanStart (C,n)) + (t + 1))) by A7, A9, A8, A26, A17, GOBOARD5:22;
then A58: (1 / 2) * (((Gauge (C,n)) * (((X-SpanStart (C,n)) -' 1),((Y-SpanStart (C,n)) + (t + 1)))) + ((Gauge (C,n)) * ((X-SpanStart (C,n)),((Y-SpanStart (C,n)) + (t + 1))))) in (cell ((Gauge (C,n)),((X-SpanStart (C,n)) -' 1),((Y-SpanStart (C,n)) + (t + 1)))) \ (L~ (Span (C,n))) by A28, A15, XBOOLE_0:def_5;
LeftComp (Span (C,n)) is_a_component_of (L~ (Span (C,n))) ` by GOBOARD9:def_1;
then UBD (L~ (Span (C,n))) is_a_component_of (L~ (Span (C,n))) ` by GOBRD14:36;
then (cell ((Gauge (C,n)),((X-SpanStart (C,n)) -' 1),((Y-SpanStart (C,n)) + (t + 1)))) \ (L~ (Span (C,n))) c= UBD (L~ (Span (C,n))) by A4, A9, A26, A24, A13, Th29, GOBOARD9:4;
then BDD (L~ (Span (C,n))) meets UBD (L~ (Span (C,n))) by A11, A20, A12, A57, A58, XBOOLE_0:3, XXREAL_0:2;
hence contradiction by JORDAN2C:24; ::_thesis: verum
end;
A59: S1[ 0 ]
proof
assume 0 <= (((2 |^ (n -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2) - (Y-SpanStart (C,n)) ; ::_thesis: (cell ((Gauge (C,n)),((X-SpanStart (C,n)) -' 1),((Y-SpanStart (C,n)) + 0))) \ (L~ (Span (C,n))) c= BDD (L~ (Span (C,n)))
A60: (Span (C,n)) /. (1 + 1) = (Gauge (C,n)) * (((X-SpanStart (C,n)) -' 1),(Y-SpanStart (C,n))) by A1, JORDAN13:def_1;
A61: [(X-SpanStart (C,n)),(Y-SpanStart (C,n))] in Indices (Gauge (C,n)) by A1, JORDAN11:8;
A62: [((X-SpanStart (C,n)) -' 1),(Y-SpanStart (C,n))] in Indices (Gauge (C,n)) by A1, JORDAN11:9;
A63: len (Span (C,n)) >= 1 + 1 by GOBOARD7:34, XXREAL_0:2;
then A64: (right_cell ((Span (C,n)),1,(Gauge (C,n)))) \ (L~ (Span (C,n))) c= RightComp (Span (C,n)) by A4, JORDAN9:27;
(Span (C,n)) /. 1 = (Gauge (C,n)) * ((X-SpanStart (C,n)),(Y-SpanStart (C,n))) by A1, JORDAN13:def_1;
then right_cell ((Span (C,n)),1,(Gauge (C,n))) = cell ((Gauge (C,n)),((X-SpanStart (C,n)) -' 1),(Y-SpanStart (C,n))) by A4, A8, A63, A60, A61, A62, GOBRD13:26;
hence (cell ((Gauge (C,n)),((X-SpanStart (C,n)) -' 1),((Y-SpanStart (C,n)) + 0))) \ (L~ (Span (C,n))) c= BDD (L~ (Span (C,n))) by A64, GOBRD14:37; ::_thesis: verum
end;
for t being Element of NAT holds S1[t] from NAT_1:sch_1(A59, A10);
hence (cell ((Gauge (C,n)),((X-SpanStart (C,n)) -' 1),k)) \ (L~ (Span (C,n))) c= BDD (L~ (Span (C,n))) by A6, A5; ::_thesis: verum
end;
theorem Th31: :: JORDAN14:31
for C being Subset of (TOP-REAL 2)
for n, m, i being Element of NAT st m <= n & 1 < i & i + 1 < len (Gauge (C,m)) holds
(((2 |^ (n -' m)) * (i - 2)) + 2) + 1 < len (Gauge (C,n))
proof
let C be Subset of (TOP-REAL 2); ::_thesis: for n, m, i being Element of NAT st m <= n & 1 < i & i + 1 < len (Gauge (C,m)) holds
(((2 |^ (n -' m)) * (i - 2)) + 2) + 1 < len (Gauge (C,n))
let n, m, i be Element of NAT ; ::_thesis: ( m <= n & 1 < i & i + 1 < len (Gauge (C,m)) implies (((2 |^ (n -' m)) * (i - 2)) + 2) + 1 < len (Gauge (C,n)) )
assume that
A1: m <= n and
A2: 1 < i and
A3: i + 1 < len (Gauge (C,m)) ; ::_thesis: (((2 |^ (n -' m)) * (i - 2)) + 2) + 1 < len (Gauge (C,n))
1 + 1 <= i by A2, NAT_1:13;
then reconsider i2 = i - 2 as Element of NAT by INT_1:5;
A4: 2 |^ (n -' m) > 0 by NEWTON:83;
len (Gauge (C,m)) = (2 |^ m) + (2 + 1) by JORDAN8:def_1
.= ((2 |^ m) + 2) + 1 ;
then i < (2 |^ m) + 2 by A3, XREAL_1:7;
then i2 < 2 |^ m by XREAL_1:19;
then (2 |^ (n -' m)) * i2 < (2 |^ (n -' m)) * (2 |^ m) by A4, XREAL_1:68;
then (2 |^ (n -' m)) * i2 < 2 |^ ((n -' m) + m) by NEWTON:8;
then (2 |^ (n -' m)) * i2 < 2 |^ n by A1, XREAL_1:235;
then ((2 |^ (n -' m)) * i2) + 2 < (2 |^ n) + 2 by XREAL_1:8;
then (((2 |^ (n -' m)) * (i - 2)) + 2) + 1 < ((2 |^ n) + 2) + 1 by XREAL_1:8;
then (((2 |^ (n -' m)) * (i - 2)) + 2) + 1 < (2 |^ n) + (1 + 2) ;
hence (((2 |^ (n -' m)) * (i - 2)) + 2) + 1 < len (Gauge (C,n)) by JORDAN8:def_1; ::_thesis: verum
end;
theorem Th32: :: JORDAN14:32
for C being Simple_closed_curve
for n, m being Element of NAT st n is_sufficiently_large_for C & n <= m holds
RightComp (Span (C,n)) meets RightComp (Span (C,m))
proof
let C be Simple_closed_curve; ::_thesis: for n, m being Element of NAT st n is_sufficiently_large_for C & n <= m holds
RightComp (Span (C,n)) meets RightComp (Span (C,m))
let n, m be Element of NAT ; ::_thesis: ( n is_sufficiently_large_for C & n <= m implies RightComp (Span (C,n)) meets RightComp (Span (C,m)) )
assume that
A1: n is_sufficiently_large_for C and
A2: n <= m ; ::_thesis: RightComp (Span (C,n)) meets RightComp (Span (C,m))
set i1 = X-SpanStart (C,m);
set G1 = Gauge (C,m);
set YI = Y-InitStart C;
set AI = ApproxIndex C;
A3: m is_sufficiently_large_for C by A1, A2, Th28;
then A4: ApproxIndex C <= m by JORDAN11:def_1;
set i = X-SpanStart (C,n);
set G = Gauge (C,n);
A5: 1 <= (X-SpanStart (C,m)) -' 1 by JORDAN1H:50;
set j1 = Y-SpanStart (C,m);
set f1 = Span (C,m);
Y-SpanStart (C,m) <= ((2 |^ (m -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2 by A3, JORDAN11:5;
then A6: (cell ((Gauge (C,m)),((X-SpanStart (C,m)) -' 1),(((2 |^ (m -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2))) \ (L~ (Span (C,m))) c= BDD (L~ (Span (C,m))) by A1, A2, Th28, Th30;
A7: X-SpanStart (C,n) < len (Gauge (C,n)) by JORDAN1H:49;
then (X-SpanStart (C,n)) + 1 <= len (Gauge (C,n)) by NAT_1:13;
then A8: X-SpanStart (C,n) <= (len (Gauge (C,n))) - 1 by XREAL_1:19;
set XSAI = X-SpanStart (C,(ApproxIndex C));
set p2 = (Gauge (C,(ApproxIndex C))) * ((X-SpanStart (C,(ApproxIndex C))),(Y-InitStart C));
A9: 1 < X-SpanStart (C,(ApproxIndex C)) by JORDAN1H:49, XXREAL_0:2;
A10: (Y-InitStart C) + 1 < width (Gauge (C,(ApproxIndex C))) by JORDAN11:3;
then A11: Y-InitStart C < width (Gauge (C,(ApproxIndex C))) by NAT_1:13;
set j4 = ((2 |^ (n -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2;
A12: X-SpanStart (C,m) < len (Gauge (C,m)) by JORDAN1H:49;
set j = Y-SpanStart (C,n);
set f = Span (C,n);
Y-SpanStart (C,n) <= ((2 |^ (n -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2 by A1, JORDAN11:5;
then A13: (cell ((Gauge (C,n)),((X-SpanStart (C,n)) -' 1),(((2 |^ (n -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2))) \ (L~ (Span (C,n))) c= BDD (L~ (Span (C,n))) by A1, Th30;
A14: Int (cell ((Gauge (C,n)),((X-SpanStart (C,n)) -' 1),(((2 |^ (n -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2))) c= cell ((Gauge (C,n)),((X-SpanStart (C,n)) -' 1),(((2 |^ (n -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2)) by TOPS_1:16;
A15: 2 < X-SpanStart (C,n) by JORDAN1H:49;
then A16: ((X-SpanStart (C,n)) -' 1) + 1 = X-SpanStart (C,n) by XREAL_1:235, XXREAL_0:2;
then A17: (X-SpanStart (C,n)) -' 1 >= 1 + 1 by A15, NAT_1:13;
set j3 = ((2 |^ (m -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2;
A18: X-SpanStart (C,n) < len (Gauge (C,n)) by JORDAN1H:49;
A19: Y-InitStart C > 1 by JORDAN11:2;
then Y-InitStart C >= (1 + 1) + 0 by NAT_1:13;
then A20: (Y-InitStart C) - 2 >= 0 by XREAL_1:19;
then A21: ((2 |^ (n -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2 = ((2 |^ (n -' (ApproxIndex C))) * ((Y-InitStart C) - 2)) + 2 by XREAL_0:def_2;
A22: ((2 |^ (m -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2 = ((2 |^ (m -' (ApproxIndex C))) * ((Y-InitStart C) - 2)) + 2 by A20, XREAL_0:def_2;
then A23: 1 < ((2 |^ (m -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2 by A4, A11, A19, JORDAN1A:32;
set p3 = (1 / 2) * (((Gauge (C,m)) * (((X-SpanStart (C,m)) -' 1),(((2 |^ (m -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2))) + ((Gauge (C,m)) * ((X-SpanStart (C,m)),((((2 |^ (m -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2) + 1))));
A24: (X-SpanStart (C,m)) -' 1 < len (Gauge (C,m)) by JORDAN1H:50;
A25: ((2 |^ (m -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2 < width (Gauge (C,m)) by A4, A11, A19, A22, JORDAN1A:32;
then A26: (((2 |^ (m -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2) + 1 <= width (Gauge (C,m)) by NAT_1:13;
2 < X-SpanStart (C,m) by JORDAN1H:49;
then A27: ((X-SpanStart (C,m)) -' 1) + 1 = X-SpanStart (C,m) by XREAL_1:235, XXREAL_0:2;
then A28: (1 / 2) * (((Gauge (C,m)) * (((X-SpanStart (C,m)) -' 1),(((2 |^ (m -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2))) + ((Gauge (C,m)) * ((X-SpanStart (C,m)),((((2 |^ (m -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2) + 1)))) in Int (cell ((Gauge (C,m)),((X-SpanStart (C,m)) -' 1),(((2 |^ (m -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2))) by A12, A23, A5, A26, GOBOARD6:31;
then A29: ((Gauge (C,m)) * (((X-SpanStart (C,m)) -' 1),(((2 |^ (m -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2))) `2 < ((1 / 2) * (((Gauge (C,m)) * (((X-SpanStart (C,m)) -' 1),(((2 |^ (m -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2))) + ((Gauge (C,m)) * ((X-SpanStart (C,m)),((((2 |^ (m -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2) + 1))))) `2 by A12, A23, A27, A5, A26, Th4;
A30: ((1 / 2) * (((Gauge (C,m)) * (((X-SpanStart (C,m)) -' 1),(((2 |^ (m -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2))) + ((Gauge (C,m)) * ((X-SpanStart (C,m)),((((2 |^ (m -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2) + 1))))) `2 < ((Gauge (C,m)) * (((X-SpanStart (C,m)) -' 1),((((2 |^ (m -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2) + 1))) `2 by A12, A23, A27, A5, A26, A28, Th4;
A31: ((Gauge (C,m)) * (((X-SpanStart (C,m)) -' 1),(((2 |^ (m -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2))) `1 < ((1 / 2) * (((Gauge (C,m)) * (((X-SpanStart (C,m)) -' 1),(((2 |^ (m -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2))) + ((Gauge (C,m)) * ((X-SpanStart (C,m)),((((2 |^ (m -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2) + 1))))) `1 by A12, A23, A27, A5, A26, A28, Th4;
A32: 1 < X-SpanStart (C,m) by JORDAN1H:49, XXREAL_0:2;
then A33: ((Gauge (C,m)) * ((X-SpanStart (C,m)),(((2 |^ (m -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2))) `2 = ((Gauge (C,m)) * (1,(((2 |^ (m -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2))) `2 by A12, A23, A25, GOBOARD5:1
.= ((Gauge (C,m)) * (((X-SpanStart (C,m)) -' 1),(((2 |^ (m -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2))) `2 by A23, A25, A5, A24, GOBOARD5:1 ;
A34: (((2 |^ (m -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2) + 1 >= 1 by NAT_1:11;
then A35: ((Gauge (C,m)) * ((X-SpanStart (C,m)),((((2 |^ (m -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2) + 1))) `2 = ((Gauge (C,m)) * (1,((((2 |^ (m -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2) + 1))) `2 by A12, A32, A26, GOBOARD5:1
.= ((Gauge (C,m)) * (((X-SpanStart (C,m)) -' 1),((((2 |^ (m -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2) + 1))) `2 by A5, A24, A26, A34, GOBOARD5:1 ;
A36: 1 <= (X-SpanStart (C,n)) -' 1 by JORDAN1H:50;
A37: ApproxIndex C <= n by A1, JORDAN11:def_1;
then A38: 1 < ((2 |^ (n -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2 by A11, A19, A21, JORDAN1A:32;
(Y-InitStart C) + 1 < len (Gauge (C,(ApproxIndex C))) by A10, JORDAN8:def_1;
then (((2 |^ (n -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2) + 1 < len (Gauge (C,n)) by A37, A21, Th31, JORDAN11:2;
then ((((2 |^ (n -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2) + 1) + 1 <= len (Gauge (C,n)) by NAT_1:13;
then A39: (((2 |^ (n -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2) + 1 <= (len (Gauge (C,n))) - 1 by XREAL_1:19;
A40: (X-SpanStart (C,n)) -' 1 < len (Gauge (C,n)) by JORDAN1H:50;
then ((X-SpanStart (C,n)) -' 1) + 1 <= len (Gauge (C,n)) by NAT_1:13;
then A41: (X-SpanStart (C,n)) -' 1 <= (len (Gauge (C,n))) - 1 by XREAL_1:19;
A42: ((2 |^ (n -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2 < width (Gauge (C,n)) by A37, A11, A19, A21, JORDAN1A:32;
then A43: (((2 |^ (n -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2) + 1 <= width (Gauge (C,n)) by NAT_1:13;
((2 |^ (n -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2 < len (Gauge (C,n)) by A42, JORDAN8:def_1;
then (((2 |^ (n -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2) + 1 <= len (Gauge (C,n)) by NAT_1:13;
then A44: ((2 |^ (n -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2 <= (len (Gauge (C,n))) - 1 by XREAL_1:19;
A45: X-SpanStart (C,(ApproxIndex C)) < len (Gauge (C,(ApproxIndex C))) by JORDAN1H:49;
X-SpanStart (C,m) = ((2 |^ (m -' (ApproxIndex C))) * ((X-SpanStart (C,(ApproxIndex C))) - 2)) + 2 by A1, A2, Th28, JORDAN11:4;
then A46: (Gauge (C,(ApproxIndex C))) * ((X-SpanStart (C,(ApproxIndex C))),(Y-InitStart C)) = (Gauge (C,m)) * ((X-SpanStart (C,m)),(((2 |^ (m -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2)) by A4, A9, A45, A11, A19, A22, JORDAN1A:33;
A47: X-SpanStart (C,n) = ((2 |^ (n -' (ApproxIndex C))) * ((X-SpanStart (C,(ApproxIndex C))) - 2)) + 2 by A1, JORDAN11:4;
then A48: (Gauge (C,(ApproxIndex C))) * ((X-SpanStart (C,(ApproxIndex C))),(Y-InitStart C)) = (Gauge (C,n)) * ((X-SpanStart (C,n)),(((2 |^ (n -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2)) by A37, A9, A45, A11, A19, A21, JORDAN1A:33;
A49: 1 < X-SpanStart (C,n) by JORDAN1H:49, XXREAL_0:2;
then ((Gauge (C,n)) * ((X-SpanStart (C,n)),(((2 |^ (n -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2))) `2 = ((Gauge (C,n)) * (1,(((2 |^ (n -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2))) `2 by A18, A38, A42, GOBOARD5:1
.= ((Gauge (C,n)) * (((X-SpanStart (C,n)) -' 1),(((2 |^ (n -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2))) `2 by A38, A42, A36, A40, GOBOARD5:1 ;
then A50: ((Gauge (C,n)) * (((X-SpanStart (C,n)) -' 1),(((2 |^ (n -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2))) `2 < ((1 / 2) * (((Gauge (C,m)) * (((X-SpanStart (C,m)) -' 1),(((2 |^ (m -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2))) + ((Gauge (C,m)) * ((X-SpanStart (C,m)),((((2 |^ (m -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2) + 1))))) `2 by A47, A37, A9, A45, A11, A19, A21, A46, A29, A33, JORDAN1A:33;
((1 / 2) * (((Gauge (C,m)) * (((X-SpanStart (C,m)) -' 1),(((2 |^ (m -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2))) + ((Gauge (C,m)) * ((X-SpanStart (C,m)),((((2 |^ (m -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2) + 1))))) `1 < ((Gauge (C,m)) * ((X-SpanStart (C,m)),(((2 |^ (m -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2))) `1 by A12, A23, A27, A5, A26, A28, Th4;
then A51: ((1 / 2) * (((Gauge (C,m)) * (((X-SpanStart (C,m)) -' 1),(((2 |^ (m -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2))) + ((Gauge (C,m)) * ((X-SpanStart (C,m)),((((2 |^ (m -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2) + 1))))) `1 < ((Gauge (C,n)) * ((X-SpanStart (C,n)),(((2 |^ (n -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2))) `1 by A47, A37, A9, A45, A11, A19, A21, A46, JORDAN1A:33;
((2 |^ (n -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2 >= 1 + 1 by A38, NAT_1:13;
then ex c, d being Element of NAT st
( 2 <= c & c <= (len (Gauge (C,m))) - 1 & 2 <= d & d <= (len (Gauge (C,m))) - 1 & [c,d] in Indices (Gauge (C,m)) & (Gauge (C,n)) * (((X-SpanStart (C,n)) -' 1),(((2 |^ (n -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2)) = (Gauge (C,m)) * (c,d) & c = 2 + ((2 |^ (m -' n)) * (((X-SpanStart (C,n)) -' 1) -' 2)) & d = 2 + ((2 |^ (m -' n)) * ((((2 |^ (n -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2) -' 2)) ) by A2, A17, A41, A44, GOBRD14:8;
then (Gauge (C,n)) * (((X-SpanStart (C,n)) -' 1),(((2 |^ (n -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2)) in { ((Gauge (C,m)) * (ii,jj)) where ii, jj is Element of NAT : [ii,jj] in Indices (Gauge (C,m)) } ;
then (Gauge (C,n)) * (((X-SpanStart (C,n)) -' 1),(((2 |^ (n -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2)) in Values (Gauge (C,m)) by MATRIX_1:45;
then ((Gauge (C,n)) * (((X-SpanStart (C,n)) -' 1),(((2 |^ (n -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2))) `1 <= ((Gauge (C,m)) * (((X-SpanStart (C,m)) -' 1),(((2 |^ (m -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2))) `1 by A48, A46, A49, A18, A38, A42, A12, A32, A23, A25, GOBRD13:14;
then A52: ((Gauge (C,n)) * (((X-SpanStart (C,n)) -' 1),(((2 |^ (n -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2))) `1 < ((1 / 2) * (((Gauge (C,m)) * (((X-SpanStart (C,m)) -' 1),(((2 |^ (m -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2))) + ((Gauge (C,m)) * ((X-SpanStart (C,m)),((((2 |^ (m -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2) + 1))))) `1 by A31, XXREAL_0:2;
(((2 |^ (n -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2) + 1 > 1 + 1 by A38, XREAL_1:6;
then ex c, d being Element of NAT st
( 2 <= c & c <= (len (Gauge (C,m))) - 1 & 2 <= d & d <= (len (Gauge (C,m))) - 1 & [c,d] in Indices (Gauge (C,m)) & (Gauge (C,n)) * ((X-SpanStart (C,n)),((((2 |^ (n -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2) + 1)) = (Gauge (C,m)) * (c,d) & c = 2 + ((2 |^ (m -' n)) * ((X-SpanStart (C,n)) -' 2)) & d = 2 + ((2 |^ (m -' n)) * (((((2 |^ (n -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2) + 1) -' 2)) ) by A2, A15, A8, A39, GOBRD14:8;
then (Gauge (C,n)) * ((X-SpanStart (C,n)),((((2 |^ (n -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2) + 1)) in { ((Gauge (C,m)) * (ii,jj)) where ii, jj is Element of NAT : [ii,jj] in Indices (Gauge (C,m)) } ;
then (Gauge (C,n)) * ((X-SpanStart (C,n)),((((2 |^ (n -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2) + 1)) in Values (Gauge (C,m)) by MATRIX_1:45;
then A53: ((Gauge (C,m)) * ((X-SpanStart (C,m)),((((2 |^ (m -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2) + 1))) `2 <= ((Gauge (C,n)) * ((X-SpanStart (C,n)),((((2 |^ (n -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2) + 1))) `2 by A48, A46, A49, A18, A38, A42, A12, A32, A23, A25, GOBRD13:15;
A54: (((2 |^ (n -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2) + 1 >= 1 by NAT_1:11;
then ((Gauge (C,n)) * ((X-SpanStart (C,n)),((((2 |^ (n -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2) + 1))) `2 = ((Gauge (C,n)) * (1,((((2 |^ (n -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2) + 1))) `2 by A49, A18, A43, GOBOARD5:1
.= ((Gauge (C,n)) * (((X-SpanStart (C,n)) -' 1),((((2 |^ (n -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2) + 1))) `2 by A36, A40, A43, A54, GOBOARD5:1 ;
then ((1 / 2) * (((Gauge (C,m)) * (((X-SpanStart (C,m)) -' 1),(((2 |^ (m -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2))) + ((Gauge (C,m)) * ((X-SpanStart (C,m)),((((2 |^ (m -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2) + 1))))) `2 < ((Gauge (C,n)) * (((X-SpanStart (C,n)) -' 1),((((2 |^ (n -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2) + 1))) `2 by A30, A35, A53, XXREAL_0:2;
then A55: (1 / 2) * (((Gauge (C,m)) * (((X-SpanStart (C,m)) -' 1),(((2 |^ (m -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2))) + ((Gauge (C,m)) * ((X-SpanStart (C,m)),((((2 |^ (m -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2) + 1)))) in Int (cell ((Gauge (C,n)),((X-SpanStart (C,n)) -' 1),(((2 |^ (n -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2))) by A7, A38, A16, A36, A52, A51, A43, A50, Th4;
Span (C,n) is_sequence_on Gauge (C,n) by A1, JORDAN13:def_1;
then Int (cell ((Gauge (C,n)),((X-SpanStart (C,n)) -' 1),(((2 |^ (n -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2))) misses L~ (Span (C,n)) by A42, A40, JORDAN9:14;
then not (1 / 2) * (((Gauge (C,m)) * (((X-SpanStart (C,m)) -' 1),(((2 |^ (m -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2))) + ((Gauge (C,m)) * ((X-SpanStart (C,m)),((((2 |^ (m -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2) + 1)))) in L~ (Span (C,n)) by A55, XBOOLE_0:3;
then (1 / 2) * (((Gauge (C,m)) * (((X-SpanStart (C,m)) -' 1),(((2 |^ (m -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2))) + ((Gauge (C,m)) * ((X-SpanStart (C,m)),((((2 |^ (m -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2) + 1)))) in (cell ((Gauge (C,n)),((X-SpanStart (C,n)) -' 1),(((2 |^ (n -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2))) \ (L~ (Span (C,n))) by A55, A14, XBOOLE_0:def_5;
then (1 / 2) * (((Gauge (C,m)) * (((X-SpanStart (C,m)) -' 1),(((2 |^ (m -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2))) + ((Gauge (C,m)) * ((X-SpanStart (C,m)),((((2 |^ (m -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2) + 1)))) in BDD (L~ (Span (C,n))) by A13;
then A56: (1 / 2) * (((Gauge (C,m)) * (((X-SpanStart (C,m)) -' 1),(((2 |^ (m -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2))) + ((Gauge (C,m)) * ((X-SpanStart (C,m)),((((2 |^ (m -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2) + 1)))) in RightComp (Span (C,n)) by GOBRD14:37;
Span (C,m) is_sequence_on Gauge (C,m) by A3, JORDAN13:def_1;
then Int (cell ((Gauge (C,m)),((X-SpanStart (C,m)) -' 1),(((2 |^ (m -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2))) misses L~ (Span (C,m)) by A25, A24, JORDAN9:14;
then A57: not (1 / 2) * (((Gauge (C,m)) * (((X-SpanStart (C,m)) -' 1),(((2 |^ (m -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2))) + ((Gauge (C,m)) * ((X-SpanStart (C,m)),((((2 |^ (m -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2) + 1)))) in L~ (Span (C,m)) by A28, XBOOLE_0:3;
Int (cell ((Gauge (C,m)),((X-SpanStart (C,m)) -' 1),(((2 |^ (m -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2))) c= cell ((Gauge (C,m)),((X-SpanStart (C,m)) -' 1),(((2 |^ (m -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2)) by TOPS_1:16;
then (1 / 2) * (((Gauge (C,m)) * (((X-SpanStart (C,m)) -' 1),(((2 |^ (m -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2))) + ((Gauge (C,m)) * ((X-SpanStart (C,m)),((((2 |^ (m -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2) + 1)))) in (cell ((Gauge (C,m)),((X-SpanStart (C,m)) -' 1),(((2 |^ (m -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2))) \ (L~ (Span (C,m))) by A28, A57, XBOOLE_0:def_5;
then (1 / 2) * (((Gauge (C,m)) * (((X-SpanStart (C,m)) -' 1),(((2 |^ (m -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2))) + ((Gauge (C,m)) * ((X-SpanStart (C,m)),((((2 |^ (m -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2) + 1)))) in BDD (L~ (Span (C,m))) by A6;
then (1 / 2) * (((Gauge (C,m)) * (((X-SpanStart (C,m)) -' 1),(((2 |^ (m -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2))) + ((Gauge (C,m)) * ((X-SpanStart (C,m)),((((2 |^ (m -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2) + 1)))) in RightComp (Span (C,m)) by GOBRD14:37;
hence RightComp (Span (C,n)) meets RightComp (Span (C,m)) by A56, XBOOLE_0:3; ::_thesis: verum
end;
theorem Th33: :: JORDAN14:33
for G being Go-board
for f being FinSequence of (TOP-REAL 2) st f is_sequence_on G & f is special holds
for i, j being Element of NAT st i <= len G & j <= width G holds
Int (cell (G,i,j)) c= (L~ f) `
proof
let G be Go-board; ::_thesis: for f being FinSequence of (TOP-REAL 2) st f is_sequence_on G & f is special holds
for i, j being Element of NAT st i <= len G & j <= width G holds
Int (cell (G,i,j)) c= (L~ f) `
let f be FinSequence of (TOP-REAL 2); ::_thesis: ( f is_sequence_on G & f is special implies for i, j being Element of NAT st i <= len G & j <= width G holds
Int (cell (G,i,j)) c= (L~ f) ` )
assume that
A1: f is_sequence_on G and
A2: f is special ; ::_thesis: for i, j being Element of NAT st i <= len G & j <= width G holds
Int (cell (G,i,j)) c= (L~ f) `
let i, j be Element of NAT ; ::_thesis: ( i <= len G & j <= width G implies Int (cell (G,i,j)) c= (L~ f) ` )
assume that
A3: i <= len G and
A4: j <= width G ; ::_thesis: Int (cell (G,i,j)) c= (L~ f) `
Int (cell (G,i,j)) misses L~ f by A1, A2, A3, A4, JORDAN9:14;
hence Int (cell (G,i,j)) c= (L~ f) ` by SUBSET_1:23; ::_thesis: verum
end;
theorem Th34: :: JORDAN14:34
for C being Simple_closed_curve
for n, m being Element of NAT st n is_sufficiently_large_for C & n <= m holds
L~ (Span (C,m)) c= Cl (LeftComp (Span (C,n)))
proof
let C be Simple_closed_curve; ::_thesis: for n, m being Element of NAT st n is_sufficiently_large_for C & n <= m holds
L~ (Span (C,m)) c= Cl (LeftComp (Span (C,n)))
let i, j be Element of NAT ; ::_thesis: ( i is_sufficiently_large_for C & i <= j implies L~ (Span (C,j)) c= Cl (LeftComp (Span (C,i))) )
assume that
A1: i is_sufficiently_large_for C and
A2: i <= j and
A3: not L~ (Span (C,j)) c= Cl (LeftComp (Span (C,i))) ; ::_thesis: contradiction
A4: j is_sufficiently_large_for C by A1, A2, Th28;
then A5: Span (C,j) is_sequence_on Gauge (C,j) by JORDAN13:def_1;
set G = Gauge (C,j);
set f = Span (C,j);
consider p being Point of (TOP-REAL 2) such that
A6: p in L~ (Span (C,j)) and
A7: not p in Cl (LeftComp (Span (C,i))) by A3, SUBSET_1:2;
consider i1 being Element of NAT such that
A8: 1 <= i1 and
A9: i1 + 1 <= len (Span (C,j)) and
A10: p in LSeg ((Span (C,j)),i1) by A6, SPPOL_2:13;
A11: i1 < len (Span (C,j)) by A9, NAT_1:13;
A12: Span (C,i) is_sequence_on Gauge (C,i) by A1, JORDAN13:def_1;
now__::_thesis:_left_cell_((Span_(C,j)),i1,(Gauge_(C,j)))_c=_Cl_(RightComp_(Span_(C,i)))
ex i2, j2 being Element of NAT st
( 1 <= i2 & i2 + 1 <= len (Gauge (C,i)) & 1 <= j2 & j2 + 1 <= width (Gauge (C,i)) & left_cell ((Span (C,j)),i1,(Gauge (C,j))) c= cell ((Gauge (C,i)),i2,j2) )
proof
A13: 1 <= i1 + 1 by NAT_1:11;
then A14: i1 + 1 in dom (Span (C,j)) by A9, FINSEQ_3:25;
then consider i5, j5 being Element of NAT such that
A15: [i5,j5] in Indices (Gauge (C,j)) and
A16: (Span (C,j)) /. (i1 + 1) = (Gauge (C,j)) * (i5,j5) by A5, GOBOARD1:def_9;
A17: 1 <= i5 by A15, MATRIX_1:38;
A18: j5 <= width (Gauge (C,j)) by A15, MATRIX_1:38;
A19: i5 <= len (Gauge (C,j)) by A15, MATRIX_1:38;
A20: 1 <= j5 by A15, MATRIX_1:38;
A21: i1 in dom (Span (C,j)) by A8, A11, FINSEQ_3:25;
then consider i4, j4 being Element of NAT such that
A22: [i4,j4] in Indices (Gauge (C,j)) and
A23: (Span (C,j)) /. i1 = (Gauge (C,j)) * (i4,j4) by A5, GOBOARD1:def_9;
A24: 1 <= i4 by A22, MATRIX_1:38;
(abs (i4 - i5)) + (abs (j4 - j5)) = 1 by A5, A21, A22, A23, A14, A15, A16, GOBOARD1:def_9;
then A25: ( ( abs (i4 - i5) = 1 & j4 = j5 ) or ( abs (j4 - j5) = 1 & i4 = i5 ) ) by SEQM_3:42;
A26: 1 <= j4 by A22, MATRIX_1:38;
left_cell ((Span (C,j)),i1,(Gauge (C,j))) = left_cell ((Span (C,j)),i1,(Gauge (C,j))) ;
then A27: ( ( i4 = i5 & j4 + 1 = j5 & left_cell ((Span (C,j)),i1,(Gauge (C,j))) = cell ((Gauge (C,j)),(i4 -' 1),j4) ) or ( i4 + 1 = i5 & j4 = j5 & left_cell ((Span (C,j)),i1,(Gauge (C,j))) = cell ((Gauge (C,j)),i4,j4) ) or ( i4 = i5 + 1 & j4 = j5 & left_cell ((Span (C,j)),i1,(Gauge (C,j))) = cell ((Gauge (C,j)),i5,(j5 -' 1)) ) or ( i4 = i5 & j4 = j5 + 1 & left_cell ((Span (C,j)),i1,(Gauge (C,j))) = cell ((Gauge (C,j)),i4,j5) ) ) by A5, A8, A9, A22, A23, A15, A16, GOBRD13:def_3;
A28: j4 <= width (Gauge (C,j)) by A22, MATRIX_1:38;
A29: i4 <= len (Gauge (C,j)) by A22, MATRIX_1:38;
percases ( ( i4 = i5 & j4 + 1 = j5 ) or ( i4 + 1 = i5 & j4 = j5 ) or ( i4 = i5 + 1 & j4 = j5 ) or ( i4 = i5 & j4 = j5 + 1 ) ) by A25, SEQM_3:41;
supposeA30: ( i4 = i5 & j4 + 1 = j5 ) ; ::_thesis: ex i2, j2 being Element of NAT st
( 1 <= i2 & i2 + 1 <= len (Gauge (C,i)) & 1 <= j2 & j2 + 1 <= width (Gauge (C,i)) & left_cell ((Span (C,j)),i1,(Gauge (C,j))) c= cell ((Gauge (C,i)),i2,j2) )
1 < i4 by A1, A2, A8, A11, A22, A23, Th22, Th28;
then 1 + 1 <= i4 by NAT_1:13;
then A31: 1 <= i4 -' 1 by JORDAN5B:2;
(i4 -' 1) + 1 = i4 by A24, XREAL_1:235;
hence ex i2, j2 being Element of NAT st
( 1 <= i2 & i2 + 1 <= len (Gauge (C,i)) & 1 <= j2 & j2 + 1 <= width (Gauge (C,i)) & left_cell ((Span (C,j)),i1,(Gauge (C,j))) c= cell ((Gauge (C,i)),i2,j2) ) by A2, A29, A26, A18, A27, A30, A31, JORDAN1H:38; ::_thesis: verum
end;
supposeA32: ( i4 + 1 = i5 & j4 = j5 ) ; ::_thesis: ex i2, j2 being Element of NAT st
( 1 <= i2 & i2 + 1 <= len (Gauge (C,i)) & 1 <= j2 & j2 + 1 <= width (Gauge (C,i)) & left_cell ((Span (C,j)),i1,(Gauge (C,j))) c= cell ((Gauge (C,i)),i2,j2) )
j4 < width (Gauge (C,j)) by A1, A2, A8, A11, A22, A23, Th25, Th28;
then j4 + 1 <= width (Gauge (C,j)) by NAT_1:13;
hence ex i2, j2 being Element of NAT st
( 1 <= i2 & i2 + 1 <= len (Gauge (C,i)) & 1 <= j2 & j2 + 1 <= width (Gauge (C,i)) & left_cell ((Span (C,j)),i1,(Gauge (C,j))) c= cell ((Gauge (C,i)),i2,j2) ) by A2, A24, A26, A19, A27, A32, JORDAN1H:38; ::_thesis: verum
end;
supposeA33: ( i4 = i5 + 1 & j4 = j5 ) ; ::_thesis: ex i2, j2 being Element of NAT st
( 1 <= i2 & i2 + 1 <= len (Gauge (C,i)) & 1 <= j2 & j2 + 1 <= width (Gauge (C,i)) & left_cell ((Span (C,j)),i1,(Gauge (C,j))) c= cell ((Gauge (C,i)),i2,j2) )
1 < j5 by A1, A2, A9, A13, A15, A16, Th24, Th28;
then 1 + 1 <= j5 by NAT_1:13;
then A34: 1 <= j5 -' 1 by JORDAN5B:2;
(j5 -' 1) + 1 = j5 by A20, XREAL_1:235;
hence ex i2, j2 being Element of NAT st
( 1 <= i2 & i2 + 1 <= len (Gauge (C,i)) & 1 <= j2 & j2 + 1 <= width (Gauge (C,i)) & left_cell ((Span (C,j)),i1,(Gauge (C,j))) c= cell ((Gauge (C,i)),i2,j2) ) by A2, A29, A17, A18, A27, A33, A34, JORDAN1H:38; ::_thesis: verum
end;
supposeA35: ( i4 = i5 & j4 = j5 + 1 ) ; ::_thesis: ex i2, j2 being Element of NAT st
( 1 <= i2 & i2 + 1 <= len (Gauge (C,i)) & 1 <= j2 & j2 + 1 <= width (Gauge (C,i)) & left_cell ((Span (C,j)),i1,(Gauge (C,j))) c= cell ((Gauge (C,i)),i2,j2) )
i4 < len (Gauge (C,j)) by A1, A2, A8, A11, A22, A23, Th23, Th28;
then i4 + 1 <= len (Gauge (C,j)) by NAT_1:13;
hence ex i2, j2 being Element of NAT st
( 1 <= i2 & i2 + 1 <= len (Gauge (C,i)) & 1 <= j2 & j2 + 1 <= width (Gauge (C,i)) & left_cell ((Span (C,j)),i1,(Gauge (C,j))) c= cell ((Gauge (C,i)),i2,j2) ) by A2, A24, A28, A20, A27, A35, JORDAN1H:38; ::_thesis: verum
end;
end;
end;
then consider i2, j2 being Element of NAT such that
1 <= i2 and
A36: i2 + 1 <= len (Gauge (C,i)) and
1 <= j2 and
A37: j2 + 1 <= width (Gauge (C,i)) and
A38: left_cell ((Span (C,j)),i1,(Gauge (C,j))) c= cell ((Gauge (C,i)),i2,j2) ;
A39: j2 < width (Gauge (C,i)) by A37, NAT_1:13;
A40: LeftComp (Span (C,i)) is_a_component_of (L~ (Span (C,i))) ` by GOBOARD9:def_1;
A41: (Cl (RightComp (Span (C,i)))) \/ (LeftComp (Span (C,i))) = ((L~ (Span (C,i))) \/ (RightComp (Span (C,i)))) \/ (LeftComp (Span (C,i))) by GOBRD14:21
.= the carrier of (TOP-REAL 2) by GOBRD14:15 ;
assume not left_cell ((Span (C,j)),i1,(Gauge (C,j))) c= Cl (RightComp (Span (C,i))) ; ::_thesis: contradiction
then not cell ((Gauge (C,i)),i2,j2) c= Cl (RightComp (Span (C,i))) by A38, XBOOLE_1:1;
then A42: cell ((Gauge (C,i)),i2,j2) meets LeftComp (Span (C,i)) by A41, XBOOLE_1:73;
A43: i2 < len (Gauge (C,i)) by A36, NAT_1:13;
then cell ((Gauge (C,i)),i2,j2) = Cl (Int (cell ((Gauge (C,i)),i2,j2))) by A39, GOBRD11:35;
then A44: Int (cell ((Gauge (C,i)),i2,j2)) meets LeftComp (Span (C,i)) by A42, TSEP_1:36;
A45: Int (left_cell ((Span (C,j)),i1,(Gauge (C,j)))) c= Int (cell ((Gauge (C,i)),i2,j2)) by A38, TOPS_1:19;
A46: Int (cell ((Gauge (C,i)),i2,j2)) is convex by A43, A39, GOBOARD9:17;
Int (cell ((Gauge (C,i)),i2,j2)) c= (L~ (Span (C,i))) ` by A12, A43, A39, Th33;
then Int (cell ((Gauge (C,i)),i2,j2)) c= LeftComp (Span (C,i)) by A44, A40, A46, GOBOARD9:4;
then Int (left_cell ((Span (C,j)),i1,(Gauge (C,j)))) c= LeftComp (Span (C,i)) by A45, XBOOLE_1:1;
then Cl (Int (left_cell ((Span (C,j)),i1,(Gauge (C,j))))) c= Cl (LeftComp (Span (C,i))) by PRE_TOPC:19;
then A47: left_cell ((Span (C,j)),i1,(Gauge (C,j))) c= Cl (LeftComp (Span (C,i))) by A5, A8, A9, JORDAN9:11;
LSeg ((Span (C,j)),i1) c= left_cell ((Span (C,j)),i1,(Gauge (C,j))) by A5, A8, A9, JORDAN1H:20;
then LSeg ((Span (C,j)),i1) c= Cl (LeftComp (Span (C,i))) by A47, XBOOLE_1:1;
hence contradiction by A7, A10; ::_thesis: verum
end;
then A48: C meets Cl (RightComp (Span (C,i))) by A4, A8, A9, Th7, XBOOLE_1:63;
A49: Cl (RightComp (Span (C,i))) = (RightComp (Span (C,i))) \/ (L~ (Span (C,i))) by GOBRD14:21;
C misses L~ (Span (C,i)) by A1, Th8;
then A50: C meets RightComp (Span (C,i)) by A48, A49, XBOOLE_1:70;
C meets C ;
then A51: C meets LeftComp (Span (C,i)) by A1, Th11, XBOOLE_1:63;
reconsider D = (L~ (Span (C,i))) ` as Subset of (TOP-REAL 2) ;
D = (RightComp (Span (C,i))) \/ (LeftComp (Span (C,i))) by GOBRD12:10;
then A52: LeftComp (Span (C,i)) c= D by XBOOLE_1:7;
C c= LeftComp (Span (C,i)) by A1, Th11;
then A53: C c= D by A52, XBOOLE_1:1;
A54: LeftComp (Span (C,i)) is_a_component_of D by GOBOARD9:def_1;
RightComp (Span (C,i)) is_a_component_of D by GOBOARD9:def_2;
hence contradiction by A50, A53, A54, A51, JORDAN9:1, SPRECT_4:6; ::_thesis: verum
end;
theorem Th35: :: JORDAN14:35
for C being Simple_closed_curve
for n, m being Element of NAT st n is_sufficiently_large_for C & n <= m holds
RightComp (Span (C,n)) c= RightComp (Span (C,m))
proof
let C be Simple_closed_curve; ::_thesis: for n, m being Element of NAT st n is_sufficiently_large_for C & n <= m holds
RightComp (Span (C,n)) c= RightComp (Span (C,m))
let n, m be Element of NAT ; ::_thesis: ( n is_sufficiently_large_for C & n <= m implies RightComp (Span (C,n)) c= RightComp (Span (C,m)) )
assume that
A1: n is_sufficiently_large_for C and
A2: n <= m ; ::_thesis: RightComp (Span (C,n)) c= RightComp (Span (C,m))
A3: L~ (Span (C,n)) misses RightComp (Span (C,n)) by SPRECT_3:25;
A4: RightComp (Span (C,n)) misses LeftComp (Span (C,n)) by GOBRD14:14;
Cl (LeftComp (Span (C,n))) = (LeftComp (Span (C,n))) \/ (L~ (Span (C,n))) by GOBRD14:22;
then Cl (LeftComp (Span (C,n))) misses RightComp (Span (C,n)) by A3, A4, XBOOLE_1:70;
then L~ (Span (C,m)) misses RightComp (Span (C,n)) by A1, A2, Th34, XBOOLE_1:63;
then A5: RightComp (Span (C,n)) c= (L~ (Span (C,m))) ` by SUBSET_1:23;
A6: RightComp (Span (C,m)) is_a_component_of (L~ (Span (C,m))) ` by GOBOARD9:def_2;
RightComp (Span (C,n)) meets RightComp (Span (C,m)) by A1, A2, Th32;
hence RightComp (Span (C,n)) c= RightComp (Span (C,m)) by A6, A5, GOBOARD9:4; ::_thesis: verum
end;
theorem :: JORDAN14:36
for C being Simple_closed_curve
for n, m being Element of NAT st n is_sufficiently_large_for C & n <= m holds
LeftComp (Span (C,m)) c= LeftComp (Span (C,n))
proof
let C be Simple_closed_curve; ::_thesis: for n, m being Element of NAT st n is_sufficiently_large_for C & n <= m holds
LeftComp (Span (C,m)) c= LeftComp (Span (C,n))
let n, m be Element of NAT ; ::_thesis: ( n is_sufficiently_large_for C & n <= m implies LeftComp (Span (C,m)) c= LeftComp (Span (C,n)) )
assume that
A1: n is_sufficiently_large_for C and
A2: n <= m ; ::_thesis: LeftComp (Span (C,m)) c= LeftComp (Span (C,n))
A3: (Cl (RightComp (Span (C,n)))) ` = LeftComp (Span (C,n)) by JORDAN1H:43;
A4: (Cl (RightComp (Span (C,m)))) ` = LeftComp (Span (C,m)) by JORDAN1H:43;
Cl (RightComp (Span (C,n))) c= Cl (RightComp (Span (C,m))) by A1, A2, Th35, PRE_TOPC:19;
hence LeftComp (Span (C,m)) c= LeftComp (Span (C,n)) by A3, A4, SUBSET_1:12; ::_thesis: verum
end;