:: JORDAN1H semantic presentation
begin
registration
let D be non empty with_non-empty_element set ;
cluster non empty Relation-like non-empty NAT -defined D * -valued Function-like finite FinSequence-like FinSubsequence-like Function-yielding V81() FinSequence-yielding finite-support for FinSequence of D * ;
existence
ex b1 being FinSequence of D * st
( not b1 is empty & b1 is non-empty )
proof
consider X being non empty set such that
A1: X in D by SETFAM_1:def_10;
A2: rng <*<*X*>*> = {<*X*>} by FINSEQ_1:39;
<*X*> in D * by A1, FUNCT_7:18;
then rng <*<*X*>*> c= D * by A2, ZFMISC_1:31;
then reconsider F = <*<*X*>*> as FinSequence of D * by FINSEQ_1:def_4;
take F ; ::_thesis: ( not F is empty & F is non-empty )
thus not F is empty ; ::_thesis: F is non-empty
assume {} in rng F ; :: according to RELAT_1:def_9 ::_thesis: contradiction
hence contradiction by A2; ::_thesis: verum
end;
end;
registration
let F be non-empty Function-yielding Function;
cluster rngs F -> non-empty ;
coherence
rngs F is non-empty
proof
now__::_thesis:_for_n_being_set_st_n_in_dom_(rngs_F)_holds_
not_(rngs_F)_._n_is_empty
let n be set ; ::_thesis: ( n in dom (rngs F) implies not (rngs F) . n is empty )
assume n in dom (rngs F) ; ::_thesis: not (rngs F) . n is empty
then n in dom F by FUNCT_6:60;
then ( (rngs F) . n = rng (F . n) & not F . n is empty ) by FUNCT_1:def_9, FUNCT_6:22;
hence not (rngs F) . n is empty ; ::_thesis: verum
end;
hence rngs F is non-empty by FUNCT_1:def_9; ::_thesis: verum
end;
end;
theorem Th1: :: JORDAN1H:1
for p, q being Point of (TOP-REAL 2) st p <> q holds
p in Cl ((LSeg (p,q)) \ {p,q})
proof
let p, q be Point of (TOP-REAL 2); ::_thesis: ( p <> q implies p in Cl ((LSeg (p,q)) \ {p,q}) )
assume A1: p <> q ; ::_thesis: p in Cl ((LSeg (p,q)) \ {p,q})
for G being Subset of (TOP-REAL 2) st G is open & p in G holds
(LSeg (p,q)) \ {p,q} meets G
proof
reconsider x = p, y = q as Point of (Euclid 2) by TOPREAL3:8;
let G be Subset of (TOP-REAL 2); ::_thesis: ( G is open & p in G implies (LSeg (p,q)) \ {p,q} meets G )
assume that
A2: G is open and
A3: p in G ; ::_thesis: (LSeg (p,q)) \ {p,q} meets G
A4: TopStruct(# the carrier of (TOP-REAL 2), the topology of (TOP-REAL 2) #) = TopSpaceMetr (Euclid 2) by EUCLID:def_8;
then reconsider P = G as Subset of (TopSpaceMetr (Euclid 2)) ;
P is open by A2, A4, PRE_TOPC:30;
then consider r being real number such that
A5: r > 0 and
A6: Ball (x,r) c= P by A3, TOPMETR:15;
reconsider r = r as Real by XREAL_0:def_1;
A7: r / 2 > 0 by A5, XREAL_1:139;
set t = min ((r / 2),((dist (x,y)) / 2));
set s = (min ((r / 2),((dist (x,y)) / 2))) / (dist (x,y));
set pp = ((1 - ((min ((r / 2),((dist (x,y)) / 2))) / (dist (x,y)))) * p) + (((min ((r / 2),((dist (x,y)) / 2))) / (dist (x,y))) * q);
reconsider z = ((1 - ((min ((r / 2),((dist (x,y)) / 2))) / (dist (x,y)))) * p) + (((min ((r / 2),((dist (x,y)) / 2))) / (dist (x,y))) * q) as Point of (Euclid 2) by TOPREAL3:8;
reconsider x9 = x, y9 = y, z9 = z as Element of REAL 2 ;
reconsider a = x9, b = y9 as Element of 2 -tuples_on REAL ;
reconsider u = a - b as Element of REAL 2 ;
A8: 0 < dist (x,y) by A1, METRIC_1:7;
then 0 < (dist (x,y)) / 2 by XREAL_1:139;
then A9: 0 < min ((r / 2),((dist (x,y)) / 2)) by A7, XXREAL_0:21;
dist (x,z) = |.(x9 - z9).| by SPPOL_1:5
.= |.((a - ((1 - ((min ((r / 2),((dist (x,y)) / 2))) / (dist (x,y)))) * a)) - (((min ((r / 2),((dist (x,y)) / 2))) / (dist (x,y))) * b)).| by RVSUM_1:39
.= |.(((1 * a) - ((1 - ((min ((r / 2),((dist (x,y)) / 2))) / (dist (x,y)))) * a)) - (((min ((r / 2),((dist (x,y)) / 2))) / (dist (x,y))) * b)).| by RVSUM_1:52
.= |.(((1 * a) + (((- 1) * (1 - ((min ((r / 2),((dist (x,y)) / 2))) / (dist (x,y))))) * a)) - (((min ((r / 2),((dist (x,y)) / 2))) / (dist (x,y))) * b)).| by RVSUM_1:49
.= |.(((1 + (- (1 - ((min ((r / 2),((dist (x,y)) / 2))) / (dist (x,y)))))) * a) - (((min ((r / 2),((dist (x,y)) / 2))) / (dist (x,y))) * b)).| by RVSUM_1:50
.= |.((((min ((r / 2),((dist (x,y)) / 2))) / (dist (x,y))) * a) + (((- 1) * ((min ((r / 2),((dist (x,y)) / 2))) / (dist (x,y)))) * b)).| by RVSUM_1:49
.= |.((((min ((r / 2),((dist (x,y)) / 2))) / (dist (x,y))) * a) + (((min ((r / 2),((dist (x,y)) / 2))) / (dist (x,y))) * ((- 1) * b))).| by RVSUM_1:49
.= |.(((min ((r / 2),((dist (x,y)) / 2))) / (dist (x,y))) * (a + ((- 1) * b))).| by RVSUM_1:51
.= |.(((min ((r / 2),((dist (x,y)) / 2))) / (dist (x,y))) * (a + (- b))).|
.= |.(((min ((r / 2),((dist (x,y)) / 2))) / (dist (x,y))) * (a - b)).|
.= (abs ((min ((r / 2),((dist (x,y)) / 2))) / (dist (x,y)))) * |.u.| by EUCLID:11
.= ((min ((r / 2),((dist (x,y)) / 2))) / (dist (x,y))) * |.(a - b).| by A8, A9, ABSVALUE:def_1
.= ((min ((r / 2),((dist (x,y)) / 2))) / (dist (x,y))) * (dist (x,y)) by SPPOL_1:5
.= min ((r / 2),((dist (x,y)) / 2)) by A8, XCMPLX_1:87 ;
then A10: dist (x,z) <= r / 2 by XXREAL_0:17;
r / 2 < r / 1 by A5, XREAL_1:76;
then dist (x,z) < r by A10, XXREAL_0:2;
then A11: z in Ball (x,r) by METRIC_1:11;
A12: ((1 - ((min ((r / 2),((dist (x,y)) / 2))) / (dist (x,y)))) * p) + (((min ((r / 2),((dist (x,y)) / 2))) / (dist (x,y))) * p) = ((1 - ((min ((r / 2),((dist (x,y)) / 2))) / (dist (x,y)))) + ((min ((r / 2),((dist (x,y)) / 2))) / (dist (x,y)))) * p by EUCLID:33
.= p by EUCLID:29 ;
( min ((r / 2),((dist (x,y)) / 2)) <= (dist (x,y)) / 2 & (dist (x,y)) / 2 < (dist (x,y)) / 1 ) by A8, XREAL_1:76, XXREAL_0:17;
then A13: min ((r / 2),((dist (x,y)) / 2)) < dist (x,y) by XXREAL_0:2;
then (min ((r / 2),((dist (x,y)) / 2))) / (dist (x,y)) < 1 by A9, XREAL_1:189;
then A14: ((1 - ((min ((r / 2),((dist (x,y)) / 2))) / (dist (x,y)))) * p) + (((min ((r / 2),((dist (x,y)) / 2))) / (dist (x,y))) * q) in LSeg (p,q) by A8, A9;
A15: ((1 - ((min ((r / 2),((dist (x,y)) / 2))) / (dist (x,y)))) * q) + (((min ((r / 2),((dist (x,y)) / 2))) / (dist (x,y))) * q) = ((1 - ((min ((r / 2),((dist (x,y)) / 2))) / (dist (x,y)))) + ((min ((r / 2),((dist (x,y)) / 2))) / (dist (x,y)))) * q by EUCLID:33
.= q by EUCLID:29 ;
A16: 1 - ((min ((r / 2),((dist (x,y)) / 2))) / (dist (x,y))) <> 0 by A9, A13, XREAL_1:189;
A17: now__::_thesis:_not_((1_-_((min_((r_/_2),((dist_(x,y))_/_2)))_/_(dist_(x,y))))_*_p)_+_(((min_((r_/_2),((dist_(x,y))_/_2)))_/_(dist_(x,y)))_*_q)_=_q
assume ((1 - ((min ((r / 2),((dist (x,y)) / 2))) / (dist (x,y)))) * p) + (((min ((r / 2),((dist (x,y)) / 2))) / (dist (x,y))) * q) = q ; ::_thesis: contradiction
then (1 - ((min ((r / 2),((dist (x,y)) / 2))) / (dist (x,y)))) * q = (((1 - ((min ((r / 2),((dist (x,y)) / 2))) / (dist (x,y)))) * p) + (((min ((r / 2),((dist (x,y)) / 2))) / (dist (x,y))) * q)) - (((min ((r / 2),((dist (x,y)) / 2))) / (dist (x,y))) * q) by A15, EUCLID:48
.= (1 - ((min ((r / 2),((dist (x,y)) / 2))) / (dist (x,y)))) * p by EUCLID:48 ;
hence contradiction by A1, A16, EUCLID:34; ::_thesis: verum
end;
A18: 0 < (min ((r / 2),((dist (x,y)) / 2))) / (dist (x,y)) by A8, A9, XREAL_1:139;
now__::_thesis:_not_((1_-_((min_((r_/_2),((dist_(x,y))_/_2)))_/_(dist_(x,y))))_*_p)_+_(((min_((r_/_2),((dist_(x,y))_/_2)))_/_(dist_(x,y)))_*_q)_=_p
assume ((1 - ((min ((r / 2),((dist (x,y)) / 2))) / (dist (x,y)))) * p) + (((min ((r / 2),((dist (x,y)) / 2))) / (dist (x,y))) * q) = p ; ::_thesis: contradiction
then ((min ((r / 2),((dist (x,y)) / 2))) / (dist (x,y))) * p = (((1 - ((min ((r / 2),((dist (x,y)) / 2))) / (dist (x,y)))) * p) + (((min ((r / 2),((dist (x,y)) / 2))) / (dist (x,y))) * q)) - ((1 - ((min ((r / 2),((dist (x,y)) / 2))) / (dist (x,y)))) * p) by A12, EUCLID:48
.= ((min ((r / 2),((dist (x,y)) / 2))) / (dist (x,y))) * q by EUCLID:48 ;
hence contradiction by A1, A18, EUCLID:34; ::_thesis: verum
end;
then not ((1 - ((min ((r / 2),((dist (x,y)) / 2))) / (dist (x,y)))) * p) + (((min ((r / 2),((dist (x,y)) / 2))) / (dist (x,y))) * q) in {p,q} by A17, TARSKI:def_2;
then ((1 - ((min ((r / 2),((dist (x,y)) / 2))) / (dist (x,y)))) * p) + (((min ((r / 2),((dist (x,y)) / 2))) / (dist (x,y))) * q) in (LSeg (p,q)) \ {p,q} by A14, XBOOLE_0:def_5;
hence (LSeg (p,q)) \ {p,q} meets G by A6, A11, XBOOLE_0:3; ::_thesis: verum
end;
hence p in Cl ((LSeg (p,q)) \ {p,q}) by TOPS_1:12; ::_thesis: verum
end;
theorem Th2: :: JORDAN1H:2
for p, q being Point of (TOP-REAL 2) st p <> q holds
Cl ((LSeg (p,q)) \ {p,q}) = LSeg (p,q)
proof
let p, q be Point of (TOP-REAL 2); ::_thesis: ( p <> q implies Cl ((LSeg (p,q)) \ {p,q}) = LSeg (p,q) )
assume A1: p <> q ; ::_thesis: Cl ((LSeg (p,q)) \ {p,q}) = LSeg (p,q)
Cl ((LSeg (p,q)) \ {p,q}) c= Cl (LSeg (p,q)) by PRE_TOPC:19, XBOOLE_1:36;
hence Cl ((LSeg (p,q)) \ {p,q}) c= LSeg (p,q) by PRE_TOPC:22; :: according to XBOOLE_0:def_10 ::_thesis: LSeg (p,q) c= Cl ((LSeg (p,q)) \ {p,q})
let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in LSeg (p,q) or e in Cl ((LSeg (p,q)) \ {p,q}) )
( p in LSeg (p,q) & q in LSeg (p,q) ) by RLTOPSP1:68;
then {p,q} c= LSeg (p,q) by ZFMISC_1:32;
then A2: LSeg (p,q) = ((LSeg (p,q)) \ {p,q}) \/ {p,q} by XBOOLE_1:45;
assume e in LSeg (p,q) ; ::_thesis: e in Cl ((LSeg (p,q)) \ {p,q})
then A3: ( e in (LSeg (p,q)) \ {p,q} or e in {p,q} ) by A2, XBOOLE_0:def_3;
percases ( e in (LSeg (p,q)) \ {p,q} or e = p or e = q ) by A3, TARSKI:def_2;
supposeA4: e in (LSeg (p,q)) \ {p,q} ; ::_thesis: e in Cl ((LSeg (p,q)) \ {p,q})
(LSeg (p,q)) \ {p,q} c= Cl ((LSeg (p,q)) \ {p,q}) by PRE_TOPC:18;
hence e in Cl ((LSeg (p,q)) \ {p,q}) by A4; ::_thesis: verum
end;
suppose ( e = p or e = q ) ; ::_thesis: e in Cl ((LSeg (p,q)) \ {p,q})
hence e in Cl ((LSeg (p,q)) \ {p,q}) by A1, Th1; ::_thesis: verum
end;
end;
end;
theorem :: JORDAN1H:3
for S being Subset of (TOP-REAL 2)
for p, q being Point of (TOP-REAL 2) st p <> q & (LSeg (p,q)) \ {p,q} c= S holds
LSeg (p,q) c= Cl S
proof
let S be Subset of (TOP-REAL 2); ::_thesis: for p, q being Point of (TOP-REAL 2) st p <> q & (LSeg (p,q)) \ {p,q} c= S holds
LSeg (p,q) c= Cl S
let p, q be Point of (TOP-REAL 2); ::_thesis: ( p <> q & (LSeg (p,q)) \ {p,q} c= S implies LSeg (p,q) c= Cl S )
assume A1: p <> q ; ::_thesis: ( not (LSeg (p,q)) \ {p,q} c= S or LSeg (p,q) c= Cl S )
assume (LSeg (p,q)) \ {p,q} c= S ; ::_thesis: LSeg (p,q) c= Cl S
then Cl ((LSeg (p,q)) \ {p,q}) c= Cl S by PRE_TOPC:19;
hence LSeg (p,q) c= Cl S by A1, Th2; ::_thesis: verum
end;
begin
definition
func RealOrd -> Relation of REAL equals :: JORDAN1H:def 1
{ [r,s] where r, s is Real : r <= s } ;
coherence
{ [r,s] where r, s is Real : r <= s } is Relation of REAL
proof
set R = { [r,s] where r, s is Real : r <= s } ;
{ [r,s] where r, s is Real : r <= s } c= [:REAL,REAL:]
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { [r,s] where r, s is Real : r <= s } or x in [:REAL,REAL:] )
assume x in { [r,s] where r, s is Real : r <= s } ; ::_thesis: x in [:REAL,REAL:]
then ex r, s being Real st
( x = [r,s] & r <= s ) ;
hence x in [:REAL,REAL:] by ZFMISC_1:87; ::_thesis: verum
end;
hence { [r,s] where r, s is Real : r <= s } is Relation of REAL ; ::_thesis: verum
end;
end;
:: deftheorem defines RealOrd JORDAN1H:def_1_:_
RealOrd = { [r,s] where r, s is Real : r <= s } ;
theorem Th4: :: JORDAN1H:4
for r, s being Real st [r,s] in RealOrd holds
r <= s
proof
let r, s be Real; ::_thesis: ( [r,s] in RealOrd implies r <= s )
hereby ::_thesis: verum
assume [r,s] in RealOrd ; ::_thesis: r <= s
then consider r1, s1 being Real such that
A1: [r,s] = [r1,s1] and
A2: r1 <= s1 ;
r = r1 by A1, XTUPLE_0:1;
hence r <= s by A1, A2, XTUPLE_0:1; ::_thesis: verum
end;
end;
Lm1: RealOrd is_reflexive_in REAL
proof
let x be set ; :: according to RELAT_2:def_1 ::_thesis: ( not x in REAL or [x,x] in RealOrd )
assume x in REAL ; ::_thesis: [x,x] in RealOrd
then reconsider x = x as Element of REAL ;
x <= x ;
hence [x,x] in RealOrd ; ::_thesis: verum
end;
Lm2: RealOrd is_antisymmetric_in REAL
proof
let x, y be set ; :: according to RELAT_2:def_4 ::_thesis: ( not x in REAL or not y in REAL or not [x,y] in RealOrd or not [y,x] in RealOrd or x = y )
assume that
A1: ( x in REAL & y in REAL ) and
A2: ( [x,y] in RealOrd & [y,x] in RealOrd ) ; ::_thesis: x = y
reconsider x = x, y = y as Element of REAL by A1;
( x <= y & y <= x ) by A2, Th4;
hence x = y by XXREAL_0:1; ::_thesis: verum
end;
Lm3: RealOrd is_transitive_in REAL
proof
let x, y, z be set ; :: according to RELAT_2:def_8 ::_thesis: ( not x in REAL or not y in REAL or not z in REAL or not [x,y] in RealOrd or not [y,z] in RealOrd or [x,z] in RealOrd )
assume that
A1: ( x in REAL & y in REAL & z in REAL ) and
A2: ( [x,y] in RealOrd & [y,z] in RealOrd ) ; ::_thesis: [x,z] in RealOrd
reconsider x = x, y = y, z = z as Element of REAL by A1;
( x <= y & y <= z ) by A2, Th4;
then x <= z by XXREAL_0:2;
hence [x,z] in RealOrd ; ::_thesis: verum
end;
Lm4: RealOrd is_connected_in REAL
proof
let x, y be set ; :: according to RELAT_2:def_6 ::_thesis: ( not x in REAL or not y in REAL or x = y or [x,y] in RealOrd or [y,x] in RealOrd )
assume ( x in REAL & y in REAL ) ; ::_thesis: ( x = y or [x,y] in RealOrd or [y,x] in RealOrd )
then reconsider x = x, y = y as Element of REAL ;
( x <= y or y <= x ) ;
hence ( x = y or [x,y] in RealOrd or [y,x] in RealOrd ) ; ::_thesis: verum
end;
theorem Th5: :: JORDAN1H:5
field RealOrd = REAL
proof
field RealOrd c= REAL \/ REAL by RELSET_1:8;
hence field RealOrd c= REAL ; :: according to XBOOLE_0:def_10 ::_thesis: REAL c= field RealOrd
thus REAL c= field RealOrd by Lm1, PARTIT_2:8; ::_thesis: verum
end;
registration
cluster RealOrd -> total reflexive antisymmetric transitive being_linear-order ;
coherence
( RealOrd is total & RealOrd is reflexive & RealOrd is antisymmetric & RealOrd is transitive & RealOrd is being_linear-order )
proof
REAL c= dom RealOrd
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in REAL or x in dom RealOrd )
assume x in REAL ; ::_thesis: x in dom RealOrd
then reconsider x = x as Element of REAL ;
[x,x] in RealOrd ;
hence x in dom RealOrd by XTUPLE_0:def_12; ::_thesis: verum
end;
then dom RealOrd = REAL by XBOOLE_0:def_10;
hence RealOrd is total by PARTFUN1:def_2; ::_thesis: ( RealOrd is reflexive & RealOrd is antisymmetric & RealOrd is transitive & RealOrd is being_linear-order )
thus RealOrd is reflexive by Lm1, Th5, RELAT_2:def_9; ::_thesis: ( RealOrd is antisymmetric & RealOrd is transitive & RealOrd is being_linear-order )
thus RealOrd is antisymmetric by Lm2, Th5, RELAT_2:def_12; ::_thesis: ( RealOrd is transitive & RealOrd is being_linear-order )
thus RealOrd is transitive by Lm3, Th5, RELAT_2:def_16; ::_thesis: RealOrd is being_linear-order
thus RealOrd is_reflexive_in field RealOrd by Lm1, Th5; :: according to RELAT_2:def_9,ORDERS_1:def_5 ::_thesis: ( RealOrd is transitive & RealOrd is antisymmetric & RealOrd is connected )
thus RealOrd is_transitive_in field RealOrd by Lm3, Th5; :: according to RELAT_2:def_16 ::_thesis: ( RealOrd is antisymmetric & RealOrd is connected )
thus RealOrd is_antisymmetric_in field RealOrd by Lm2, Th5; :: according to RELAT_2:def_12 ::_thesis: RealOrd is connected
thus RealOrd is_connected_in field RealOrd by Lm4, Th5; :: according to RELAT_2:def_14 ::_thesis: verum
end;
end;
theorem Th6: :: JORDAN1H:6
RealOrd linearly_orders REAL
proof
thus RealOrd is_reflexive_in REAL by Lm1; :: according to ORDERS_1:def_8 ::_thesis: ( RealOrd is_transitive_in REAL & RealOrd is_antisymmetric_in REAL & RealOrd is_connected_in REAL )
thus RealOrd is_transitive_in REAL by Lm3; ::_thesis: ( RealOrd is_antisymmetric_in REAL & RealOrd is_connected_in REAL )
thus RealOrd is_antisymmetric_in REAL by Lm2; ::_thesis: RealOrd is_connected_in REAL
thus RealOrd is_connected_in REAL by Lm4; ::_thesis: verum
end;
theorem Th7: :: JORDAN1H:7
for A being finite Subset of REAL holds SgmX (RealOrd,A) is increasing
proof
let A be finite Subset of REAL; ::_thesis: SgmX (RealOrd,A) is increasing
set IT = SgmX (RealOrd,A);
let n, m be Element of NAT ; :: according to SEQM_3:def_1 ::_thesis: ( not n in dom (SgmX (RealOrd,A)) or not m in dom (SgmX (RealOrd,A)) or m <= n or not (SgmX (RealOrd,A)) . m <= (SgmX (RealOrd,A)) . n )
assume that
A1: ( n in dom (SgmX (RealOrd,A)) & m in dom (SgmX (RealOrd,A)) ) and
A2: n < m ; ::_thesis: not (SgmX (RealOrd,A)) . m <= (SgmX (RealOrd,A)) . n
A3: RealOrd linearly_orders A by Th6, ORDERS_1:38;
( (SgmX (RealOrd,A)) /. n = (SgmX (RealOrd,A)) . n & (SgmX (RealOrd,A)) /. m = (SgmX (RealOrd,A)) . m ) by A1, PARTFUN1:def_6;
then [((SgmX (RealOrd,A)) . n),((SgmX (RealOrd,A)) . m)] in RealOrd by A1, A2, A3, PRE_POLY:def_2;
then A4: (SgmX (RealOrd,A)) . n <= (SgmX (RealOrd,A)) . m by Th4;
SgmX (RealOrd,A) is one-to-one by Th6, ORDERS_1:38, PRE_POLY:10;
then (SgmX (RealOrd,A)) . n <> (SgmX (RealOrd,A)) . m by A1, A2, FUNCT_1:def_4;
hence not (SgmX (RealOrd,A)) . m <= (SgmX (RealOrd,A)) . n by A4, XXREAL_0:1; ::_thesis: verum
end;
theorem Th8: :: JORDAN1H:8
for f being FinSequence of REAL
for A being finite Subset of REAL st A = rng f holds
SgmX (RealOrd,A) = Incr f
proof
let f be FinSequence of REAL ; ::_thesis: for A being finite Subset of REAL st A = rng f holds
SgmX (RealOrd,A) = Incr f
let A be finite Subset of REAL; ::_thesis: ( A = rng f implies SgmX (RealOrd,A) = Incr f )
assume A1: A = rng f ; ::_thesis: SgmX (RealOrd,A) = Incr f
reconsider F = SgmX (RealOrd,A) as increasing FinSequence of REAL by Th7;
RealOrd linearly_orders A by Th6, ORDERS_1:38;
then A2: rng (SgmX (RealOrd,A)) = rng f by A1, PRE_POLY:def_2;
len F = card (rng f) by A1, Th6, ORDERS_1:38, PRE_POLY:11;
hence SgmX (RealOrd,A) = Incr f by A2, SEQ_4:def_21; ::_thesis: verum
end;
registration
let A be finite Subset of REAL;
cluster SgmX (RealOrd,A) -> increasing ;
coherence
SgmX (RealOrd,A) is increasing by Th7;
end;
theorem Th9: :: JORDAN1H:9
for X being non empty set
for A being finite Subset of X
for R being being_linear-order Order of X holds len (SgmX (R,A)) = card A
proof
let X be non empty set ; ::_thesis: for A being finite Subset of X
for R being being_linear-order Order of X holds len (SgmX (R,A)) = card A
let A be finite Subset of X; ::_thesis: for R being being_linear-order Order of X holds len (SgmX (R,A)) = card A
let R be being_linear-order Order of X; ::_thesis: len (SgmX (R,A)) = card A
( field R = X & R linearly_orders field R ) by ORDERS_1:15, ORDERS_1:37;
hence len (SgmX (R,A)) = card A by ORDERS_1:38, PRE_POLY:11; ::_thesis: verum
end;
begin
theorem Th10: :: JORDAN1H:10
for f being FinSequence of (TOP-REAL 2) holds X_axis f = proj1 * f
proof
let f be FinSequence of (TOP-REAL 2); ::_thesis: X_axis f = proj1 * f
reconsider pf = proj1 * f as FinSequence of REAL by FINSEQ_2:32;
A1: len (X_axis f) = len f by GOBOARD1:def_1;
then A2: dom (X_axis f) = dom f by FINSEQ_3:29;
A3: for k being Nat st k in dom (X_axis f) holds
(X_axis f) . k = pf . k
proof
let k be Nat; ::_thesis: ( k in dom (X_axis f) implies (X_axis f) . k = pf . k )
assume A4: k in dom (X_axis f) ; ::_thesis: (X_axis f) . k = pf . k
A5: f /. k = f . k by A2, A4, PARTFUN1:def_6;
thus (X_axis f) . k = (f /. k) `1 by A4, GOBOARD1:def_1
.= proj1 . (f . k) by A5, PSCOMP_1:def_5
.= pf . k by A2, A4, FUNCT_1:13 ; ::_thesis: verum
end;
len pf = len f by FINSEQ_2:33;
then dom (X_axis f) = dom pf by A1, FINSEQ_3:29;
hence X_axis f = proj1 * f by A3, FINSEQ_1:13; ::_thesis: verum
end;
theorem Th11: :: JORDAN1H:11
for f being FinSequence of (TOP-REAL 2) holds Y_axis f = proj2 * f
proof
let f be FinSequence of (TOP-REAL 2); ::_thesis: Y_axis f = proj2 * f
reconsider pf = proj2 * f as FinSequence of REAL by FINSEQ_2:32;
A1: len (Y_axis f) = len f by GOBOARD1:def_2;
then A2: dom (Y_axis f) = dom f by FINSEQ_3:29;
A3: for k being Nat st k in dom (Y_axis f) holds
(Y_axis f) . k = pf . k
proof
let k be Nat; ::_thesis: ( k in dom (Y_axis f) implies (Y_axis f) . k = pf . k )
assume A4: k in dom (Y_axis f) ; ::_thesis: (Y_axis f) . k = pf . k
A5: f /. k = f . k by A2, A4, PARTFUN1:def_6;
thus (Y_axis f) . k = (f /. k) `2 by A4, GOBOARD1:def_2
.= proj2 . (f . k) by A5, PSCOMP_1:def_6
.= pf . k by A2, A4, FUNCT_1:13 ; ::_thesis: verum
end;
len pf = len f by FINSEQ_2:33;
then dom (Y_axis f) = dom pf by A1, FINSEQ_3:29;
hence Y_axis f = proj2 * f by A3, FINSEQ_1:13; ::_thesis: verum
end;
definition
let D be non empty set ;
let M be FinSequence of D * ;
:: original: Values
redefine func Values M -> Subset of D;
coherence
Values M is Subset of D
proof
set A = { (rng f) where f is Element of D * : f in rng M } ;
for X being set st X in { (rng f) where f is Element of D * : f in rng M } holds
X c= D
proof
let X be set ; ::_thesis: ( X in { (rng f) where f is Element of D * : f in rng M } implies X c= D )
assume X in { (rng f) where f is Element of D * : f in rng M } ; ::_thesis: X c= D
then ex f being Element of D * st
( X = rng f & f in rng M ) ;
hence X c= D ; ::_thesis: verum
end;
then union { (rng f) where f is Element of D * : f in rng M } c= D by ZFMISC_1:76;
hence Values M is Subset of D by MATRIX_1:41; ::_thesis: verum
end;
end;
registration
let D be non empty with_non-empty_elements set ;
let M be non empty non-empty FinSequence of D * ;
cluster Values M -> non empty ;
coherence
not Values M is empty
proof
dom (rngs M) = dom M by FUNCT_6:60;
then reconsider X = rng (rngs M) as non empty with_non-empty_elements set by RELAT_1:42;
Values M = Union (rngs M) by MATRIX_1:def_16
.= union X by CARD_3:def_4 ;
hence not Values M is empty ; ::_thesis: verum
end;
end;
theorem Th12: :: JORDAN1H:12
for D being non empty set
for M being Matrix of D
for i being Element of NAT st i in Seg (width M) holds
rng (Col (M,i)) c= Values M
proof
let D be non empty set ; ::_thesis: for M being Matrix of D
for i being Element of NAT st i in Seg (width M) holds
rng (Col (M,i)) c= Values M
let M be Matrix of D; ::_thesis: for i being Element of NAT st i in Seg (width M) holds
rng (Col (M,i)) c= Values M
let k be Element of NAT ; ::_thesis: ( k in Seg (width M) implies rng (Col (M,k)) c= Values M )
assume k in Seg (width M) ; ::_thesis: rng (Col (M,k)) c= Values M
then A1: ( 1 <= k & k <= width M ) by FINSEQ_1:1;
let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in rng (Col (M,k)) or e in Values M )
assume e in rng (Col (M,k)) ; ::_thesis: e in Values M
then consider u being set such that
A2: u in dom (Col (M,k)) and
A3: e = (Col (M,k)) . u by FUNCT_1:def_3;
reconsider u = u as Element of NAT by A2;
A4: 1 <= u by A2, FINSEQ_3:25;
A5: len (Col (M,k)) = len M by MATRIX_1:def_8;
then u <= len M by A2, FINSEQ_3:25;
then A6: [u,k] in Indices M by A4, A1, MATRIX_1:36;
A7: Values M = { (M * (i,j)) where i, j is Element of NAT : [i,j] in Indices M } by MATRIX_1:45;
dom (Col (M,k)) = dom M by A5, FINSEQ_3:29;
then (Col (M,k)) . u = M * (u,k) by A2, MATRIX_1:def_8;
hence e in Values M by A7, A3, A6; ::_thesis: verum
end;
theorem Th13: :: JORDAN1H:13
for D being non empty set
for M being Matrix of D
for i being Element of NAT st i in dom M holds
rng (Line (M,i)) c= Values M
proof
let D be non empty set ; ::_thesis: for M being Matrix of D
for i being Element of NAT st i in dom M holds
rng (Line (M,i)) c= Values M
let M be Matrix of D; ::_thesis: for i being Element of NAT st i in dom M holds
rng (Line (M,i)) c= Values M
let k be Element of NAT ; ::_thesis: ( k in dom M implies rng (Line (M,k)) c= Values M )
assume k in dom M ; ::_thesis: rng (Line (M,k)) c= Values M
then A1: ( 1 <= k & k <= len M ) by FINSEQ_3:25;
let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in rng (Line (M,k)) or e in Values M )
assume e in rng (Line (M,k)) ; ::_thesis: e in Values M
then consider u being set such that
A2: u in dom (Line (M,k)) and
A3: e = (Line (M,k)) . u by FUNCT_1:def_3;
reconsider u = u as Element of NAT by A2;
A4: 1 <= u by A2, FINSEQ_3:25;
A5: len (Line (M,k)) = width M by MATRIX_1:def_7;
then u <= width M by A2, FINSEQ_3:25;
then A6: [k,u] in Indices M by A1, A4, MATRIX_1:36;
A7: Values M = { (M * (i,j)) where i, j is Element of NAT : [i,j] in Indices M } by MATRIX_1:45;
dom (Line (M,k)) = Seg (width M) by A5, FINSEQ_1:def_3;
then (Line (M,k)) . u = M * (k,u) by A2, MATRIX_1:def_7;
hence e in Values M by A7, A3, A6; ::_thesis: verum
end;
theorem Th14: :: JORDAN1H:14
for G being V15() X_increasing-in-column Matrix of (TOP-REAL 2) holds len G <= card (proj1 .: (Values G))
proof
let G be V15() X_increasing-in-column Matrix of (TOP-REAL 2); ::_thesis: len G <= card (proj1 .: (Values G))
0 <> width G by GOBOARD1:def_3;
then 1 <= width G by NAT_1:14;
then A1: 1 in Seg (width G) by FINSEQ_1:1;
then reconsider L = X_axis (Col (G,1)) as increasing FinSequence of REAL by GOBOARD1:def_7;
A2: card (rng L) = len L by FINSEQ_4:62
.= len (Col (G,1)) by GOBOARD1:def_1
.= len G by MATRIX_1:def_8 ;
A3: rng L = rng (proj1 * (Col (G,1))) by Th10
.= proj1 .: (rng (Col (G,1))) by RELAT_1:127 ;
rng (Col (G,1)) c= Values G by A1, Th12;
hence len G <= card (proj1 .: (Values G)) by A3, A2, NAT_1:43, RELAT_1:123; ::_thesis: verum
end;
theorem Th15: :: JORDAN1H:15
for G being X_equal-in-line Matrix of (TOP-REAL 2) holds card (proj1 .: (Values G)) <= len G
proof
let G be X_equal-in-line Matrix of (TOP-REAL 2); ::_thesis: card (proj1 .: (Values G)) <= len G
deffunc H1( Nat) -> Element of REAL = proj1 . (G * ($1,1));
consider f being FinSequence such that
A1: len f = len G and
A2: for k being Nat st k in dom f holds
f . k = H1(k) from FINSEQ_1:sch_2();
A3: dom f = dom G by A1, FINSEQ_3:29;
proj1 .: (Values G) c= rng f
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in proj1 .: (Values G) or y in rng f )
A4: Values G = { (G * (i,j)) where i, j is Element of NAT : [i,j] in Indices G } by MATRIX_1:45;
assume y in proj1 .: (Values G) ; ::_thesis: y in rng f
then consider x being set such that
A5: x in the carrier of (TOP-REAL 2) and
A6: x in Values G and
A7: y = proj1 . x by FUNCT_2:64;
consider i, j being Element of NAT such that
A8: x = G * (i,j) and
A9: [i,j] in Indices G by A6, A4;
reconsider x = x as Point of (TOP-REAL 2) by A5;
A10: ( 1 <= j & j <= width G ) by A9, MATRIX_1:38;
A11: ( 1 <= i & i <= len G ) by A9, MATRIX_1:38;
then A12: i in dom G by FINSEQ_3:25;
y = x `1 by A7, PSCOMP_1:def_5
.= (G * (i,1)) `1 by A8, A11, A10, GOBOARD5:2
.= proj1 . (G * (i,1)) by PSCOMP_1:def_5
.= f . i by A2, A3, A12 ;
hence y in rng f by A3, A12, FUNCT_1:3; ::_thesis: verum
end;
then card (proj1 .: (Values G)) c= card (dom G) by A3, CARD_1:12;
then card (proj1 .: (Values G)) <= card (dom G) by NAT_1:39;
hence card (proj1 .: (Values G)) <= len G by CARD_1:62; ::_thesis: verum
end;
theorem Th16: :: JORDAN1H:16
for G being V15() X_equal-in-line X_increasing-in-column Matrix of (TOP-REAL 2) holds len G = card (proj1 .: (Values G))
proof
let G be V15() X_equal-in-line X_increasing-in-column Matrix of (TOP-REAL 2); ::_thesis: len G = card (proj1 .: (Values G))
( len G <= card (proj1 .: (Values G)) & card (proj1 .: (Values G)) <= len G ) by Th14, Th15;
hence len G = card (proj1 .: (Values G)) by XXREAL_0:1; ::_thesis: verum
end;
theorem Th17: :: JORDAN1H:17
for G being V15() Y_increasing-in-line Matrix of (TOP-REAL 2) holds width G <= card (proj2 .: (Values G))
proof
let G be V15() Y_increasing-in-line Matrix of (TOP-REAL 2); ::_thesis: width G <= card (proj2 .: (Values G))
0 <> len G by GOBOARD1:def_3;
then 1 <= len G by NAT_1:14;
then A1: 1 in dom G by FINSEQ_3:25;
then reconsider L = Y_axis (Line (G,1)) as increasing FinSequence of REAL by GOBOARD1:def_6;
A2: card (rng L) = len L by FINSEQ_4:62
.= len (Line (G,1)) by GOBOARD1:def_2
.= width G by MATRIX_1:def_7 ;
A3: rng L = rng (proj2 * (Line (G,1))) by Th11
.= proj2 .: (rng (Line (G,1))) by RELAT_1:127 ;
rng (Line (G,1)) c= Values G by A1, Th13;
hence width G <= card (proj2 .: (Values G)) by A3, A2, NAT_1:43, RELAT_1:123; ::_thesis: verum
end;
theorem Th18: :: JORDAN1H:18
for G being V15() Y_equal-in-column Matrix of (TOP-REAL 2) holds card (proj2 .: (Values G)) <= width G
proof
let G be V15() Y_equal-in-column Matrix of (TOP-REAL 2); ::_thesis: card (proj2 .: (Values G)) <= width G
deffunc H1( Nat) -> Element of REAL = proj2 . (G * (1,$1));
consider f being FinSequence such that
A1: len f = width G and
A2: for k being Nat st k in dom f holds
f . k = H1(k) from FINSEQ_1:sch_2();
A3: dom f = Seg (width G) by A1, FINSEQ_1:def_3;
proj2 .: (Values G) c= rng f
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in proj2 .: (Values G) or y in rng f )
A4: Values G = { (G * (i,j)) where i, j is Element of NAT : [i,j] in Indices G } by MATRIX_1:45;
assume y in proj2 .: (Values G) ; ::_thesis: y in rng f
then consider x being set such that
A5: x in the carrier of (TOP-REAL 2) and
A6: x in Values G and
A7: y = proj2 . x by FUNCT_2:64;
consider i, j being Element of NAT such that
A8: x = G * (i,j) and
A9: [i,j] in Indices G by A6, A4;
reconsider x = x as Point of (TOP-REAL 2) by A5;
A10: ( 1 <= i & i <= len G ) by A9, MATRIX_1:38;
A11: ( 1 <= j & j <= width G ) by A9, MATRIX_1:38;
then A12: j in Seg (width G) by FINSEQ_1:1;
y = x `2 by A7, PSCOMP_1:def_6
.= (G * (1,j)) `2 by A8, A11, A10, GOBOARD5:1
.= proj2 . (G * (1,j)) by PSCOMP_1:def_6
.= f . j by A2, A3, A12 ;
hence y in rng f by A3, A12, FUNCT_1:3; ::_thesis: verum
end;
then card (proj2 .: (Values G)) c= card (Seg (width G)) by A3, CARD_1:12;
then card (proj2 .: (Values G)) <= card (Seg (width G)) by NAT_1:39;
hence card (proj2 .: (Values G)) <= width G by FINSEQ_1:57; ::_thesis: verum
end;
theorem Th19: :: JORDAN1H:19
for G being V15() Y_equal-in-column Y_increasing-in-line Matrix of (TOP-REAL 2) holds width G = card (proj2 .: (Values G))
proof
let G be V15() Y_equal-in-column Y_increasing-in-line Matrix of (TOP-REAL 2); ::_thesis: width G = card (proj2 .: (Values G))
( width G <= card (proj2 .: (Values G)) & card (proj2 .: (Values G)) <= width G ) by Th17, Th18;
hence width G = card (proj2 .: (Values G)) by XXREAL_0:1; ::_thesis: verum
end;
begin
theorem :: JORDAN1H:20
for G being Go-board
for f being FinSequence of (TOP-REAL 2) st f is_sequence_on G holds
for k being Element of NAT st 1 <= k & k + 1 <= len f holds
LSeg (f,k) c= left_cell (f,k,G)
proof
let G be Go-board; ::_thesis: for f being FinSequence of (TOP-REAL 2) st f is_sequence_on G holds
for k being Element of NAT st 1 <= k & k + 1 <= len f holds
LSeg (f,k) c= left_cell (f,k,G)
let f be FinSequence of (TOP-REAL 2); ::_thesis: ( f is_sequence_on G implies for k being Element of NAT st 1 <= k & k + 1 <= len f holds
LSeg (f,k) c= left_cell (f,k,G) )
assume A1: f is_sequence_on G ; ::_thesis: for k being Element of NAT st 1 <= k & k + 1 <= len f holds
LSeg (f,k) c= left_cell (f,k,G)
let k be Element of NAT ; ::_thesis: ( 1 <= k & k + 1 <= len f implies LSeg (f,k) c= left_cell (f,k,G) )
assume A2: ( 1 <= k & k + 1 <= len f ) ; ::_thesis: LSeg (f,k) c= left_cell (f,k,G)
then A3: k in dom f by SEQ_4:134;
then consider i1, j1 being Element of NAT such that
A4: [i1,j1] in Indices G and
A5: f /. k = G * (i1,j1) by A1, GOBOARD1:def_9;
A6: k + 1 in dom f by A2, SEQ_4:134;
then consider i2, j2 being Element of NAT such that
A7: [i2,j2] in Indices G and
A8: f /. (k + 1) = G * (i2,j2) by A1, GOBOARD1:def_9;
A9: 1 <= i2 by A7, MATRIX_1:38;
A10: 1 <= j1 by A4, MATRIX_1:38;
left_cell (f,k,G) = left_cell (f,k,G) ;
then A11: ( ( 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, A4, A5, A7, A8, GOBRD13:def_3;
A12: 1 <= j2 by A7, MATRIX_1:38;
A13: j1 <= width G by A4, MATRIX_1:38;
A14: j2 <= width G by A7, MATRIX_1:38;
A15: i2 <= len G by A7, MATRIX_1:38;
A16: 1 <= i1 by A4, MATRIX_1:38;
(abs (i1 - i2)) + (abs (j1 - j2)) = 1 by A1, A3, A6, A4, A5, A7, A8, GOBOARD1:def_9;
then A17: ( ( abs (i1 - i2) = 1 & j1 = j2 ) or ( abs (j1 - j2) = 1 & i1 = i2 ) ) by SEQM_3:42;
A18: i1 <= len G by A4, 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 A17, SEQM_3:41;
supposeA19: ( i1 = i2 & j1 + 1 = j2 ) ; ::_thesis: LSeg (f,k) c= left_cell (f,k,G)
then A20: j1 < width G by A14, NAT_1:13;
A21: (i1 -' 1) + 1 = i1 by A16, XREAL_1:235;
then i1 -' 1 < len G by A18, NAT_1:13;
then LSeg ((f /. k),(f /. (k + 1))) c= cell (G,(i1 -' 1),j1) by A5, A8, A10, A19, A21, A20, GOBOARD5:18;
hence LSeg (f,k) c= left_cell (f,k,G) by A2, A11, A19, TOPREAL1:def_3; ::_thesis: verum
end;
supposeA22: ( i1 + 1 = i2 & j1 = j2 ) ; ::_thesis: LSeg (f,k) c= left_cell (f,k,G)
then i1 < len G by A15, NAT_1:13;
then LSeg ((f /. k),(f /. (k + 1))) c= cell (G,i1,j1) by A5, A8, A16, A10, A13, A22, GOBOARD5:22;
hence LSeg (f,k) c= left_cell (f,k,G) by A2, A11, A22, TOPREAL1:def_3; ::_thesis: verum
end;
supposeA23: ( i1 = i2 + 1 & j1 = j2 ) ; ::_thesis: LSeg (f,k) c= left_cell (f,k,G)
then A24: i2 < len G by A18, NAT_1:13;
A25: (j2 -' 1) + 1 = j2 by A12, XREAL_1:235;
then j2 -' 1 < width G by A14, NAT_1:13;
then LSeg ((f /. k),(f /. (k + 1))) c= cell (G,i2,(j2 -' 1)) by A5, A8, A9, A23, A25, A24, GOBOARD5:21;
hence LSeg (f,k) c= left_cell (f,k,G) by A2, A11, A23, TOPREAL1:def_3; ::_thesis: verum
end;
supposeA26: ( i1 = i2 & j1 = j2 + 1 ) ; ::_thesis: LSeg (f,k) c= left_cell (f,k,G)
then j2 < width G by A13, NAT_1:13;
then LSeg ((f /. k),(f /. (k + 1))) c= left_cell (f,k,G) by A5, A8, A16, A18, A12, A11, A26, GOBOARD5:19;
hence LSeg (f,k) c= left_cell (f,k,G) by A2, TOPREAL1:def_3; ::_thesis: verum
end;
end;
end;
theorem :: JORDAN1H:21
for k being Element of NAT
for f being standard special_circular_sequence st 1 <= k & k + 1 <= len f holds
left_cell (f,k,(GoB f)) = left_cell (f,k)
proof
let k be Element of NAT ; ::_thesis: for f being standard special_circular_sequence st 1 <= k & k + 1 <= len f holds
left_cell (f,k,(GoB f)) = left_cell (f,k)
let f be standard special_circular_sequence; ::_thesis: ( 1 <= k & k + 1 <= len f implies left_cell (f,k,(GoB f)) = left_cell (f,k) )
assume that
A1: 1 <= k and
A2: k + 1 <= len f ; ::_thesis: left_cell (f,k,(GoB f)) = left_cell (f,k)
set G = GoB f;
A3: f is_sequence_on GoB f by GOBOARD5:def_5;
for i1, j1, i2, j2 being Element of NAT st [i1,j1] in Indices (GoB f) & [i2,j2] in Indices (GoB f) & f /. k = (GoB f) * (i1,j1) & f /. (k + 1) = (GoB f) * (i2,j2) & not ( i1 = i2 & j1 + 1 = j2 & left_cell (f,k) = cell ((GoB f),(i1 -' 1),j1) ) & not ( i1 + 1 = i2 & j1 = j2 & left_cell (f,k) = cell ((GoB f),i1,j1) ) & not ( i1 = i2 + 1 & j1 = j2 & left_cell (f,k) = cell ((GoB f),i2,(j2 -' 1)) ) holds
( i1 = i2 & j1 = j2 + 1 & left_cell (f,k) = cell ((GoB f),i1,j2) )
proof
1 <= k + 1 by NAT_1:11;
then A4: k + 1 in dom f by A2, FINSEQ_3:25;
let i1, j1, i2, j2 be Element of NAT ; ::_thesis: ( [i1,j1] in Indices (GoB f) & [i2,j2] in Indices (GoB f) & f /. k = (GoB f) * (i1,j1) & f /. (k + 1) = (GoB f) * (i2,j2) & not ( i1 = i2 & j1 + 1 = j2 & left_cell (f,k) = cell ((GoB f),(i1 -' 1),j1) ) & not ( i1 + 1 = i2 & j1 = j2 & left_cell (f,k) = cell ((GoB f),i1,j1) ) & not ( i1 = i2 + 1 & j1 = j2 & left_cell (f,k) = cell ((GoB f),i2,(j2 -' 1)) ) implies ( i1 = i2 & j1 = j2 + 1 & left_cell (f,k) = cell ((GoB f),i1,j2) ) )
assume A5: ( [i1,j1] in Indices (GoB f) & [i2,j2] in Indices (GoB f) & f /. k = (GoB f) * (i1,j1) & f /. (k + 1) = (GoB f) * (i2,j2) ) ; ::_thesis: ( ( i1 = i2 & j1 + 1 = j2 & left_cell (f,k) = cell ((GoB f),(i1 -' 1),j1) ) or ( i1 + 1 = i2 & j1 = j2 & left_cell (f,k) = cell ((GoB f),i1,j1) ) or ( i1 = i2 + 1 & j1 = j2 & left_cell (f,k) = cell ((GoB f),i2,(j2 -' 1)) ) or ( i1 = i2 & j1 = j2 + 1 & left_cell (f,k) = cell ((GoB f),i1,j2) ) )
k < len f by A2, NAT_1:13;
then k in dom f by A1, FINSEQ_3:25;
then (abs (i1 - i2)) + (abs (j1 - j2)) = 1 by A3, A5, A4, GOBOARD1:def_9;
then A6: ( ( abs (i1 - i2) = 1 & j1 = j2 ) or ( abs (j1 - j2) = 1 & i1 = i2 ) ) by SEQM_3:42;
left_cell (f,k) = left_cell (f,k) ;
then A7: ( ( i1 = i2 & j1 + 1 = j2 & left_cell (f,k) = cell ((GoB f),(i1 -' 1),j1) ) or ( i1 + 1 = i2 & j1 = j2 & left_cell (f,k) = cell ((GoB f),i1,j1) ) or ( i1 = i2 + 1 & j1 = j2 & left_cell (f,k) = cell ((GoB f),i2,(j2 -' 1)) ) or ( i1 = i2 & j1 = j2 + 1 & left_cell (f,k) = cell ((GoB f),i1,j2) ) ) by A1, A2, A5, GOBOARD5:def_7;
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 A6, SEQM_3:41;
case ( i1 = i2 & j1 + 1 = j2 ) ; ::_thesis: left_cell (f,k) = cell ((GoB f),(i1 -' 1),j1)
hence left_cell (f,k) = cell ((GoB f),(i1 -' 1),j1) by A7; ::_thesis: verum
end;
case ( i1 + 1 = i2 & j1 = j2 ) ; ::_thesis: left_cell (f,k) = cell ((GoB f),i1,j1)
hence left_cell (f,k) = cell ((GoB f),i1,j1) by A7; ::_thesis: verum
end;
case ( i1 = i2 + 1 & j1 = j2 ) ; ::_thesis: left_cell (f,k) = cell ((GoB f),i2,(j2 -' 1))
hence left_cell (f,k) = cell ((GoB f),i2,(j2 -' 1)) by A7; ::_thesis: verum
end;
case ( i1 = i2 & j1 = j2 + 1 ) ; ::_thesis: left_cell (f,k) = cell ((GoB f),i1,j2)
hence left_cell (f,k) = cell ((GoB f),i1,j2) by A7; ::_thesis: verum
end;
end;
end;
hence left_cell (f,k,(GoB f)) = left_cell (f,k) by A1, A2, A3, GOBRD13:def_3; ::_thesis: verum
end;
theorem Th22: :: JORDAN1H:22
for G being Go-board
for f being FinSequence of (TOP-REAL 2) st f is_sequence_on G holds
for k being Element of NAT st 1 <= k & k + 1 <= len f holds
LSeg (f,k) c= right_cell (f,k,G)
proof
let G be Go-board; ::_thesis: for f being FinSequence of (TOP-REAL 2) st f is_sequence_on G holds
for k being Element of NAT st 1 <= k & k + 1 <= len f holds
LSeg (f,k) c= right_cell (f,k,G)
let f be FinSequence of (TOP-REAL 2); ::_thesis: ( f is_sequence_on G implies for k being Element of NAT st 1 <= k & k + 1 <= len f holds
LSeg (f,k) c= right_cell (f,k,G) )
assume A1: f is_sequence_on G ; ::_thesis: for k being Element of NAT st 1 <= k & k + 1 <= len f holds
LSeg (f,k) c= right_cell (f,k,G)
let k be Element of NAT ; ::_thesis: ( 1 <= k & k + 1 <= len f implies LSeg (f,k) c= right_cell (f,k,G) )
assume A2: ( 1 <= k & k + 1 <= len f ) ; ::_thesis: LSeg (f,k) c= right_cell (f,k,G)
then A3: k in dom f by SEQ_4:134;
then consider i1, j1 being Element of NAT such that
A4: [i1,j1] in Indices G and
A5: f /. k = G * (i1,j1) by A1, GOBOARD1:def_9;
A6: k + 1 in dom f by A2, SEQ_4:134;
then consider i2, j2 being Element of NAT such that
A7: [i2,j2] in Indices G and
A8: f /. (k + 1) = G * (i2,j2) by A1, GOBOARD1:def_9;
A9: 1 <= i2 by A7, MATRIX_1:38;
A10: 1 <= j1 by A4, MATRIX_1:38;
right_cell (f,k,G) = right_cell (f,k,G) ;
then A11: ( ( i1 = i2 & j1 + 1 = j2 & right_cell (f,k,G) = cell (G,i1,j1) ) or ( i1 + 1 = i2 & j1 = j2 & right_cell (f,k,G) = cell (G,i1,(j1 -' 1)) ) or ( i1 = i2 + 1 & j1 = j2 & right_cell (f,k,G) = cell (G,i2,j2) ) or ( i1 = i2 & j1 = j2 + 1 & right_cell (f,k,G) = cell (G,(i1 -' 1),j2) ) ) by A1, A2, A4, A5, A7, A8, GOBRD13:def_2;
A12: 1 <= j2 by A7, MATRIX_1:38;
A13: j1 <= width G by A4, MATRIX_1:38;
A14: j2 <= width G by A7, MATRIX_1:38;
A15: i2 <= len G by A7, MATRIX_1:38;
A16: 1 <= i1 by A4, MATRIX_1:38;
(abs (i1 - i2)) + (abs (j1 - j2)) = 1 by A1, A3, A6, A4, A5, A7, A8, GOBOARD1:def_9;
then A17: ( ( abs (i1 - i2) = 1 & j1 = j2 ) or ( abs (j1 - j2) = 1 & i1 = i2 ) ) by SEQM_3:42;
A18: i1 <= len G by A4, 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 A17, SEQM_3:41;
supposeA19: ( i1 = i2 & j1 + 1 = j2 ) ; ::_thesis: LSeg (f,k) c= right_cell (f,k,G)
then j1 < width G by A14, NAT_1:13;
then LSeg ((f /. k),(f /. (k + 1))) c= cell (G,i1,j1) by A5, A8, A16, A18, A10, A19, GOBOARD5:19;
hence LSeg (f,k) c= right_cell (f,k,G) by A2, A11, A19, TOPREAL1:def_3; ::_thesis: verum
end;
supposeA20: ( i1 + 1 = i2 & j1 = j2 ) ; ::_thesis: LSeg (f,k) c= right_cell (f,k,G)
then A21: i1 < len G by A15, NAT_1:13;
A22: (j1 -' 1) + 1 = j1 by A10, XREAL_1:235;
then j1 -' 1 < width G by A13, NAT_1:13;
then LSeg ((f /. k),(f /. (k + 1))) c= cell (G,i1,(j1 -' 1)) by A5, A8, A16, A20, A22, A21, GOBOARD5:21;
hence LSeg (f,k) c= right_cell (f,k,G) by A2, A11, A20, TOPREAL1:def_3; ::_thesis: verum
end;
supposeA23: ( i1 = i2 + 1 & j1 = j2 ) ; ::_thesis: LSeg (f,k) c= right_cell (f,k,G)
then i2 < len G by A18, NAT_1:13;
then LSeg ((f /. k),(f /. (k + 1))) c= cell (G,i2,j2) by A5, A8, A9, A12, A14, A23, GOBOARD5:22;
hence LSeg (f,k) c= right_cell (f,k,G) by A2, A11, A23, TOPREAL1:def_3; ::_thesis: verum
end;
supposeA24: ( i1 = i2 & j1 = j2 + 1 ) ; ::_thesis: LSeg (f,k) c= right_cell (f,k,G)
then A25: j2 < width G by A13, NAT_1:13;
A26: (i1 -' 1) + 1 = i1 by A16, XREAL_1:235;
then i1 -' 1 < len G by A18, NAT_1:13;
then LSeg ((f /. k),(f /. (k + 1))) c= right_cell (f,k,G) by A5, A8, A12, A11, A24, A26, A25, GOBOARD5:18;
hence LSeg (f,k) c= right_cell (f,k,G) by A2, TOPREAL1:def_3; ::_thesis: verum
end;
end;
end;
theorem Th23: :: JORDAN1H:23
for k being Element of NAT
for f being standard special_circular_sequence st 1 <= k & k + 1 <= len f holds
right_cell (f,k,(GoB f)) = right_cell (f,k)
proof
let k be Element of NAT ; ::_thesis: for f being standard special_circular_sequence st 1 <= k & k + 1 <= len f holds
right_cell (f,k,(GoB f)) = right_cell (f,k)
let f be standard special_circular_sequence; ::_thesis: ( 1 <= k & k + 1 <= len f implies right_cell (f,k,(GoB f)) = right_cell (f,k) )
assume that
A1: 1 <= k and
A2: k + 1 <= len f ; ::_thesis: right_cell (f,k,(GoB f)) = right_cell (f,k)
set G = GoB f;
A3: f is_sequence_on GoB f by GOBOARD5:def_5;
for i1, j1, i2, j2 being Element of NAT st [i1,j1] in Indices (GoB f) & [i2,j2] in Indices (GoB f) & f /. k = (GoB f) * (i1,j1) & f /. (k + 1) = (GoB f) * (i2,j2) & not ( i1 = i2 & j1 + 1 = j2 & right_cell (f,k) = cell ((GoB f),i1,j1) ) & not ( i1 + 1 = i2 & j1 = j2 & right_cell (f,k) = cell ((GoB f),i1,(j1 -' 1)) ) & not ( i1 = i2 + 1 & j1 = j2 & right_cell (f,k) = cell ((GoB f),i2,j2) ) holds
( i1 = i2 & j1 = j2 + 1 & right_cell (f,k) = cell ((GoB f),(i1 -' 1),j2) )
proof
1 <= k + 1 by NAT_1:11;
then A4: k + 1 in dom f by A2, FINSEQ_3:25;
set IT = right_cell (f,k);
let i1, j1, i2, j2 be Element of NAT ; ::_thesis: ( [i1,j1] in Indices (GoB f) & [i2,j2] in Indices (GoB f) & f /. k = (GoB f) * (i1,j1) & f /. (k + 1) = (GoB f) * (i2,j2) & not ( i1 = i2 & j1 + 1 = j2 & right_cell (f,k) = cell ((GoB f),i1,j1) ) & not ( i1 + 1 = i2 & j1 = j2 & right_cell (f,k) = cell ((GoB f),i1,(j1 -' 1)) ) & not ( i1 = i2 + 1 & j1 = j2 & right_cell (f,k) = cell ((GoB f),i2,j2) ) implies ( i1 = i2 & j1 = j2 + 1 & right_cell (f,k) = cell ((GoB f),(i1 -' 1),j2) ) )
assume A5: ( [i1,j1] in Indices (GoB f) & [i2,j2] in Indices (GoB f) & f /. k = (GoB f) * (i1,j1) & f /. (k + 1) = (GoB f) * (i2,j2) ) ; ::_thesis: ( ( i1 = i2 & j1 + 1 = j2 & right_cell (f,k) = cell ((GoB f),i1,j1) ) or ( i1 + 1 = i2 & j1 = j2 & right_cell (f,k) = cell ((GoB f),i1,(j1 -' 1)) ) or ( i1 = i2 + 1 & j1 = j2 & right_cell (f,k) = cell ((GoB f),i2,j2) ) or ( i1 = i2 & j1 = j2 + 1 & right_cell (f,k) = cell ((GoB f),(i1 -' 1),j2) ) )
k < len f by A2, NAT_1:13;
then k in dom f by A1, FINSEQ_3:25;
then (abs (i1 - i2)) + (abs (j1 - j2)) = 1 by A3, A5, A4, GOBOARD1:def_9;
then A6: ( ( abs (i1 - i2) = 1 & j1 = j2 ) or ( abs (j1 - j2) = 1 & i1 = i2 ) ) by SEQM_3:42;
right_cell (f,k) = right_cell (f,k) ;
then A7: ( ( i1 = i2 & j1 + 1 = j2 & right_cell (f,k) = cell ((GoB f),i1,j1) ) or ( i1 + 1 = i2 & j1 = j2 & right_cell (f,k) = cell ((GoB f),i1,(j1 -' 1)) ) or ( i1 = i2 + 1 & j1 = j2 & right_cell (f,k) = cell ((GoB f),i2,j2) ) or ( i1 = i2 & j1 = j2 + 1 & right_cell (f,k) = cell ((GoB f),(i1 -' 1),j2) ) ) by A1, A2, A5, GOBOARD5:def_6;
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 A6, SEQM_3:41;
case ( i1 = i2 & j1 + 1 = j2 ) ; ::_thesis: right_cell (f,k) = cell ((GoB f),i1,j1)
hence right_cell (f,k) = cell ((GoB f),i1,j1) by A7; ::_thesis: verum
end;
case ( i1 + 1 = i2 & j1 = j2 ) ; ::_thesis: right_cell (f,k) = cell ((GoB f),i1,(j1 -' 1))
hence right_cell (f,k) = cell ((GoB f),i1,(j1 -' 1)) by A7; ::_thesis: verum
end;
case ( i1 = i2 + 1 & j1 = j2 ) ; ::_thesis: right_cell (f,k) = cell ((GoB f),i2,j2)
hence right_cell (f,k) = cell ((GoB f),i2,j2) by A7; ::_thesis: verum
end;
case ( i1 = i2 & j1 = j2 + 1 ) ; ::_thesis: right_cell (f,k) = cell ((GoB f),(i1 -' 1),j2)
hence right_cell (f,k) = cell ((GoB f),(i1 -' 1),j2) by A7; ::_thesis: verum
end;
end;
end;
hence right_cell (f,k,(GoB f)) = right_cell (f,k) by A1, A2, A3, GOBRD13:def_2; ::_thesis: verum
end;
theorem :: JORDAN1H:24
for P being Subset of (TOP-REAL 2)
for f being non constant standard special_circular_sequence holds
( not P is_a_component_of (L~ f) ` or P = RightComp f or P = LeftComp f )
proof
let P be Subset of (TOP-REAL 2); ::_thesis: for f being non constant standard special_circular_sequence holds
( not P is_a_component_of (L~ f) ` or P = RightComp f or P = LeftComp f )
let f be non constant standard special_circular_sequence; ::_thesis: ( not P is_a_component_of (L~ f) ` or P = RightComp f or P = LeftComp f )
assume P is_a_component_of (L~ f) ` ; ::_thesis: ( P = RightComp f or P = LeftComp f )
then ex B1 being Subset of ((TOP-REAL 2) | ((L~ f) `)) st
( B1 = P & B1 is a_component ) by CONNSP_1:def_6;
hence ( P = RightComp f or P = LeftComp f ) by GOBRD14:12; ::_thesis: verum
end;
theorem :: JORDAN1H:25
for G being Go-board
for f being non constant standard special_circular_sequence st f is_sequence_on G holds
for k being Element of NAT st 1 <= k & k + 1 <= len f holds
( Int (right_cell (f,k,G)) c= RightComp f & Int (left_cell (f,k,G)) c= LeftComp f )
proof
let G be Go-board; ::_thesis: for f being non constant standard special_circular_sequence st f is_sequence_on G holds
for k being Element of NAT st 1 <= k & k + 1 <= len f holds
( Int (right_cell (f,k,G)) c= RightComp f & Int (left_cell (f,k,G)) c= LeftComp f )
let f be non constant standard special_circular_sequence; ::_thesis: ( f is_sequence_on G implies for k being Element of NAT st 1 <= k & k + 1 <= len f holds
( Int (right_cell (f,k,G)) c= RightComp f & Int (left_cell (f,k,G)) c= LeftComp f ) )
assume A1: f is_sequence_on G ; ::_thesis: for k being Element of NAT st 1 <= k & k + 1 <= len f holds
( Int (right_cell (f,k,G)) c= RightComp f & Int (left_cell (f,k,G)) c= LeftComp f )
let k be Element of NAT ; ::_thesis: ( 1 <= k & k + 1 <= len f implies ( Int (right_cell (f,k,G)) c= RightComp f & Int (left_cell (f,k,G)) c= LeftComp f ) )
assume A2: ( 1 <= k & k + 1 <= len f ) ; ::_thesis: ( Int (right_cell (f,k,G)) c= RightComp f & Int (left_cell (f,k,G)) c= LeftComp f )
Int (right_cell (f,k,G)) misses L~ f by A1, A2, JORDAN9:15;
then A3: Int (right_cell (f,k,G)) c= (right_cell (f,k,G)) \ (L~ f) by TOPS_1:16, XBOOLE_1:86;
Int (left_cell (f,k,G)) misses L~ f by A1, A2, JORDAN9:15;
then A4: Int (left_cell (f,k,G)) c= (left_cell (f,k,G)) \ (L~ f) by TOPS_1:16, XBOOLE_1:86;
(right_cell (f,k,G)) \ (L~ f) c= RightComp f by A1, A2, JORDAN9:27;
hence Int (right_cell (f,k,G)) c= RightComp f by A3, XBOOLE_1:1; ::_thesis: Int (left_cell (f,k,G)) c= LeftComp f
(left_cell (f,k,G)) \ (L~ f) c= LeftComp f by A1, A2, JORDAN9:27;
hence Int (left_cell (f,k,G)) c= LeftComp f by A4, XBOOLE_1:1; ::_thesis: verum
end;
theorem Th26: :: JORDAN1H:26
for i1, j1, i2, j2 being Element of NAT
for G being Go-board st [i1,j1] in Indices G & [i2,j2] in Indices G & G * (i1,j1) = G * (i2,j2) holds
( i1 = i2 & j1 = j2 )
proof
let i1, j1, i2, j2 be Element of NAT ; ::_thesis: for G being Go-board st [i1,j1] in Indices G & [i2,j2] in Indices G & G * (i1,j1) = G * (i2,j2) holds
( i1 = i2 & j1 = j2 )
let G be Go-board; ::_thesis: ( [i1,j1] in Indices G & [i2,j2] in Indices G & G * (i1,j1) = G * (i2,j2) implies ( i1 = i2 & j1 = j2 ) )
assume that
A1: [i1,j1] in Indices G and
A2: [i2,j2] in Indices G and
A3: G * (i1,j1) = G * (i2,j2) ; ::_thesis: ( i1 = i2 & j1 = j2 )
A4: 1 <= i1 by A1, MATRIX_1:38;
A5: j1 <= width G by A1, MATRIX_1:38;
A6: 1 <= j1 by A1, MATRIX_1:38;
A7: 1 <= i2 by A2, MATRIX_1:38;
A8: i1 <= len G by A1, MATRIX_1:38;
A9: i2 <= len G by A2, MATRIX_1:38;
A10: j2 <= width G by A2, MATRIX_1:38;
A11: 1 <= j2 by A2, MATRIX_1:38;
then A12: (G * (i1,j2)) `2 = (G * (1,j2)) `2 by A4, A8, A10, GOBOARD5:1
.= (G * (i1,j1)) `2 by A3, A7, A9, A11, A10, GOBOARD5:1 ;
A13: (G * (i1,j2)) `1 = (G * (i1,1)) `1 by A4, A8, A11, A10, GOBOARD5:2
.= (G * (i1,j1)) `1 by A4, A8, A6, A5, GOBOARD5:2 ;
assume A14: ( not i1 = i2 or not j1 = j2 ) ; ::_thesis: contradiction
percases ( i1 < i2 or i1 > i2 or j1 < j2 or j1 > j2 ) by A14, XXREAL_0:1;
suppose i1 < i2 ; ::_thesis: contradiction
hence contradiction by A3, A4, A9, A11, A10, A13, GOBOARD5:3; ::_thesis: verum
end;
suppose i1 > i2 ; ::_thesis: contradiction
hence contradiction by A3, A8, A7, A11, A10, A13, GOBOARD5:3; ::_thesis: verum
end;
suppose j1 < j2 ; ::_thesis: contradiction
hence contradiction by A4, A8, A6, A10, A12, GOBOARD5:4; ::_thesis: verum
end;
suppose j1 > j2 ; ::_thesis: contradiction
hence contradiction by A4, A8, A5, A11, A12, GOBOARD5:4; ::_thesis: verum
end;
end;
end;
theorem Th27: :: JORDAN1H:27
for i1, i2 being Element of NAT
for f being FinSequence of (TOP-REAL 2)
for M being Go-board st f is_sequence_on M holds
mid (f,i1,i2) is_sequence_on M
proof
let i1, i2 be Element of NAT ; ::_thesis: for f being FinSequence of (TOP-REAL 2)
for M being Go-board st f is_sequence_on M holds
mid (f,i1,i2) is_sequence_on M
let f be FinSequence of (TOP-REAL 2); ::_thesis: for M being Go-board st f is_sequence_on M holds
mid (f,i1,i2) is_sequence_on M
let M be Go-board; ::_thesis: ( f is_sequence_on M implies mid (f,i1,i2) is_sequence_on M )
assume A1: f is_sequence_on M ; ::_thesis: mid (f,i1,i2) is_sequence_on M
percases ( i1 <= i2 or i1 > i2 ) ;
supposeA2: i1 <= i2 ; ::_thesis: mid (f,i1,i2) is_sequence_on M
A3: f /^ (i1 -' 1) is_sequence_on M by A1, JORDAN8:2;
mid (f,i1,i2) = (f /^ (i1 -' 1)) | ((i2 -' i1) + 1) by A2, FINSEQ_6:def_3;
hence mid (f,i1,i2) is_sequence_on M by A3, GOBOARD1:22; ::_thesis: verum
end;
supposeA4: i1 > i2 ; ::_thesis: mid (f,i1,i2) is_sequence_on M
f /^ (i2 -' 1) is_sequence_on M by A1, JORDAN8:2;
then A5: (f /^ (i2 -' 1)) | ((i1 -' i2) + 1) is_sequence_on M by GOBOARD1:22;
mid (f,i1,i2) = Rev ((f /^ (i2 -' 1)) | ((i1 -' i2) + 1)) by A4, FINSEQ_6:def_3;
hence mid (f,i1,i2) is_sequence_on M by A5, JORDAN9:5; ::_thesis: verum
end;
end;
end;
registration
cluster non empty-yielding tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column -> non empty non-empty for FinSequence of the carrier of (TOP-REAL 2) * ;
coherence
for b1 being Go-board holds
( not b1 is empty & b1 is non-empty )
proof
let G be Go-board; ::_thesis: ( not G is empty & G is non-empty )
thus not G is empty ; ::_thesis: G is non-empty
consider n0 being Nat such that
A1: for x being set st x in rng G holds
ex s being FinSequence st
( s = x & len s = n0 ) by MATRIX_1:def_1;
len G <> 0 by GOBOARD1:def_3;
then consider s0 being FinSequence such that
A2: s0 in rng G and
A3: len s0 = width G by MATRIX_1:def_3;
A4: ex s being FinSequence st
( s = s0 & len s = n0 ) by A2, A1;
assume not G is non-empty ; ::_thesis: contradiction
then consider n being set such that
A5: n in dom G and
A6: G . n is empty by FUNCT_1:def_9;
A7: card (G . n) is empty by A6;
ex s1 being FinSequence st
( s1 = G . n & len s1 = n0 ) by A5, A1, FUNCT_1:3;
hence contradiction by A3, A4, A7, GOBOARD1:def_3; ::_thesis: verum
end;
end;
theorem Th28: :: JORDAN1H:28
for i being Element of NAT
for G being Go-board st 1 <= i & i <= len G holds
(SgmX (RealOrd,(proj1 .: (Values G)))) . i = (G * (i,1)) `1
proof
let i be Element of NAT ; ::_thesis: for G being Go-board st 1 <= i & i <= len G holds
(SgmX (RealOrd,(proj1 .: (Values G)))) . i = (G * (i,1)) `1
let G be Go-board; ::_thesis: ( 1 <= i & i <= len G implies (SgmX (RealOrd,(proj1 .: (Values G)))) . i = (G * (i,1)) `1 )
assume ( 1 <= i & i <= len G ) ; ::_thesis: (SgmX (RealOrd,(proj1 .: (Values G)))) . i = (G * (i,1)) `1
then i in dom G by FINSEQ_3:25;
then A1: i in Seg (len G) by FINSEQ_1:def_3;
0 <> width G by GOBOARD1:def_3;
then A2: 1 <= width G by NAT_1:14;
reconsider A = proj1 .: (Values G) as finite Subset of REAL ;
deffunc H1( Nat) -> Element of REAL = (G * ($1,1)) `1 ;
consider f being FinSequence of REAL such that
A3: len f = len G and
A4: for i being Nat st i in dom f holds
f . i = H1(i) from FINSEQ_2:sch_1();
A5: dom f = Seg (len G) by A3, FINSEQ_1:def_3;
A6: rng f = A
proof
A7: Values G = { (G * (m,n)) where m, n is Element of NAT : [m,n] in Indices G } by MATRIX_1:45;
thus rng f c= A :: according to XBOOLE_0:def_10 ::_thesis: A c= rng f
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng f or x in A )
assume A8: x in rng f ; ::_thesis: x in A
then reconsider x = x as Element of REAL ;
consider y being set such that
A9: y in dom f and
A10: x = f . y by A8, FUNCT_1:def_3;
reconsider y = y as Element of NAT by A9;
( 1 <= y & y <= len G ) by A3, A9, FINSEQ_3:25;
then [y,1] in Indices G by A2, MATRIX_1:36;
then A11: G * (y,1) in Values G by A7;
x = (G * (y,1)) `1 by A4, A9, A10
.= proj1 . (G * (y,1)) by PSCOMP_1:def_5 ;
hence x in A by A11, FUNCT_2:35; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in A or x in rng f )
assume A12: x in A ; ::_thesis: x in rng f
then reconsider x = x as Element of REAL ;
consider p being Element of (TOP-REAL 2) such that
A13: p in Values G and
A14: x = proj1 . p by A12, FUNCT_2:65;
consider m, n being Element of NAT such that
A15: p = G * (m,n) and
A16: [m,n] in Indices G by A7, A13;
A17: ( 1 <= n & n <= width G ) by A16, MATRIX_1:38;
A18: ( 1 <= m & m <= len G ) by A16, MATRIX_1:38;
then A19: m in Seg (len G) by FINSEQ_1:1;
A20: m in dom f by A3, A18, FINSEQ_3:25;
x = p `1 by A14, PSCOMP_1:def_5
.= (G * (m,1)) `1 by A15, A17, A18, GOBOARD5:2
.= f . m by A4, A5, A19 ;
hence x in rng f by A20, FUNCT_1:def_3; ::_thesis: verum
end;
for n, m being Nat st n in dom f & m in dom f & n < m holds
( f /. n <> f /. m & [(f /. n),(f /. m)] in RealOrd )
proof
let n, m be Nat; ::_thesis: ( n in dom f & m in dom f & n < m implies ( f /. n <> f /. m & [(f /. n),(f /. m)] in RealOrd ) )
assume that
A21: ( n in dom f & m in dom f ) and
A22: n < m ; ::_thesis: ( f /. n <> f /. m & [(f /. n),(f /. m)] in RealOrd )
A23: ( 1 <= n & m <= len G ) by A3, A21, FINSEQ_3:25;
reconsider n9 = n, m9 = m as Element of NAT by ORDINAL1:def_12;
A24: ( f /. n = f . n & f /. m = f . m ) by A21, PARTFUN1:def_6;
A25: ( f . n = (G * (n9,1)) `1 & f . m = (G * (m9,1)) `1 ) by A4, A21;
hence f /. n <> f /. m by A2, A22, A23, A24, GOBOARD5:3; ::_thesis: [(f /. n),(f /. m)] in RealOrd
f . n9 < f . m9 by A2, A22, A25, A23, GOBOARD5:3;
hence [(f /. n),(f /. m)] in RealOrd by A24; ::_thesis: verum
end;
then f = SgmX (RealOrd,(proj1 .: (Values G))) by A6, PRE_POLY:9;
hence (SgmX (RealOrd,(proj1 .: (Values G)))) . i = (G * (i,1)) `1 by A4, A5, A1; ::_thesis: verum
end;
theorem Th29: :: JORDAN1H:29
for j being Element of NAT
for G being Go-board st 1 <= j & j <= width G holds
(SgmX (RealOrd,(proj2 .: (Values G)))) . j = (G * (1,j)) `2
proof
let j be Element of NAT ; ::_thesis: for G being Go-board st 1 <= j & j <= width G holds
(SgmX (RealOrd,(proj2 .: (Values G)))) . j = (G * (1,j)) `2
let G be Go-board; ::_thesis: ( 1 <= j & j <= width G implies (SgmX (RealOrd,(proj2 .: (Values G)))) . j = (G * (1,j)) `2 )
assume ( 1 <= j & j <= width G ) ; ::_thesis: (SgmX (RealOrd,(proj2 .: (Values G)))) . j = (G * (1,j)) `2
then A1: j in Seg (width G) by FINSEQ_1:1;
A2: 1 <= len G by NAT_1:14;
reconsider A = proj2 .: (Values G) as finite Subset of REAL ;
deffunc H1( Nat) -> Element of REAL = (G * (1,$1)) `2 ;
consider f being FinSequence of REAL such that
A3: len f = width G and
A4: for i being Nat st i in dom f holds
f . i = H1(i) from FINSEQ_2:sch_1();
A5: dom f = Seg (width G) by A3, FINSEQ_1:def_3;
A6: rng f = A
proof
A7: Values G = { (G * (m,n)) where m, n is Element of NAT : [m,n] in Indices G } by MATRIX_1:45;
thus rng f c= A :: according to XBOOLE_0:def_10 ::_thesis: A c= rng f
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng f or x in A )
assume A8: x in rng f ; ::_thesis: x in A
then reconsider x = x as Element of REAL ;
consider y being set such that
A9: y in dom f and
A10: x = f . y by A8, FUNCT_1:def_3;
reconsider y = y as Element of NAT by A9;
( 1 <= y & y <= width G ) by A3, A9, FINSEQ_3:25;
then [1,y] in Indices G by A2, MATRIX_1:36;
then A11: G * (1,y) in Values G by A7;
x = (G * (1,y)) `2 by A4, A9, A10
.= proj2 . (G * (1,y)) by PSCOMP_1:def_6 ;
hence x in A by A11, FUNCT_2:35; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in A or x in rng f )
assume A12: x in A ; ::_thesis: x in rng f
then reconsider x = x as Element of REAL ;
consider p being Element of (TOP-REAL 2) such that
A13: p in Values G and
A14: x = proj2 . p by A12, FUNCT_2:65;
consider m, n being Element of NAT such that
A15: p = G * (m,n) and
A16: [m,n] in Indices G by A7, A13;
A17: ( 1 <= m & m <= len G ) by A16, MATRIX_1:38;
A18: ( 1 <= n & n <= width G ) by A16, MATRIX_1:38;
then A19: n in Seg (width G) by FINSEQ_1:1;
A20: n in dom f by A3, A18, FINSEQ_3:25;
x = p `2 by A14, PSCOMP_1:def_6
.= (G * (1,n)) `2 by A15, A17, A18, GOBOARD5:1
.= f . n by A4, A5, A19 ;
hence x in rng f by A20, FUNCT_1:def_3; ::_thesis: verum
end;
for n, m being Nat st n in dom f & m in dom f & n < m holds
( f /. n <> f /. m & [(f /. n),(f /. m)] in RealOrd )
proof
let n, m be Nat; ::_thesis: ( n in dom f & m in dom f & n < m implies ( f /. n <> f /. m & [(f /. n),(f /. m)] in RealOrd ) )
assume that
A21: ( n in dom f & m in dom f ) and
A22: n < m ; ::_thesis: ( f /. n <> f /. m & [(f /. n),(f /. m)] in RealOrd )
A23: ( 1 <= n & m <= width G ) by A3, A21, FINSEQ_3:25;
reconsider n9 = n, m9 = m as Element of NAT by ORDINAL1:def_12;
A24: ( f /. n = f . n & f /. m = f . m ) by A21, PARTFUN1:def_6;
A25: ( f . n = (G * (1,n9)) `2 & f . m = (G * (1,m9)) `2 ) by A4, A21;
hence f /. n <> f /. m by A2, A22, A23, A24, GOBOARD5:4; ::_thesis: [(f /. n),(f /. m)] in RealOrd
f . n9 < f . m9 by A2, A22, A25, A23, GOBOARD5:4;
hence [(f /. n),(f /. m)] in RealOrd by A24; ::_thesis: verum
end;
then f = SgmX (RealOrd,(proj2 .: (Values G))) by A6, PRE_POLY:9;
hence (SgmX (RealOrd,(proj2 .: (Values G)))) . j = (G * (1,j)) `2 by A4, A5, A1; ::_thesis: verum
end;
theorem Th30: :: JORDAN1H:30
for f being non empty FinSequence of (TOP-REAL 2)
for G being Go-board st f is_sequence_on G & ex i being Element of NAT st
( [1,i] in Indices G & G * (1,i) in rng f ) & ex i being Element of NAT st
( [(len G),i] in Indices G & G * ((len G),i) in rng f ) holds
proj1 .: (rng f) = proj1 .: (Values G)
proof
let f be non empty FinSequence of (TOP-REAL 2); ::_thesis: for G being Go-board st f is_sequence_on G & ex i being Element of NAT st
( [1,i] in Indices G & G * (1,i) in rng f ) & ex i being Element of NAT st
( [(len G),i] in Indices G & G * ((len G),i) in rng f ) holds
proj1 .: (rng f) = proj1 .: (Values G)
let G be Go-board; ::_thesis: ( f is_sequence_on G & ex i being Element of NAT st
( [1,i] in Indices G & G * (1,i) in rng f ) & ex i being Element of NAT st
( [(len G),i] in Indices G & G * ((len G),i) in rng f ) implies proj1 .: (rng f) = proj1 .: (Values G) )
assume A1: f is_sequence_on G ; ::_thesis: ( for i being Element of NAT holds
( not [1,i] in Indices G or not G * (1,i) in rng f ) or for i being Element of NAT holds
( not [(len G),i] in Indices G or not G * ((len G),i) in rng f ) or proj1 .: (rng f) = proj1 .: (Values G) )
given i1 being Element of NAT such that A2: [1,i1] in Indices G and
A3: G * (1,i1) in rng f ; ::_thesis: ( for i being Element of NAT holds
( not [(len G),i] in Indices G or not G * ((len G),i) in rng f ) or proj1 .: (rng f) = proj1 .: (Values G) )
consider k1 being set such that
A4: k1 in dom f and
A5: G * (1,i1) = f . k1 by A3, FUNCT_1:def_3;
reconsider k1 = k1 as Element of NAT by A4;
A6: 1 <= k1 by A4, FINSEQ_3:25;
given i2 being Element of NAT such that A7: [(len G),i2] in Indices G and
A8: G * ((len G),i2) in rng f ; ::_thesis: proj1 .: (rng f) = proj1 .: (Values G)
consider k2 being set such that
A9: k2 in dom f and
A10: G * ((len G),i2) = f . k2 by A8, FUNCT_1:def_3;
reconsider k2 = k2 as Element of NAT by A9;
A11: k2 <= len f by A9, FINSEQ_3:25;
A12: k1 <= len f by A4, FINSEQ_3:25;
set g = mid (f,k1,k2);
A13: mid (f,k1,k2) is_sequence_on G by A1, Th27;
A14: 1 <= k2 by A9, FINSEQ_3:25;
A15: now__::_thesis:_len_(mid_(f,k1,k2))_>=_0_+_1
percases ( k1 <= k2 or k1 > k2 ) ;
suppose k1 <= k2 ; ::_thesis: len (mid (f,k1,k2)) >= 0 + 1
then len (mid (f,k1,k2)) = (k2 -' k1) + 1 by A6, A11, JORDAN4:8;
hence len (mid (f,k1,k2)) >= 0 + 1 by XREAL_1:6; ::_thesis: verum
end;
suppose k1 > k2 ; ::_thesis: len (mid (f,k1,k2)) >= 0 + 1
then len (mid (f,k1,k2)) = (k1 -' k2) + 1 by A12, A14, JORDAN4:9;
hence len (mid (f,k1,k2)) >= 0 + 1 by XREAL_1:6; ::_thesis: verum
end;
end;
end;
A16: Values G = { (G * (i,j)) where i, j is Element of NAT : [i,j] in Indices G } by MATRIX_1:45;
A17: proj1 .: (Values G) c= proj1 .: (rng (mid (f,k1,k2)))
proof
assume not proj1 .: (Values G) c= proj1 .: (rng (mid (f,k1,k2))) ; ::_thesis: contradiction
then consider x being Element of REAL such that
A18: x in proj1 .: (Values G) and
A19: not x in proj1 .: (rng (mid (f,k1,k2))) by SUBSET_1:2;
consider p being Element of (TOP-REAL 2) such that
A20: p in Values G and
A21: x = proj1 . p by A18, FUNCT_2:65;
consider i0, j0 being Element of NAT such that
A22: p = G * (i0,j0) and
A23: [i0,j0] in Indices G by A16, A20;
A24: i0 <= len G by A23, MATRIX_1:38;
defpred S1[ Nat] means ( 1 <= $1 & $1 <= len (mid (f,k1,k2)) implies for i, j being Element of NAT st [i,j] in Indices G & G * (i,j) = (mid (f,k1,k2)) . $1 holds
i < i0 );
A25: 1 <= i0 by A23, MATRIX_1:38;
A26: ( 1 <= j0 & j0 <= width G ) by A23, MATRIX_1:38;
A27: for n being Element of NAT st S1[n] holds
S1[n + 1]
proof
let n be Element of NAT ; ::_thesis: ( S1[n] implies S1[n + 1] )
assume that
A28: ( 1 <= n & n <= len (mid (f,k1,k2)) implies for i, j being Element of NAT st [i,j] in Indices G & G * (i,j) = (mid (f,k1,k2)) . n holds
i < i0 ) and
A29: 1 <= n + 1 and
A30: n + 1 <= len (mid (f,k1,k2)) ; ::_thesis: for i, j being Element of NAT st [i,j] in Indices G & G * (i,j) = (mid (f,k1,k2)) . (n + 1) holds
i < i0
let i, j be Element of NAT ; ::_thesis: ( [i,j] in Indices G & G * (i,j) = (mid (f,k1,k2)) . (n + 1) implies i < i0 )
assume that
A31: [i,j] in Indices G and
A32: G * (i,j) = (mid (f,k1,k2)) . (n + 1) ; ::_thesis: i < i0
A33: now__::_thesis:_not_i_=_i0
A34: n + 1 in dom (mid (f,k1,k2)) by A29, A30, FINSEQ_3:25;
then A35: G * (i,j) = (mid (f,k1,k2)) /. (n + 1) by A32, PARTFUN1:def_6;
then A36: ( dom proj1 = the carrier of (TOP-REAL 2) & (mid (f,k1,k2)) /. (n + 1) in rng (mid (f,k1,k2)) ) by A32, A34, FUNCT_1:3, FUNCT_2:def_1;
A37: ( 1 <= j & j <= width G ) by A31, MATRIX_1:38;
assume A38: i = i0 ; ::_thesis: contradiction
x = p `1 by A21, PSCOMP_1:def_5
.= (G * (i0,1)) `1 by A22, A25, A24, A26, GOBOARD5:2
.= (G * (i,j)) `1 by A25, A24, A38, A37, GOBOARD5:2
.= proj1 . ((mid (f,k1,k2)) /. (n + 1)) by A35, PSCOMP_1:def_5 ;
hence contradiction by A19, A36, FUNCT_1:def_6; ::_thesis: verum
end;
percases ( n = 0 or n <> 0 ) ;
suppose n = 0 ; ::_thesis: i < i0
then G * (i,j) = G * (1,i1) by A5, A6, A12, A14, A11, A32, FINSEQ_6:118;
then i = 1 by A2, A31, Th26;
hence i < i0 by A25, A33, XXREAL_0:1; ::_thesis: verum
end;
supposeA39: n <> 0 ; ::_thesis: i < i0
then A40: 1 <= n by NAT_1:14;
A41: n <= n + 1 by NAT_1:11;
then n <= len (mid (f,k1,k2)) by A30, XXREAL_0:2;
then A42: n in dom (mid (f,k1,k2)) by A40, FINSEQ_3:25;
then consider i1, j1 being Element of NAT such that
A43: ( [i1,j1] in Indices G & (mid (f,k1,k2)) /. n = G * (i1,j1) ) by A13, GOBOARD1:def_9;
A44: n + 1 in dom (mid (f,k1,k2)) by A29, A30, FINSEQ_3:25;
then (mid (f,k1,k2)) /. (n + 1) = G * (i,j) by A32, PARTFUN1:def_6;
then (abs (i1 - i)) + (abs (j1 - j)) = 1 by A13, A31, A42, A43, A44, GOBOARD1:def_9;
then A45: ( ( abs (i1 - i) = 1 & j1 = j ) or ( abs (j1 - j) = 1 & i1 = i ) ) by SEQM_3:42;
now__::_thesis:_i_<_i0
(mid (f,k1,k2)) . n = (mid (f,k1,k2)) /. n by A42, PARTFUN1:def_6;
then A46: i1 < i0 by A28, A30, A39, A41, A43, NAT_1:14, XXREAL_0:2;
percases ( i1 = i or i < i1 or i = i1 + 1 ) by A45, SEQM_3:41;
suppose ( i1 = i or i < i1 ) ; ::_thesis: i < i0
hence i < i0 by A46, XXREAL_0:2; ::_thesis: verum
end;
suppose i = i1 + 1 ; ::_thesis: i < i0
then i <= i0 by A46, NAT_1:13;
hence i < i0 by A33, XXREAL_0:1; ::_thesis: verum
end;
end;
end;
hence i < i0 ; ::_thesis: verum
end;
end;
end;
A47: G * ((len G),i2) = (mid (f,k1,k2)) . (len (mid (f,k1,k2))) by A6, A12, A10, A14, A11, JORDAN4:11;
A48: S1[ 0 ] ;
for n being Element of NAT holds S1[n] from NAT_1:sch_1(A48, A27);
then len G < i0 by A7, A15, A47;
hence contradiction by A23, MATRIX_1:38; ::_thesis: verum
end;
thus proj1 .: (rng f) c= proj1 .: (Values G) by A1, GOBRD13:8, RELAT_1:123; :: according to XBOOLE_0:def_10 ::_thesis: proj1 .: (Values G) c= proj1 .: (rng f)
proj1 .: (rng (mid (f,k1,k2))) c= proj1 .: (rng f) by FINSEQ_6:119, RELAT_1:123;
hence proj1 .: (Values G) c= proj1 .: (rng f) by A17, XBOOLE_1:1; ::_thesis: verum
end;
theorem Th31: :: JORDAN1H:31
for f being non empty FinSequence of (TOP-REAL 2)
for G being Go-board st f is_sequence_on G & ex i being Element of NAT st
( [i,1] in Indices G & G * (i,1) in rng f ) & ex i being Element of NAT st
( [i,(width G)] in Indices G & G * (i,(width G)) in rng f ) holds
proj2 .: (rng f) = proj2 .: (Values G)
proof
let f be non empty FinSequence of (TOP-REAL 2); ::_thesis: for G being Go-board st f is_sequence_on G & ex i being Element of NAT st
( [i,1] in Indices G & G * (i,1) in rng f ) & ex i being Element of NAT st
( [i,(width G)] in Indices G & G * (i,(width G)) in rng f ) holds
proj2 .: (rng f) = proj2 .: (Values G)
let G be Go-board; ::_thesis: ( f is_sequence_on G & ex i being Element of NAT st
( [i,1] in Indices G & G * (i,1) in rng f ) & ex i being Element of NAT st
( [i,(width G)] in Indices G & G * (i,(width G)) in rng f ) implies proj2 .: (rng f) = proj2 .: (Values G) )
assume A1: f is_sequence_on G ; ::_thesis: ( for i being Element of NAT holds
( not [i,1] in Indices G or not G * (i,1) in rng f ) or for i being Element of NAT holds
( not [i,(width G)] in Indices G or not G * (i,(width G)) in rng f ) or proj2 .: (rng f) = proj2 .: (Values G) )
given i1 being Element of NAT such that A2: [i1,1] in Indices G and
A3: G * (i1,1) in rng f ; ::_thesis: ( for i being Element of NAT holds
( not [i,(width G)] in Indices G or not G * (i,(width G)) in rng f ) or proj2 .: (rng f) = proj2 .: (Values G) )
consider k1 being set such that
A4: k1 in dom f and
A5: G * (i1,1) = f . k1 by A3, FUNCT_1:def_3;
reconsider k1 = k1 as Element of NAT by A4;
A6: 1 <= k1 by A4, FINSEQ_3:25;
given i2 being Element of NAT such that A7: [i2,(width G)] in Indices G and
A8: G * (i2,(width G)) in rng f ; ::_thesis: proj2 .: (rng f) = proj2 .: (Values G)
consider k2 being set such that
A9: k2 in dom f and
A10: G * (i2,(width G)) = f . k2 by A8, FUNCT_1:def_3;
reconsider k2 = k2 as Element of NAT by A9;
A11: k2 <= len f by A9, FINSEQ_3:25;
A12: k1 <= len f by A4, FINSEQ_3:25;
set g = mid (f,k1,k2);
A13: mid (f,k1,k2) is_sequence_on G by A1, Th27;
A14: 1 <= k2 by A9, FINSEQ_3:25;
A15: now__::_thesis:_len_(mid_(f,k1,k2))_>=_0_+_1
percases ( k1 <= k2 or k1 > k2 ) ;
suppose k1 <= k2 ; ::_thesis: len (mid (f,k1,k2)) >= 0 + 1
then len (mid (f,k1,k2)) = (k2 -' k1) + 1 by A6, A11, JORDAN4:8;
hence len (mid (f,k1,k2)) >= 0 + 1 by XREAL_1:6; ::_thesis: verum
end;
suppose k1 > k2 ; ::_thesis: len (mid (f,k1,k2)) >= 0 + 1
then len (mid (f,k1,k2)) = (k1 -' k2) + 1 by A12, A14, JORDAN4:9;
hence len (mid (f,k1,k2)) >= 0 + 1 by XREAL_1:6; ::_thesis: verum
end;
end;
end;
A16: Values G = { (G * (i,j)) where i, j is Element of NAT : [i,j] in Indices G } by MATRIX_1:45;
A17: proj2 .: (Values G) c= proj2 .: (rng (mid (f,k1,k2)))
proof
assume not proj2 .: (Values G) c= proj2 .: (rng (mid (f,k1,k2))) ; ::_thesis: contradiction
then consider x being Element of REAL such that
A18: x in proj2 .: (Values G) and
A19: not x in proj2 .: (rng (mid (f,k1,k2))) by SUBSET_1:2;
consider p being Element of (TOP-REAL 2) such that
A20: p in Values G and
A21: x = proj2 . p by A18, FUNCT_2:65;
consider i0, j0 being Element of NAT such that
A22: p = G * (i0,j0) and
A23: [i0,j0] in Indices G by A16, A20;
A24: j0 <= width G by A23, MATRIX_1:38;
defpred S1[ Nat] means ( 1 <= $1 & $1 <= len (mid (f,k1,k2)) implies for i, j being Element of NAT st [i,j] in Indices G & G * (i,j) = (mid (f,k1,k2)) . $1 holds
j < j0 );
A25: 1 <= j0 by A23, MATRIX_1:38;
A26: ( 1 <= i0 & i0 <= len G ) by A23, MATRIX_1:38;
A27: for n being Element of NAT st S1[n] holds
S1[n + 1]
proof
let n be Element of NAT ; ::_thesis: ( S1[n] implies S1[n + 1] )
assume that
A28: ( 1 <= n & n <= len (mid (f,k1,k2)) implies for i, j being Element of NAT st [i,j] in Indices G & G * (i,j) = (mid (f,k1,k2)) . n holds
j < j0 ) and
A29: 1 <= n + 1 and
A30: n + 1 <= len (mid (f,k1,k2)) ; ::_thesis: for i, j being Element of NAT st [i,j] in Indices G & G * (i,j) = (mid (f,k1,k2)) . (n + 1) holds
j < j0
let i, j be Element of NAT ; ::_thesis: ( [i,j] in Indices G & G * (i,j) = (mid (f,k1,k2)) . (n + 1) implies j < j0 )
assume that
A31: [i,j] in Indices G and
A32: G * (i,j) = (mid (f,k1,k2)) . (n + 1) ; ::_thesis: j < j0
A33: now__::_thesis:_not_j_=_j0
A34: n + 1 in dom (mid (f,k1,k2)) by A29, A30, FINSEQ_3:25;
then A35: G * (i,j) = (mid (f,k1,k2)) /. (n + 1) by A32, PARTFUN1:def_6;
then A36: ( dom proj2 = the carrier of (TOP-REAL 2) & (mid (f,k1,k2)) /. (n + 1) in rng (mid (f,k1,k2)) ) by A32, A34, FUNCT_1:3, FUNCT_2:def_1;
A37: ( 1 <= i & i <= len G ) by A31, MATRIX_1:38;
assume A38: j = j0 ; ::_thesis: contradiction
x = p `2 by A21, PSCOMP_1:def_6
.= (G * (1,j0)) `2 by A22, A26, A25, A24, GOBOARD5:1
.= (G * (i,j)) `2 by A25, A24, A38, A37, GOBOARD5:1
.= proj2 . ((mid (f,k1,k2)) /. (n + 1)) by A35, PSCOMP_1:def_6 ;
hence contradiction by A19, A36, FUNCT_1:def_6; ::_thesis: verum
end;
percases ( n = 0 or n <> 0 ) ;
suppose n = 0 ; ::_thesis: j < j0
then G * (i,j) = G * (i1,1) by A5, A6, A12, A14, A11, A32, FINSEQ_6:118;
then j = 1 by A2, A31, Th26;
hence j < j0 by A25, A33, XXREAL_0:1; ::_thesis: verum
end;
supposeA39: n <> 0 ; ::_thesis: j < j0
then A40: 1 <= n by NAT_1:14;
A41: n <= n + 1 by NAT_1:11;
then n <= len (mid (f,k1,k2)) by A30, XXREAL_0:2;
then A42: n in dom (mid (f,k1,k2)) by A40, FINSEQ_3:25;
then consider i1, j1 being Element of NAT such that
A43: ( [i1,j1] in Indices G & (mid (f,k1,k2)) /. n = G * (i1,j1) ) by A13, GOBOARD1:def_9;
A44: n + 1 in dom (mid (f,k1,k2)) by A29, A30, FINSEQ_3:25;
then (mid (f,k1,k2)) /. (n + 1) = G * (i,j) by A32, PARTFUN1:def_6;
then (abs (i1 - i)) + (abs (j1 - j)) = 1 by A13, A31, A42, A43, A44, GOBOARD1:def_9;
then A45: ( ( abs (i1 - i) = 1 & j1 = j ) or ( abs (j1 - j) = 1 & i1 = i ) ) by SEQM_3:42;
now__::_thesis:_j_<_j0
(mid (f,k1,k2)) . n = (mid (f,k1,k2)) /. n by A42, PARTFUN1:def_6;
then A46: j1 < j0 by A28, A30, A39, A41, A43, NAT_1:14, XXREAL_0:2;
percases ( j1 = j or j < j1 or j = j1 + 1 ) by A45, SEQM_3:41;
suppose ( j1 = j or j < j1 ) ; ::_thesis: j < j0
hence j < j0 by A46, XXREAL_0:2; ::_thesis: verum
end;
suppose j = j1 + 1 ; ::_thesis: j < j0
then j <= j0 by A46, NAT_1:13;
hence j < j0 by A33, XXREAL_0:1; ::_thesis: verum
end;
end;
end;
hence j < j0 ; ::_thesis: verum
end;
end;
end;
A47: G * (i2,(width G)) = (mid (f,k1,k2)) . (len (mid (f,k1,k2))) by A6, A12, A10, A14, A11, JORDAN4:11;
A48: S1[ 0 ] ;
for n being Element of NAT holds S1[n] from NAT_1:sch_1(A48, A27);
then width G < j0 by A7, A15, A47;
hence contradiction by A23, MATRIX_1:38; ::_thesis: verum
end;
thus proj2 .: (rng f) c= proj2 .: (Values G) by A1, GOBRD13:8, RELAT_1:123; :: according to XBOOLE_0:def_10 ::_thesis: proj2 .: (Values G) c= proj2 .: (rng f)
proj2 .: (rng (mid (f,k1,k2))) c= proj2 .: (rng f) by FINSEQ_6:119, RELAT_1:123;
hence proj2 .: (Values G) c= proj2 .: (rng f) by A17, XBOOLE_1:1; ::_thesis: verum
end;
registration
let G be Go-board;
cluster Values G -> non empty ;
coherence
not Values G is empty
proof
not dom G is empty ;
then reconsider f = rngs G as non empty non-empty Function by FUNCT_6:60, RELAT_1:38;
not Union f is empty ;
hence not Values G is empty by MATRIX_1:def_16; ::_thesis: verum
end;
end;
theorem Th32: :: JORDAN1H:32
for G being Go-board holds G = GoB ((SgmX (RealOrd,(proj1 .: (Values G)))),(SgmX (RealOrd,(proj2 .: (Values G)))))
proof
let G be Go-board; ::_thesis: G = GoB ((SgmX (RealOrd,(proj1 .: (Values G)))),(SgmX (RealOrd,(proj2 .: (Values G)))))
set v1 = SgmX (RealOrd,(proj1 .: (Values G)));
set v2 = SgmX (RealOrd,(proj2 .: (Values G)));
A1: width G = card (proj2 .: (Values G)) by Th19
.= len (SgmX (RealOrd,(proj2 .: (Values G)))) by Th9 ;
A2: for n, m being Element of NAT st [n,m] in Indices G holds
G * (n,m) = |[((SgmX (RealOrd,(proj1 .: (Values G)))) . n),((SgmX (RealOrd,(proj2 .: (Values G)))) . m)]|
proof
let n, m be Element of NAT ; ::_thesis: ( [n,m] in Indices G implies G * (n,m) = |[((SgmX (RealOrd,(proj1 .: (Values G)))) . n),((SgmX (RealOrd,(proj2 .: (Values G)))) . m)]| )
assume A3: [n,m] in Indices G ; ::_thesis: G * (n,m) = |[((SgmX (RealOrd,(proj1 .: (Values G)))) . n),((SgmX (RealOrd,(proj2 .: (Values G)))) . m)]|
then A4: ( 1 <= n & n <= len G ) by MATRIX_1:38;
A5: ( 1 <= m & m <= width G ) by A3, MATRIX_1:38;
(SgmX (RealOrd,(proj1 .: (Values G)))) . n = (G * (n,1)) `1 by A4, Th28;
then A6: (SgmX (RealOrd,(proj1 .: (Values G)))) . n = (G * (n,m)) `1 by A4, A5, GOBOARD5:2;
(SgmX (RealOrd,(proj2 .: (Values G)))) . m = (G * (1,m)) `2 by A5, Th29;
then (SgmX (RealOrd,(proj2 .: (Values G)))) . m = (G * (n,m)) `2 by A4, A5, GOBOARD5:1;
hence G * (n,m) = |[((SgmX (RealOrd,(proj1 .: (Values G)))) . n),((SgmX (RealOrd,(proj2 .: (Values G)))) . m)]| by A6, EUCLID:53; ::_thesis: verum
end;
len G = card (proj1 .: (Values G)) by Th16
.= len (SgmX (RealOrd,(proj1 .: (Values G)))) by Th9 ;
hence G = GoB ((SgmX (RealOrd,(proj1 .: (Values G)))),(SgmX (RealOrd,(proj2 .: (Values G))))) by A1, A2, GOBOARD2:def_1; ::_thesis: verum
end;
theorem Th33: :: JORDAN1H:33
for f being non empty FinSequence of (TOP-REAL 2)
for G being Go-board st proj1 .: (rng f) = proj1 .: (Values G) & proj2 .: (rng f) = proj2 .: (Values G) holds
G = GoB f
proof
let f be non empty FinSequence of (TOP-REAL 2); ::_thesis: for G being Go-board st proj1 .: (rng f) = proj1 .: (Values G) & proj2 .: (rng f) = proj2 .: (Values G) holds
G = GoB f
let G be Go-board; ::_thesis: ( proj1 .: (rng f) = proj1 .: (Values G) & proj2 .: (rng f) = proj2 .: (Values G) implies G = GoB f )
X_axis f = proj1 * f by Th10;
then rng (X_axis f) = proj1 .: (rng f) by RELAT_1:127;
then A1: Incr (X_axis f) = SgmX (RealOrd,(proj1 .: (rng f))) by Th8;
Y_axis f = proj2 * f by Th11;
then rng (Y_axis f) = proj2 .: (rng f) by RELAT_1:127;
then A2: Incr (Y_axis f) = SgmX (RealOrd,(proj2 .: (rng f))) by Th8;
assume ( proj1 .: (rng f) = proj1 .: (Values G) & proj2 .: (rng f) = proj2 .: (Values G) ) ; ::_thesis: G = GoB f
hence G = GoB ((Incr (X_axis f)),(Incr (Y_axis f))) by A1, A2, Th32
.= GoB f by GOBOARD2:def_2 ;
::_thesis: verum
end;
theorem Th34: :: JORDAN1H:34
for f being non empty FinSequence of (TOP-REAL 2)
for G being Go-board st f is_sequence_on G & ex i being Element of NAT st
( [1,i] in Indices G & G * (1,i) in rng f ) & ex i being Element of NAT st
( [i,1] in Indices G & G * (i,1) in rng f ) & ex i being Element of NAT st
( [(len G),i] in Indices G & G * ((len G),i) in rng f ) & ex i being Element of NAT st
( [i,(width G)] in Indices G & G * (i,(width G)) in rng f ) holds
G = GoB f
proof
let f be non empty FinSequence of (TOP-REAL 2); ::_thesis: for G being Go-board st f is_sequence_on G & ex i being Element of NAT st
( [1,i] in Indices G & G * (1,i) in rng f ) & ex i being Element of NAT st
( [i,1] in Indices G & G * (i,1) in rng f ) & ex i being Element of NAT st
( [(len G),i] in Indices G & G * ((len G),i) in rng f ) & ex i being Element of NAT st
( [i,(width G)] in Indices G & G * (i,(width G)) in rng f ) holds
G = GoB f
let G be Go-board; ::_thesis: ( f is_sequence_on G & ex i being Element of NAT st
( [1,i] in Indices G & G * (1,i) in rng f ) & ex i being Element of NAT st
( [i,1] in Indices G & G * (i,1) in rng f ) & ex i being Element of NAT st
( [(len G),i] in Indices G & G * ((len G),i) in rng f ) & ex i being Element of NAT st
( [i,(width G)] in Indices G & G * (i,(width G)) in rng f ) implies G = GoB f )
assume A1: f is_sequence_on G ; ::_thesis: ( for i being Element of NAT holds
( not [1,i] in Indices G or not G * (1,i) in rng f ) or for i being Element of NAT holds
( not [i,1] in Indices G or not G * (i,1) in rng f ) or for i being Element of NAT holds
( not [(len G),i] in Indices G or not G * ((len G),i) in rng f ) or for i being Element of NAT holds
( not [i,(width G)] in Indices G or not G * (i,(width G)) in rng f ) or G = GoB f )
given i1 being Element of NAT such that A2: ( [1,i1] in Indices G & G * (1,i1) in rng f ) ; ::_thesis: ( for i being Element of NAT holds
( not [i,1] in Indices G or not G * (i,1) in rng f ) or for i being Element of NAT holds
( not [(len G),i] in Indices G or not G * ((len G),i) in rng f ) or for i being Element of NAT holds
( not [i,(width G)] in Indices G or not G * (i,(width G)) in rng f ) or G = GoB f )
given i2 being Element of NAT such that A3: ( [i2,1] in Indices G & G * (i2,1) in rng f ) ; ::_thesis: ( for i being Element of NAT holds
( not [(len G),i] in Indices G or not G * ((len G),i) in rng f ) or for i being Element of NAT holds
( not [i,(width G)] in Indices G or not G * (i,(width G)) in rng f ) or G = GoB f )
given i3 being Element of NAT such that A4: ( [(len G),i3] in Indices G & G * ((len G),i3) in rng f ) ; ::_thesis: ( for i being Element of NAT holds
( not [i,(width G)] in Indices G or not G * (i,(width G)) in rng f ) or G = GoB f )
given i4 being Element of NAT such that A5: ( [i4,(width G)] in Indices G & G * (i4,(width G)) in rng f ) ; ::_thesis: G = GoB f
A6: proj2 .: (rng f) = proj2 .: (Values G) by A1, A3, A5, Th31;
proj1 .: (rng f) = proj1 .: (Values G) by A1, A2, A4, Th30;
hence G = GoB f by A6, Th33; ::_thesis: verum
end;
begin
theorem Th35: :: JORDAN1H:35
for i, n, m being Element of NAT st 1 <= i holds
[\(((i - 2) / (2 |^ (n -' m))) + 2)/] is Element of NAT
proof
let i, n, m be Element of NAT ; ::_thesis: ( 1 <= i implies [\(((i - 2) / (2 |^ (n -' m))) + 2)/] is Element of NAT )
set i1 = [\(((i - 2) / (2 |^ (n -' m))) + 2)/];
(((i - 2) / (2 |^ (n -' m))) + 2) - 1 = ((i - 2) / (2 |^ (n -' m))) + (2 - 1) ;
then A1: ((i - 2) / (2 |^ (n -' m))) + 1 < [\(((i - 2) / (2 |^ (n -' m))) + 2)/] by INT_1:def_6;
( (n -' m) + 1 >= 0 + 1 & (n -' m) + 1 <= 2 |^ (n -' m) ) by NEWTON:85, XREAL_1:6;
then 0 + 1 <= 2 |^ (n -' m) by XXREAL_0:2;
then A2: (- 1) / 1 <= (- 1) / (2 |^ (n -' m)) by XREAL_1:120;
assume 1 <= i ; ::_thesis: [\(((i - 2) / (2 |^ (n -' m))) + 2)/] is Element of NAT
then 1 - 2 <= i - 2 by XREAL_1:9;
then (- 1) / (2 |^ (n -' m)) <= (i - 2) / (2 |^ (n -' m)) by XREAL_1:72;
then - 1 <= (i - 2) / (2 |^ (n -' m)) by A2, XXREAL_0:2;
then (- 1) + 1 <= ((i - 2) / (2 |^ (n -' m))) + 1 by XREAL_1:6;
hence [\(((i - 2) / (2 |^ (n -' m))) + 2)/] is Element of NAT by A1, INT_1:3; ::_thesis: verum
end;
theorem Th36: :: JORDAN1H:36
for m, n, i being Element of NAT
for C being compact non horizontal non vertical Subset of (TOP-REAL 2) st m <= n & 1 <= i & i + 1 <= len (Gauge (C,n)) holds
( 1 <= [\(((i - 2) / (2 |^ (n -' m))) + 2)/] & [\(((i - 2) / (2 |^ (n -' m))) + 2)/] + 1 <= len (Gauge (C,m)) )
proof
let m, n, i be Element of NAT ; ::_thesis: for C being compact non horizontal non vertical Subset of (TOP-REAL 2) st m <= n & 1 <= i & i + 1 <= len (Gauge (C,n)) holds
( 1 <= [\(((i - 2) / (2 |^ (n -' m))) + 2)/] & [\(((i - 2) / (2 |^ (n -' m))) + 2)/] + 1 <= len (Gauge (C,m)) )
let C be compact non horizontal non vertical Subset of (TOP-REAL 2); ::_thesis: ( m <= n & 1 <= i & i + 1 <= len (Gauge (C,n)) implies ( 1 <= [\(((i - 2) / (2 |^ (n -' m))) + 2)/] & [\(((i - 2) / (2 |^ (n -' m))) + 2)/] + 1 <= len (Gauge (C,m)) ) )
assume that
A1: m <= n and
A2: 1 <= i and
A3: i + 1 <= len (Gauge (C,n)) ; ::_thesis: ( 1 <= [\(((i - 2) / (2 |^ (n -' m))) + 2)/] & [\(((i - 2) / (2 |^ (n -' m))) + 2)/] + 1 <= len (Gauge (C,m)) )
A4: (n -' m) + 1 <= 2 |^ (n -' m) by NEWTON:85;
i + 1 <= (2 |^ n) + (2 + 1) by A3, JORDAN8:def_1;
then i + 1 <= ((2 |^ n) + 2) + 1 ;
then i <= (2 |^ n) + 2 by XREAL_1:6;
then i - 2 <= 2 |^ n by XREAL_1:20;
then i - 2 <= 2 |^ (m + (n -' m)) by A1, XREAL_1:235;
then (i - 2) * 1 <= (2 |^ m) * (2 |^ (n -' m)) by NEWTON:8;
then (i - 2) / (2 |^ (n -' m)) <= (2 |^ m) / 1 by A4, XREAL_1:102;
then ((i - 2) / (2 |^ (n -' m))) + 3 <= (2 |^ m) + 3 by XREAL_1:6;
then A5: ((i - 2) / (2 |^ (n -' m))) + 3 <= len (Gauge (C,m)) by JORDAN8:def_1;
set i1 = [\(((i - 2) / (2 |^ (n -' m))) + 2)/];
(((i - 2) / (2 |^ (n -' m))) + 2) - 1 = ((i - 2) / (2 |^ (n -' m))) + (2 - 1) ;
then A6: ((i - 2) / (2 |^ (n -' m))) + 1 < [\(((i - 2) / (2 |^ (n -' m))) + 2)/] by INT_1:def_6;
(n -' m) + 1 >= 0 + 1 by XREAL_1:6;
then 0 + 1 <= 2 |^ (n -' m) by A4, XXREAL_0:2;
then A7: (- 1) / 1 <= (- 1) / (2 |^ (n -' m)) by XREAL_1:120;
1 - 2 <= i - 2 by A2, XREAL_1:9;
then (- 1) / (2 |^ (n -' m)) <= (i - 2) / (2 |^ (n -' m)) by XREAL_1:72;
then - 1 <= (i - 2) / (2 |^ (n -' m)) by A7, XXREAL_0:2;
then (- 1) + 1 <= ((i - 2) / (2 |^ (n -' m))) + 1 by XREAL_1:6;
then [\(((i - 2) / (2 |^ (n -' m))) + 2)/] >= 1 + 0 by A6, INT_1:7;
hence 1 <= [\(((i - 2) / (2 |^ (n -' m))) + 2)/] ; ::_thesis: [\(((i - 2) / (2 |^ (n -' m))) + 2)/] + 1 <= len (Gauge (C,m))
[\(((i - 2) / (2 |^ (n -' m))) + 2)/] <= ((i - 2) / (2 |^ (n -' m))) + 2 by INT_1:def_6;
then [\(((i - 2) / (2 |^ (n -' m))) + 2)/] + 1 <= (((i - 2) / (2 |^ (n -' m))) + 2) + 1 by XREAL_1:6;
hence [\(((i - 2) / (2 |^ (n -' m))) + 2)/] + 1 <= len (Gauge (C,m)) by A5, XXREAL_0:2; ::_thesis: verum
end;
theorem Th37: :: JORDAN1H:37
for m, n, i, j being Element of NAT
for C being compact non horizontal non vertical Subset of (TOP-REAL 2) st m <= n & 1 <= i & i + 1 <= len (Gauge (C,n)) & 1 <= j & j + 1 <= width (Gauge (C,n)) holds
ex i1, j1 being Element of NAT st
( i1 = [\(((i - 2) / (2 |^ (n -' m))) + 2)/] & j1 = [\(((j - 2) / (2 |^ (n -' m))) + 2)/] & cell ((Gauge (C,n)),i,j) c= cell ((Gauge (C,m)),i1,j1) )
proof
let m, n, i, j be Element of NAT ; ::_thesis: for C being compact non horizontal non vertical Subset of (TOP-REAL 2) st m <= n & 1 <= i & i + 1 <= len (Gauge (C,n)) & 1 <= j & j + 1 <= width (Gauge (C,n)) holds
ex i1, j1 being Element of NAT st
( i1 = [\(((i - 2) / (2 |^ (n -' m))) + 2)/] & j1 = [\(((j - 2) / (2 |^ (n -' m))) + 2)/] & cell ((Gauge (C,n)),i,j) c= cell ((Gauge (C,m)),i1,j1) )
let C be compact non horizontal non vertical Subset of (TOP-REAL 2); ::_thesis: ( m <= n & 1 <= i & i + 1 <= len (Gauge (C,n)) & 1 <= j & j + 1 <= width (Gauge (C,n)) implies ex i1, j1 being Element of NAT st
( i1 = [\(((i - 2) / (2 |^ (n -' m))) + 2)/] & j1 = [\(((j - 2) / (2 |^ (n -' m))) + 2)/] & cell ((Gauge (C,n)),i,j) c= cell ((Gauge (C,m)),i1,j1) ) )
assume that
A1: m <= n and
A2: 1 <= i and
A3: i + 1 <= len (Gauge (C,n)) and
A4: 1 <= j and
A5: j + 1 <= width (Gauge (C,n)) ; ::_thesis: ex i1, j1 being Element of NAT st
( i1 = [\(((i - 2) / (2 |^ (n -' m))) + 2)/] & j1 = [\(((j - 2) / (2 |^ (n -' m))) + 2)/] & cell ((Gauge (C,n)),i,j) c= cell ((Gauge (C,m)),i1,j1) )
reconsider i1 = [\(((i - 2) / (2 |^ (n -' m))) + 2)/], j1 = [\(((j - 2) / (2 |^ (n -' m))) + 2)/] as Element of NAT by A2, A4, Th35;
set Gm = Gauge (C,m);
set Gn = Gauge (C,n);
A6: 2 |^ (n -' m) > n -' m by NEWTON:86;
take i1 ; ::_thesis: ex j1 being Element of NAT st
( i1 = [\(((i - 2) / (2 |^ (n -' m))) + 2)/] & j1 = [\(((j - 2) / (2 |^ (n -' m))) + 2)/] & cell ((Gauge (C,n)),i,j) c= cell ((Gauge (C,m)),i1,j1) )
take j1 ; ::_thesis: ( i1 = [\(((i - 2) / (2 |^ (n -' m))) + 2)/] & j1 = [\(((j - 2) / (2 |^ (n -' m))) + 2)/] & cell ((Gauge (C,n)),i,j) c= cell ((Gauge (C,m)),i1,j1) )
thus i1 = [\(((i - 2) / (2 |^ (n -' m))) + 2)/] ; ::_thesis: ( j1 = [\(((j - 2) / (2 |^ (n -' m))) + 2)/] & cell ((Gauge (C,n)),i,j) c= cell ((Gauge (C,m)),i1,j1) )
thus j1 = [\(((j - 2) / (2 |^ (n -' m))) + 2)/] ; ::_thesis: cell ((Gauge (C,n)),i,j) c= cell ((Gauge (C,m)),i1,j1)
let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in cell ((Gauge (C,n)),i,j) or e in cell ((Gauge (C,m)),i1,j1) )
assume A7: e in cell ((Gauge (C,n)),i,j) ; ::_thesis: e in cell ((Gauge (C,m)),i1,j1)
then reconsider p = e as Point of (TOP-REAL 2) ;
A8: p `2 <= ((Gauge (C,n)) * (i,(j + 1))) `2 by A2, A3, A4, A5, A7, JORDAN9:17;
( i <= len (Gauge (C,n)) & j <= width (Gauge (C,n)) ) by A3, A5, NAT_1:13;
then [i,j] in Indices (Gauge (C,n)) by A2, A4, MATRIX_1:36;
then A9: (Gauge (C,n)) * (i,j) = |[((W-bound C) + ((((E-bound C) - (W-bound C)) / (2 |^ n)) * (i - 2))),((S-bound C) + ((((N-bound C) - (S-bound C)) / (2 |^ n)) * (j - 2)))]| by JORDAN8:def_1;
then A10: ((Gauge (C,n)) * (i,j)) `1 = (W-bound C) + ((((E-bound C) - (W-bound C)) / (2 |^ n)) * ((i - 2) / 1)) by EUCLID:52
.= (W-bound C) + ((((E-bound C) - (W-bound C)) / 1) * ((i - 2) / (2 |^ n))) by XCMPLX_1:85 ;
A11: ((Gauge (C,n)) * (i,j)) `1 <= p `1 by A2, A3, A4, A5, A7, JORDAN9:17;
A12: ((Gauge (C,n)) * (i,j)) `2 = (S-bound C) + ((((N-bound C) - (S-bound C)) / (2 |^ n)) * ((j - 2) / 1)) by A9, EUCLID:52
.= (S-bound C) + ((((N-bound C) - (S-bound C)) / 1) * ((j - 2) / (2 |^ n))) by XCMPLX_1:85 ;
A13: p `1 <= ((Gauge (C,n)) * ((i + 1),j)) `1 by A2, A3, A4, A5, A7, JORDAN9:17;
E-bound C >= (W-bound C) + 0 by SPRECT_1:21;
then A14: (E-bound C) - (W-bound C) >= 0 by XREAL_1:19;
( 1 <= j + 1 & i <= len (Gauge (C,n)) ) by A3, NAT_1:11, NAT_1:13;
then [i,(j + 1)] in Indices (Gauge (C,n)) by A2, A5, MATRIX_1:36;
then (Gauge (C,n)) * (i,(j + 1)) = |[((W-bound C) + ((((E-bound C) - (W-bound C)) / (2 |^ n)) * (i - 2))),((S-bound C) + ((((N-bound C) - (S-bound C)) / (2 |^ n)) * ((j + 1) - 2)))]| by JORDAN8:def_1;
then A15: ((Gauge (C,n)) * (i,(j + 1))) `2 = (S-bound C) + ((((N-bound C) - (S-bound C)) / (2 |^ n)) * (((j + 1) - 2) / 1)) by EUCLID:52
.= (S-bound C) + ((((N-bound C) - (S-bound C)) / 1) * (((j + 1) - 2) / (2 |^ n))) by XCMPLX_1:85 ;
( (n -' m) + 1 >= 0 + 1 & (n -' m) + 1 <= 2 |^ (n -' m) ) by NEWTON:85, XREAL_1:6;
then 0 + 1 <= 2 |^ (n -' m) by XXREAL_0:2;
then A16: (- 1) / 1 <= (- 1) / (2 |^ (n -' m)) by XREAL_1:120;
A17: ((Gauge (C,n)) * (i,j)) `2 <= p `2 by A2, A3, A4, A5, A7, JORDAN9:17;
( 1 <= i + 1 & j <= width (Gauge (C,n)) ) by A5, NAT_1:11, NAT_1:13;
then [(i + 1),j] in Indices (Gauge (C,n)) by A3, A4, MATRIX_1:36;
then (Gauge (C,n)) * ((i + 1),j) = |[((W-bound C) + ((((E-bound C) - (W-bound C)) / (2 |^ n)) * ((i + 1) - 2))),((S-bound C) + ((((N-bound C) - (S-bound C)) / (2 |^ n)) * (j - 2)))]| by JORDAN8:def_1;
then A18: ((Gauge (C,n)) * ((i + 1),j)) `1 = (W-bound C) + ((((E-bound C) - (W-bound C)) / (2 |^ n)) * (((i + 1) - 2) / 1)) by EUCLID:52
.= (W-bound C) + ((((E-bound C) - (W-bound C)) / 1) * (((i + 1) - 2) / (2 |^ n))) by XCMPLX_1:85 ;
(((i - 2) / (2 |^ (n -' m))) + 2) - 1 = ((i - 2) / (2 |^ (n -' m))) + (2 - 1) ;
then A19: ((i - 2) / (2 |^ (n -' m))) + 1 < i1 by INT_1:def_6;
1 - 2 <= i - 2 by A2, XREAL_1:9;
then (- 1) / (2 |^ (n -' m)) <= (i - 2) / (2 |^ (n -' m)) by XREAL_1:72;
then - 1 <= (i - 2) / (2 |^ (n -' m)) by A16, XXREAL_0:2;
then (- 1) + 1 <= ((i - 2) / (2 |^ (n -' m))) + 1 by XREAL_1:6;
then A20: i1 >= 1 + 0 by A19, INT_1:7;
N-bound C >= (S-bound C) + 0 by SPRECT_1:22;
then A21: (N-bound C) - (S-bound C) >= 0 by XREAL_1:19;
(((i - 2) / (2 |^ (n -' m))) + 2) - 1 < i1 by INT_1:def_6;
then ((i - 2) / (2 |^ (n -' m))) + 2 < i1 + 1 by XREAL_1:19;
then (i - 2) / (2 |^ (n -' m)) < (i1 + 1) - 2 by XREAL_1:20;
then (i - 2) + 1 <= ((i1 + 1) - 2) * (2 |^ (n -' m)) by A6, INT_1:7, XREAL_1:77;
then ((i + 1) - 2) / (2 |^ (n -' m)) <= (i1 + 1) - 2 by A6, XREAL_1:79;
then (((i + 1) - 2) / (2 |^ (n -' m))) / (2 |^ m) <= ((i1 + 1) - 2) / (2 |^ m) by XREAL_1:72;
then ((i + 1) - 2) / ((2 |^ (n -' m)) * (2 |^ m)) <= ((i1 + 1) - 2) / (2 |^ m) by XCMPLX_1:78;
then ((i + 1) - 2) / (2 |^ ((n -' m) + m)) <= ((i1 + 1) - 2) / (2 |^ m) by NEWTON:8;
then ((i + 1) - 2) / (2 |^ n) <= ((i1 + 1) - 2) / (2 |^ m) by A1, XREAL_1:235;
then A22: ((E-bound C) - (W-bound C)) * (((i + 1) - 2) / (2 |^ n)) <= ((E-bound C) - (W-bound C)) * (((i1 + 1) - 2) / (2 |^ m)) by A14, XREAL_1:64;
i1 <= ((i - 2) / (2 |^ (n -' m))) + 2 by INT_1:def_6;
then i1 - 2 <= (i - 2) / (2 |^ (n -' m)) by XREAL_1:20;
then (i1 - 2) / (2 |^ m) <= ((i - 2) / (2 |^ (n -' m))) / (2 |^ m) by XREAL_1:72;
then (i1 - 2) / (2 |^ m) <= (i - 2) / ((2 |^ (n -' m)) * (2 |^ m)) by XCMPLX_1:78;
then (i1 - 2) / (2 |^ m) <= (i - 2) / (2 |^ ((n -' m) + m)) by NEWTON:8;
then (i1 - 2) / (2 |^ m) <= (i - 2) / (2 |^ n) by A1, XREAL_1:235;
then A23: ((E-bound C) - (W-bound C)) * ((i1 - 2) / (2 |^ m)) <= ((E-bound C) - (W-bound C)) * ((i - 2) / (2 |^ n)) by A14, XREAL_1:64;
j1 <= ((j - 2) / (2 |^ (n -' m))) + 2 by INT_1:def_6;
then j1 - 2 <= (j - 2) / (2 |^ (n -' m)) by XREAL_1:20;
then (j1 - 2) / (2 |^ m) <= ((j - 2) / (2 |^ (n -' m))) / (2 |^ m) by XREAL_1:72;
then (j1 - 2) / (2 |^ m) <= (j - 2) / ((2 |^ (n -' m)) * (2 |^ m)) by XCMPLX_1:78;
then (j1 - 2) / (2 |^ m) <= (j - 2) / (2 |^ ((n -' m) + m)) by NEWTON:8;
then (j1 - 2) / (2 |^ m) <= (j - 2) / (2 |^ n) by A1, XREAL_1:235;
then A24: ((N-bound C) - (S-bound C)) * ((j1 - 2) / (2 |^ m)) <= ((N-bound C) - (S-bound C)) * ((j - 2) / (2 |^ n)) by A21, XREAL_1:64;
(((j - 2) / (2 |^ (n -' m))) + 2) - 1 = ((j - 2) / (2 |^ (n -' m))) + (2 - 1) ;
then A25: ((j - 2) / (2 |^ (n -' m))) + 1 < j1 by INT_1:def_6;
1 - 2 <= j - 2 by A4, XREAL_1:9;
then (- 1) / (2 |^ (n -' m)) <= (j - 2) / (2 |^ (n -' m)) by XREAL_1:72;
then - 1 <= (j - 2) / (2 |^ (n -' m)) by A16, XXREAL_0:2;
then (- 1) + 1 <= ((j - 2) / (2 |^ (n -' m))) + 1 by XREAL_1:6;
then A26: j1 >= 1 + 0 by A25, INT_1:7;
(((j - 2) / (2 |^ (n -' m))) + 2) - 1 < j1 by INT_1:def_6;
then ((j - 2) / (2 |^ (n -' m))) + 2 < j1 + 1 by XREAL_1:19;
then (j - 2) / (2 |^ (n -' m)) < (j1 + 1) - 2 by XREAL_1:20;
then (j - 2) + 1 <= ((j1 + 1) - 2) * (2 |^ (n -' m)) by A6, INT_1:7, XREAL_1:77;
then ((j + 1) - 2) / (2 |^ (n -' m)) <= (j1 + 1) - 2 by A6, XREAL_1:79;
then (((j + 1) - 2) / (2 |^ (n -' m))) / (2 |^ m) <= ((j1 + 1) - 2) / (2 |^ m) by XREAL_1:72;
then ((j + 1) - 2) / ((2 |^ (n -' m)) * (2 |^ m)) <= ((j1 + 1) - 2) / (2 |^ m) by XCMPLX_1:78;
then ((j + 1) - 2) / (2 |^ ((n -' m) + m)) <= ((j1 + 1) - 2) / (2 |^ m) by NEWTON:8;
then ((j + 1) - 2) / (2 |^ n) <= ((j1 + 1) - 2) / (2 |^ m) by A1, XREAL_1:235;
then A27: ((N-bound C) - (S-bound C)) * (((j + 1) - 2) / (2 |^ n)) <= ((N-bound C) - (S-bound C)) * (((j1 + 1) - 2) / (2 |^ m)) by A21, XREAL_1:64;
( len (Gauge (C,m)) = width (Gauge (C,m)) & len (Gauge (C,n)) = width (Gauge (C,n)) ) by JORDAN8:def_1;
then A28: j1 + 1 <= width (Gauge (C,m)) by A1, A4, A5, Th36;
then A29: j1 <= width (Gauge (C,m)) by NAT_1:13;
A30: i1 + 1 <= len (Gauge (C,m)) by A1, A2, A3, Th36;
then ( 1 <= j1 + 1 & i1 <= len (Gauge (C,m)) ) by NAT_1:11, NAT_1:13;
then [i1,(j1 + 1)] in Indices (Gauge (C,m)) by A20, A28, MATRIX_1:36;
then (Gauge (C,m)) * (i1,(j1 + 1)) = |[((W-bound C) + ((((E-bound C) - (W-bound C)) / (2 |^ m)) * (i1 - 2))),((S-bound C) + ((((N-bound C) - (S-bound C)) / (2 |^ m)) * ((j1 + 1) - 2)))]| by JORDAN8:def_1;
then ((Gauge (C,m)) * (i1,(j1 + 1))) `2 = (S-bound C) + ((((N-bound C) - (S-bound C)) / (2 |^ m)) * (((j1 + 1) - 2) / 1)) by EUCLID:52
.= (S-bound C) + ((((N-bound C) - (S-bound C)) / 1) * (((j1 + 1) - 2) / (2 |^ m))) by XCMPLX_1:85 ;
then ((Gauge (C,n)) * (i,(j + 1))) `2 <= ((Gauge (C,m)) * (i1,(j1 + 1))) `2 by A15, A27, XREAL_1:6;
then A31: p `2 <= ((Gauge (C,m)) * (i1,(j1 + 1))) `2 by A8, XXREAL_0:2;
i1 <= len (Gauge (C,m)) by A30, NAT_1:13;
then [i1,j1] in Indices (Gauge (C,m)) by A20, A26, A29, MATRIX_1:36;
then A32: (Gauge (C,m)) * (i1,j1) = |[((W-bound C) + ((((E-bound C) - (W-bound C)) / (2 |^ m)) * (i1 - 2))),((S-bound C) + ((((N-bound C) - (S-bound C)) / (2 |^ m)) * (j1 - 2)))]| by JORDAN8:def_1;
then ((Gauge (C,m)) * (i1,j1)) `1 = (W-bound C) + ((((E-bound C) - (W-bound C)) / (2 |^ m)) * ((i1 - 2) / 1)) by EUCLID:52
.= (W-bound C) + ((((E-bound C) - (W-bound C)) / 1) * ((i1 - 2) / (2 |^ m))) by XCMPLX_1:85 ;
then ((Gauge (C,m)) * (i1,j1)) `1 <= ((Gauge (C,n)) * (i,j)) `1 by A10, A23, XREAL_1:6;
then A33: ((Gauge (C,m)) * (i1,j1)) `1 <= p `1 by A11, XXREAL_0:2;
((Gauge (C,m)) * (i1,j1)) `2 = (S-bound C) + ((((N-bound C) - (S-bound C)) / (2 |^ m)) * ((j1 - 2) / 1)) by A32, EUCLID:52
.= (S-bound C) + ((((N-bound C) - (S-bound C)) / 1) * ((j1 - 2) / (2 |^ m))) by XCMPLX_1:85 ;
then ((Gauge (C,m)) * (i1,j1)) `2 <= ((Gauge (C,n)) * (i,j)) `2 by A12, A24, XREAL_1:6;
then A34: ((Gauge (C,m)) * (i1,j1)) `2 <= p `2 by A17, XXREAL_0:2;
( 1 <= i1 + 1 & j1 <= width (Gauge (C,m)) ) by A28, NAT_1:11, NAT_1:13;
then [(i1 + 1),j1] in Indices (Gauge (C,m)) by A26, A30, MATRIX_1:36;
then (Gauge (C,m)) * ((i1 + 1),j1) = |[((W-bound C) + ((((E-bound C) - (W-bound C)) / (2 |^ m)) * ((i1 + 1) - 2))),((S-bound C) + ((((N-bound C) - (S-bound C)) / (2 |^ m)) * (j1 - 2)))]| by JORDAN8:def_1;
then ((Gauge (C,m)) * ((i1 + 1),j1)) `1 = (W-bound C) + ((((E-bound C) - (W-bound C)) / (2 |^ m)) * (((i1 + 1) - 2) / 1)) by EUCLID:52
.= (W-bound C) + ((((E-bound C) - (W-bound C)) / 1) * (((i1 + 1) - 2) / (2 |^ m))) by XCMPLX_1:85 ;
then ((Gauge (C,n)) * ((i + 1),j)) `1 <= ((Gauge (C,m)) * ((i1 + 1),j1)) `1 by A18, A22, XREAL_1:6;
then p `1 <= ((Gauge (C,m)) * ((i1 + 1),j1)) `1 by A13, XXREAL_0:2;
hence e in cell ((Gauge (C,m)),i1,j1) by A20, A26, A30, A28, A33, A34, A31, JORDAN9:17; ::_thesis: verum
end;
theorem Th38: :: JORDAN1H:38
for m, n, i, j being Element of NAT
for C being compact non horizontal non vertical Subset of (TOP-REAL 2) st m <= n & 1 <= i & i + 1 <= len (Gauge (C,n)) & 1 <= j & j + 1 <= width (Gauge (C,n)) holds
ex i1, j1 being Element of NAT st
( 1 <= i1 & i1 + 1 <= len (Gauge (C,m)) & 1 <= j1 & j1 + 1 <= width (Gauge (C,m)) & cell ((Gauge (C,n)),i,j) c= cell ((Gauge (C,m)),i1,j1) )
proof
let m, n, i, j be Element of NAT ; ::_thesis: for C being compact non horizontal non vertical Subset of (TOP-REAL 2) st m <= n & 1 <= i & i + 1 <= len (Gauge (C,n)) & 1 <= j & j + 1 <= width (Gauge (C,n)) holds
ex i1, j1 being Element of NAT st
( 1 <= i1 & i1 + 1 <= len (Gauge (C,m)) & 1 <= j1 & j1 + 1 <= width (Gauge (C,m)) & cell ((Gauge (C,n)),i,j) c= cell ((Gauge (C,m)),i1,j1) )
let C be compact non horizontal non vertical Subset of (TOP-REAL 2); ::_thesis: ( m <= n & 1 <= i & i + 1 <= len (Gauge (C,n)) & 1 <= j & j + 1 <= width (Gauge (C,n)) implies ex i1, j1 being Element of NAT st
( 1 <= i1 & i1 + 1 <= len (Gauge (C,m)) & 1 <= j1 & j1 + 1 <= width (Gauge (C,m)) & cell ((Gauge (C,n)),i,j) c= cell ((Gauge (C,m)),i1,j1) ) )
assume that
A1: m <= n and
A2: ( 1 <= i & i + 1 <= len (Gauge (C,n)) ) and
A3: ( 1 <= j & j + 1 <= width (Gauge (C,n)) ) ; ::_thesis: ex i1, j1 being Element of NAT st
( 1 <= i1 & i1 + 1 <= len (Gauge (C,m)) & 1 <= j1 & j1 + 1 <= width (Gauge (C,m)) & cell ((Gauge (C,n)),i,j) c= cell ((Gauge (C,m)),i1,j1) )
consider i1, j1 being Element of NAT such that
A4: i1 = [\(((i - 2) / (2 |^ (n -' m))) + 2)/] and
A5: j1 = [\(((j - 2) / (2 |^ (n -' m))) + 2)/] and
A6: cell ((Gauge (C,n)),i,j) c= cell ((Gauge (C,m)),i1,j1) by A1, A2, A3, Th37;
take i1 ; ::_thesis: ex j1 being Element of NAT st
( 1 <= i1 & i1 + 1 <= len (Gauge (C,m)) & 1 <= j1 & j1 + 1 <= width (Gauge (C,m)) & cell ((Gauge (C,n)),i,j) c= cell ((Gauge (C,m)),i1,j1) )
take j1 ; ::_thesis: ( 1 <= i1 & i1 + 1 <= len (Gauge (C,m)) & 1 <= j1 & j1 + 1 <= width (Gauge (C,m)) & cell ((Gauge (C,n)),i,j) c= cell ((Gauge (C,m)),i1,j1) )
thus ( 1 <= i1 & i1 + 1 <= len (Gauge (C,m)) ) by A1, A2, A4, Th36; ::_thesis: ( 1 <= j1 & j1 + 1 <= width (Gauge (C,m)) & cell ((Gauge (C,n)),i,j) c= cell ((Gauge (C,m)),i1,j1) )
( len (Gauge (C,m)) = width (Gauge (C,m)) & len (Gauge (C,n)) = width (Gauge (C,n)) ) by JORDAN8:def_1;
hence ( 1 <= j1 & j1 + 1 <= width (Gauge (C,m)) ) by A1, A3, A5, Th36; ::_thesis: cell ((Gauge (C,n)),i,j) c= cell ((Gauge (C,m)),i1,j1)
thus cell ((Gauge (C,n)),i,j) c= cell ((Gauge (C,m)),i1,j1) by A6; ::_thesis: verum
end;
theorem :: JORDAN1H:39
for P being Subset of (TOP-REAL 2) st P is bounded holds
not UBD P is bounded
proof
let P be Subset of (TOP-REAL 2); ::_thesis: ( P is bounded implies not UBD P is bounded )
assume P is bounded ; ::_thesis: not UBD P is bounded
then UBD P is_outside_component_of P by JORDAN2C:68;
hence not UBD P is bounded by JORDAN2C:def_3; ::_thesis: verum
end;
theorem Th40: :: JORDAN1H:40
for p being Point of (TOP-REAL 2)
for f being non constant standard special_circular_sequence st Rotate (f,p) is clockwise_oriented holds
f is clockwise_oriented
proof
let p be Point of (TOP-REAL 2); ::_thesis: for f being non constant standard special_circular_sequence st Rotate (f,p) is clockwise_oriented holds
f is clockwise_oriented
let f be non constant standard special_circular_sequence; ::_thesis: ( Rotate (f,p) is clockwise_oriented implies f is clockwise_oriented )
assume Rotate (f,p) is clockwise_oriented ; ::_thesis: f is clockwise_oriented
then reconsider g = Rotate (f,p) as non constant standard clockwise_oriented special_circular_sequence ;
for i being Element of NAT st 1 < i & i < len f holds
f /. i <> f /. 1 by GOBOARD7:36;
then f = Rotate (g,(f /. 1)) by REVROT_1:16;
hence f is clockwise_oriented ; ::_thesis: verum
end;
theorem :: JORDAN1H:41
for f being non constant standard special_circular_sequence st LeftComp f = UBD (L~ f) holds
f is clockwise_oriented
proof
let f be non constant standard special_circular_sequence; ::_thesis: ( LeftComp f = UBD (L~ f) implies f is clockwise_oriented )
assume A1: LeftComp f = UBD (L~ f) ; ::_thesis: f is clockwise_oriented
set g = Rotate (f,(N-min (L~ f)));
assume not f is clockwise_oriented ; ::_thesis: contradiction
then not Rotate (f,(N-min (L~ f))) is clockwise_oriented by Th40;
then A2: Rev (Rotate (f,(N-min (L~ f)))) is clockwise_oriented by REVROT_1:38;
L~ f = L~ (Rotate (f,(N-min (L~ f)))) by REVROT_1:33;
then UBD (L~ f) = UBD (L~ (Rev (Rotate (f,(N-min (L~ f)))))) by SPPOL_2:22
.= LeftComp (Rev (Rotate (f,(N-min (L~ f))))) by A2, GOBRD14:36
.= RightComp (Rotate (f,(N-min (L~ f)))) by GOBOARD9:23
.= RightComp f by REVROT_1:37 ;
hence contradiction by A1, SPRECT_4:6; ::_thesis: verum
end;
begin
theorem Th42: :: JORDAN1H:42
for f being non constant standard special_circular_sequence holds (Cl (LeftComp f)) ` = RightComp f
proof
let f be non constant standard special_circular_sequence; ::_thesis: (Cl (LeftComp f)) ` = RightComp f
A1: (Cl (LeftComp f)) ` misses Cl (LeftComp f) by SUBSET_1:24;
(Cl (LeftComp f)) \/ (RightComp f) = ((L~ f) \/ (LeftComp f)) \/ (RightComp f) by GOBRD14:22
.= ((L~ f) \/ (RightComp f)) \/ (LeftComp f) by XBOOLE_1:4
.= the carrier of (TOP-REAL 2) by GOBRD14:15 ;
hence (Cl (LeftComp f)) ` c= RightComp f by A1, XBOOLE_1:73; :: according to XBOOLE_0:def_10 ::_thesis: RightComp f c= (Cl (LeftComp f)) `
A2: RightComp f misses LeftComp f by GOBRD14:14;
( Cl (LeftComp f) = (LeftComp f) \/ (L~ f) & L~ f misses RightComp f ) by GOBRD14:22, SPRECT_3:25;
then Cl (LeftComp f) misses RightComp f by A2, XBOOLE_1:70;
hence RightComp f c= (Cl (LeftComp f)) ` by SUBSET_1:23; ::_thesis: verum
end;
theorem :: JORDAN1H:43
for f being non constant standard special_circular_sequence holds (Cl (RightComp f)) ` = LeftComp f
proof
let f be non constant standard special_circular_sequence; ::_thesis: (Cl (RightComp f)) ` = LeftComp f
A1: (Cl (RightComp f)) ` misses Cl (RightComp f) by SUBSET_1:24;
(Cl (RightComp f)) \/ (LeftComp f) = ((L~ f) \/ (RightComp f)) \/ (LeftComp f) by GOBRD14:21
.= the carrier of (TOP-REAL 2) by GOBRD14:15 ;
hence (Cl (RightComp f)) ` c= LeftComp f by A1, XBOOLE_1:73; :: according to XBOOLE_0:def_10 ::_thesis: LeftComp f c= (Cl (RightComp f)) `
A2: LeftComp f misses RightComp f by GOBRD14:14;
( Cl (RightComp f) = (RightComp f) \/ (L~ f) & L~ f misses LeftComp f ) by GOBRD14:21, SPRECT_3:26;
then Cl (RightComp f) misses LeftComp f by A2, XBOOLE_1:70;
hence LeftComp f c= (Cl (RightComp f)) ` by SUBSET_1:23; ::_thesis: verum
end;
theorem Th44: :: JORDAN1H:44
for n being Element of NAT
for C being compact non horizontal non vertical Subset of (TOP-REAL 2) st C is connected holds
GoB (Cage (C,n)) = Gauge (C,n)
proof
let n be Element of NAT ; ::_thesis: for C being compact non horizontal non vertical Subset of (TOP-REAL 2) st C is connected holds
GoB (Cage (C,n)) = Gauge (C,n)
let C be compact non horizontal non vertical Subset of (TOP-REAL 2); ::_thesis: ( C is connected implies GoB (Cage (C,n)) = Gauge (C,n) )
A1: ( S-max (L~ (Cage (C,n))) in rng (Cage (C,n)) & E-max (L~ (Cage (C,n))) in rng (Cage (C,n)) ) by SPRECT_2:42, SPRECT_2:46;
assume A2: C is connected ; ::_thesis: GoB (Cage (C,n)) = Gauge (C,n)
then consider iw being Element of NAT such that
A3: ( 1 <= iw & iw <= width (Gauge (C,n)) ) and
A4: W-min (L~ (Cage (C,n))) = (Gauge (C,n)) * (1,iw) by JORDAN1D:30;
A5: ( N-min (L~ (Cage (C,n))) in rng (Cage (C,n)) & Cage (C,n) is_sequence_on Gauge (C,n) ) by A2, JORDAN9:def_1, SPRECT_2:39;
consider ie being Element of NAT such that
A6: ( 1 <= ie & ie <= width (Gauge (C,n)) ) and
A7: (Gauge (C,n)) * ((len (Gauge (C,n))),ie) = E-max (L~ (Cage (C,n))) by A2, JORDAN1D:25;
A8: 1 <= len (Gauge (C,n)) by GOBRD11:34;
then A9: [(len (Gauge (C,n))),ie] in Indices (Gauge (C,n)) by A6, MATRIX_1:36;
consider iS being Element of NAT such that
A10: ( 1 <= iS & iS <= len (Gauge (C,n)) ) and
A11: (Gauge (C,n)) * (iS,1) = S-max (L~ (Cage (C,n))) by A2, JORDAN1D:28;
A12: 1 <= width (Gauge (C,n)) by GOBRD11:34;
then A13: [iS,1] in Indices (Gauge (C,n)) by A10, MATRIX_1:36;
consider IN being Element of NAT such that
A14: ( 1 <= IN & IN <= len (Gauge (C,n)) ) and
A15: (Gauge (C,n)) * (IN,(width (Gauge (C,n)))) = N-min (L~ (Cage (C,n))) by A2, JORDAN1D:21;
A16: [IN,(width (Gauge (C,n)))] in Indices (Gauge (C,n)) by A12, A14, MATRIX_1:36;
[1,iw] in Indices (Gauge (C,n)) by A8, A3, MATRIX_1:36;
hence GoB (Cage (C,n)) = Gauge (C,n) by A4, A11, A13, A7, A9, A1, A15, A16, A5, Th34, SPRECT_2:43; ::_thesis: verum
end;
theorem :: JORDAN1H:45
for n being Element of NAT
for C being compact non horizontal non vertical Subset of (TOP-REAL 2) st C is connected holds
N-min C in right_cell ((Cage (C,n)),1)
proof
let n be Element of NAT ; ::_thesis: for C being compact non horizontal non vertical Subset of (TOP-REAL 2) st C is connected holds
N-min C in right_cell ((Cage (C,n)),1)
let C be compact non horizontal non vertical Subset of (TOP-REAL 2); ::_thesis: ( C is connected implies N-min C in right_cell ((Cage (C,n)),1) )
assume A1: C is connected ; ::_thesis: N-min C in right_cell ((Cage (C,n)),1)
then consider i being Element of NAT such that
A2: 1 <= i and
A3: i + 1 <= len (Gauge (C,n)) and
A4: (Cage (C,n)) /. 1 = (Gauge (C,n)) * (i,(width (Gauge (C,n)))) and
A5: (Cage (C,n)) /. 2 = (Gauge (C,n)) * ((i + 1),(width (Gauge (C,n)))) and
A6: N-min C in cell ((Gauge (C,n)),i,((width (Gauge (C,n))) -' 1)) and
N-min C <> (Gauge (C,n)) * (i,((width (Gauge (C,n))) -' 1)) by JORDAN9:def_1;
A7: for i1, j1, i2, j2 being Element of NAT st [i1,j1] in Indices (GoB (Cage (C,n))) & [i2,j2] in Indices (GoB (Cage (C,n))) & (Cage (C,n)) /. 1 = (GoB (Cage (C,n))) * (i1,j1) & (Cage (C,n)) /. (1 + 1) = (GoB (Cage (C,n))) * (i2,j2) & not ( i1 = i2 & j1 + 1 = j2 & cell ((Gauge (C,n)),i,((width (Gauge (C,n))) -' 1)) = cell ((GoB (Cage (C,n))),i1,j1) ) & not ( i1 + 1 = i2 & j1 = j2 & cell ((Gauge (C,n)),i,((width (Gauge (C,n))) -' 1)) = cell ((GoB (Cage (C,n))),i1,(j1 -' 1)) ) & not ( i1 = i2 + 1 & j1 = j2 & cell ((Gauge (C,n)),i,((width (Gauge (C,n))) -' 1)) = cell ((GoB (Cage (C,n))),i2,j2) ) holds
( i1 = i2 & j1 = j2 + 1 & cell ((Gauge (C,n)),i,((width (Gauge (C,n))) -' 1)) = cell ((GoB (Cage (C,n))),(i1 -' 1),j2) )
proof
0 <> width (Gauge (C,n)) by GOBOARD1:def_3;
then A8: 1 <= width (Gauge (C,n)) by NAT_1:14;
A9: GoB (Cage (C,n)) = Gauge (C,n) by A1, Th44;
let i1, j1, i2, j2 be Element of NAT ; ::_thesis: ( [i1,j1] in Indices (GoB (Cage (C,n))) & [i2,j2] in Indices (GoB (Cage (C,n))) & (Cage (C,n)) /. 1 = (GoB (Cage (C,n))) * (i1,j1) & (Cage (C,n)) /. (1 + 1) = (GoB (Cage (C,n))) * (i2,j2) & not ( i1 = i2 & j1 + 1 = j2 & cell ((Gauge (C,n)),i,((width (Gauge (C,n))) -' 1)) = cell ((GoB (Cage (C,n))),i1,j1) ) & not ( i1 + 1 = i2 & j1 = j2 & cell ((Gauge (C,n)),i,((width (Gauge (C,n))) -' 1)) = cell ((GoB (Cage (C,n))),i1,(j1 -' 1)) ) & not ( i1 = i2 + 1 & j1 = j2 & cell ((Gauge (C,n)),i,((width (Gauge (C,n))) -' 1)) = cell ((GoB (Cage (C,n))),i2,j2) ) implies ( i1 = i2 & j1 = j2 + 1 & cell ((Gauge (C,n)),i,((width (Gauge (C,n))) -' 1)) = cell ((GoB (Cage (C,n))),(i1 -' 1),j2) ) )
assume that
A10: [i1,j1] in Indices (GoB (Cage (C,n))) and
A11: [i2,j2] in Indices (GoB (Cage (C,n))) and
A12: (Cage (C,n)) /. 1 = (GoB (Cage (C,n))) * (i1,j1) and
A13: (Cage (C,n)) /. (1 + 1) = (GoB (Cage (C,n))) * (i2,j2) ; ::_thesis: ( ( i1 = i2 & j1 + 1 = j2 & cell ((Gauge (C,n)),i,((width (Gauge (C,n))) -' 1)) = cell ((GoB (Cage (C,n))),i1,j1) ) or ( i1 + 1 = i2 & j1 = j2 & cell ((Gauge (C,n)),i,((width (Gauge (C,n))) -' 1)) = cell ((GoB (Cage (C,n))),i1,(j1 -' 1)) ) or ( i1 = i2 + 1 & j1 = j2 & cell ((Gauge (C,n)),i,((width (Gauge (C,n))) -' 1)) = cell ((GoB (Cage (C,n))),i2,j2) ) or ( i1 = i2 & j1 = j2 + 1 & cell ((Gauge (C,n)),i,((width (Gauge (C,n))) -' 1)) = cell ((GoB (Cage (C,n))),(i1 -' 1),j2) ) )
1 <= i + 1 by NAT_1:11;
then A14: [(i + 1),(width (Gauge (C,n)))] in Indices (Gauge (C,n)) by A3, A8, MATRIX_1:36;
then A15: i2 = i + 1 by A5, A11, A13, A9, GOBOARD1:5;
i < len (Gauge (C,n)) by A3, NAT_1:13;
then A16: [i,(width (Gauge (C,n)))] in Indices (Gauge (C,n)) by A2, A8, MATRIX_1:36;
then A17: i1 = i by A4, A10, A12, A9, GOBOARD1:5;
A18: j2 = width (Gauge (C,n)) by A5, A11, A13, A9, A14, GOBOARD1:5;
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 A4, A10, A12, A9, A16, A15, A18, GOBOARD1:5;
case ( i1 = i2 & j1 + 1 = j2 ) ; ::_thesis: cell ((Gauge (C,n)),i,((width (Gauge (C,n))) -' 1)) = cell ((GoB (Cage (C,n))),i1,j1)
hence cell ((Gauge (C,n)),i,((width (Gauge (C,n))) -' 1)) = cell ((GoB (Cage (C,n))),i1,j1) by A17, A15; ::_thesis: verum
end;
case ( i1 + 1 = i2 & j1 = j2 ) ; ::_thesis: cell ((Gauge (C,n)),i,((width (Gauge (C,n))) -' 1)) = cell ((GoB (Cage (C,n))),i1,(j1 -' 1))
thus cell ((Gauge (C,n)),i,((width (Gauge (C,n))) -' 1)) = cell ((GoB (Cage (C,n))),i1,(j1 -' 1)) by A4, A10, A12, A9, A16, A17, GOBOARD1:5; ::_thesis: verum
end;
case ( i1 = i2 + 1 & j1 = j2 ) ; ::_thesis: cell ((Gauge (C,n)),i,((width (Gauge (C,n))) -' 1)) = cell ((GoB (Cage (C,n))),i2,j2)
hence cell ((Gauge (C,n)),i,((width (Gauge (C,n))) -' 1)) = cell ((GoB (Cage (C,n))),i2,j2) by A17, A15; ::_thesis: verum
end;
case ( i1 = i2 & j1 = j2 + 1 ) ; ::_thesis: cell ((Gauge (C,n)),i,((width (Gauge (C,n))) -' 1)) = cell ((GoB (Cage (C,n))),(i1 -' 1),j2)
hence cell ((Gauge (C,n)),i,((width (Gauge (C,n))) -' 1)) = cell ((GoB (Cage (C,n))),(i1 -' 1),j2) by A17, A15; ::_thesis: verum
end;
end;
end;
1 + 1 <= len (Cage (C,n)) by GOBOARD7:34, XXREAL_0:2;
hence N-min C in right_cell ((Cage (C,n)),1) by A6, A7, GOBOARD5:def_6; ::_thesis: verum
end;
theorem Th46: :: JORDAN1H:46
for i, j being Element of NAT
for C being compact non horizontal non vertical Subset of (TOP-REAL 2) st C is connected & i <= j holds
L~ (Cage (C,j)) c= Cl (RightComp (Cage (C,i)))
proof
let i, j be Element of NAT ; ::_thesis: for C being compact non horizontal non vertical Subset of (TOP-REAL 2) st C is connected & i <= j holds
L~ (Cage (C,j)) c= Cl (RightComp (Cage (C,i)))
let C be compact non horizontal non vertical Subset of (TOP-REAL 2); ::_thesis: ( C is connected & i <= j implies L~ (Cage (C,j)) c= Cl (RightComp (Cage (C,i))) )
assume that
A1: C is connected and
A2: i <= j and
A3: not L~ (Cage (C,j)) c= Cl (RightComp (Cage (C,i))) ; ::_thesis: contradiction
A4: Cage (C,j) is_sequence_on Gauge (C,j) by A1, JORDAN9:def_1;
A5: GoB (Cage (C,i)) = Gauge (C,i) by A1, Th44;
consider p being Point of (TOP-REAL 2) such that
A6: p in L~ (Cage (C,j)) and
A7: not p in Cl (RightComp (Cage (C,i))) by A3, SUBSET_1:2;
consider i1 being Element of NAT such that
A8: 1 <= i1 and
A9: i1 + 1 <= len (Cage (C,j)) and
A10: p in LSeg ((Cage (C,j)),i1) by A6, SPPOL_2:13;
A11: GoB (Cage (C,j)) = Gauge (C,j) by A1, Th44;
then A12: right_cell ((Cage (C,j)),i1,(Gauge (C,j))) = right_cell ((Cage (C,j)),i1) by A8, A9, Th23;
A13: i1 < len (Cage (C,j)) by A9, NAT_1:13;
now__::_thesis:_right_cell_((Cage_(C,j)),i1)_c=_Cl_(LeftComp_(Cage_(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)) & right_cell ((Cage (C,j)),i1) c= cell ((Gauge (C,i)),i2,j2) )
proof
set f = Cage (C,j);
A14: i1 in dom (Cage (C,j)) by A8, A13, FINSEQ_3:25;
then consider i4, j4 being Element of NAT such that
A15: [i4,j4] in Indices (Gauge (C,j)) and
A16: (Cage (C,j)) /. i1 = (Gauge (C,j)) * (i4,j4) by A4, GOBOARD1:def_9;
A17: 1 <= i4 by A15, MATRIX_1:38;
A18: j4 <= width (Gauge (C,j)) by A15, MATRIX_1:38;
A19: 1 <= j4 by A15, MATRIX_1:38;
A20: i4 <= len (Gauge (C,j)) by A15, MATRIX_1:38;
1 <= i1 + 1 by NAT_1:11;
then A21: i1 + 1 in dom (Cage (C,j)) by A9, FINSEQ_3:25;
then consider i5, j5 being Element of NAT such that
A22: [i5,j5] in Indices (Gauge (C,j)) and
A23: (Cage (C,j)) /. (i1 + 1) = (Gauge (C,j)) * (i5,j5) by A4, GOBOARD1:def_9;
A24: 1 <= i5 by A22, MATRIX_1:38;
right_cell ((Cage (C,j)),i1) = right_cell ((Cage (C,j)),i1) ;
then A25: ( ( i4 = i5 & j4 + 1 = j5 & right_cell ((Cage (C,j)),i1) = cell ((GoB (Cage (C,j))),i4,j4) ) or ( i4 + 1 = i5 & j4 = j5 & right_cell ((Cage (C,j)),i1) = cell ((GoB (Cage (C,j))),i4,(j4 -' 1)) ) or ( i4 = i5 + 1 & j4 = j5 & right_cell ((Cage (C,j)),i1) = cell ((GoB (Cage (C,j))),i5,j5) ) or ( i4 = i5 & j4 = j5 + 1 & right_cell ((Cage (C,j)),i1) = cell ((GoB (Cage (C,j))),(i4 -' 1),j5) ) ) by A8, A9, A11, A15, A16, A22, A23, GOBOARD5:def_6;
(abs (i4 - i5)) + (abs (j4 - j5)) = 1 by A4, A14, A15, A16, A21, A22, A23, GOBOARD1:def_9;
then A26: ( ( abs (i4 - i5) = 1 & j4 = j5 ) or ( abs (j4 - j5) = 1 & i4 = i5 ) ) by SEQM_3:42;
A27: j5 <= width (Gauge (C,j)) by A22, MATRIX_1:38;
A28: i5 <= len (Gauge (C,j)) by A22, MATRIX_1:38;
A29: 1 <= j5 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 A26, 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)) & right_cell ((Cage (C,j)),i1) c= cell ((Gauge (C,i)),i2,j2) )
then i4 < len (Gauge (C,j)) by A1, A8, A9, A15, A16, A22, A23, JORDAN10:1;
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)) & right_cell ((Cage (C,j)),i1) c= cell ((Gauge (C,i)),i2,j2) ) by A2, A11, A17, A19, A27, A25, A30, Th38; ::_thesis: verum
end;
supposeA31: ( 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)) & right_cell ((Cage (C,j)),i1) c= cell ((Gauge (C,i)),i2,j2) )
then 1 < j4 by A1, A8, A9, A15, A16, A22, A23, JORDAN10:3;
then 1 + 1 <= j4 by NAT_1:13;
then A32: 1 <= j4 -' 1 by JORDAN5B:2;
(j4 -' 1) + 1 = j4 by A19, 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)) & right_cell ((Cage (C,j)),i1) c= cell ((Gauge (C,i)),i2,j2) ) by A2, A11, A17, A18, A28, A25, A31, A32, Th38; ::_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)) & right_cell ((Cage (C,j)),i1) c= cell ((Gauge (C,i)),i2,j2) )
then j5 < width (Gauge (C,j)) by A1, A8, A9, A15, A16, A22, A23, JORDAN10:4;
then j5 + 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)) & right_cell ((Cage (C,j)),i1) c= cell ((Gauge (C,i)),i2,j2) ) by A2, A11, A20, A24, A29, A25, A33, Th38; ::_thesis: verum
end;
supposeA34: ( 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)) & right_cell ((Cage (C,j)),i1) c= cell ((Gauge (C,i)),i2,j2) )
then 1 < i4 by A1, A8, A9, A15, A16, A22, A23, JORDAN10:2;
then 1 + 1 <= i4 by NAT_1:13;
then A35: 1 <= i4 -' 1 by JORDAN5B:2;
(i4 -' 1) + 1 = i4 by A17, 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)) & right_cell ((Cage (C,j)),i1) c= cell ((Gauge (C,i)),i2,j2) ) by A2, A11, A20, A18, A29, A25, A34, A35, Th38; ::_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: right_cell ((Cage (C,j)),i1) c= cell ((Gauge (C,i)),i2,j2) ;
A39: Int (right_cell ((Cage (C,j)),i1)) c= Int (cell ((Gauge (C,i)),i2,j2)) by A38, TOPS_1:19;
A40: RightComp (Cage (C,i)) is_a_component_of (L~ (Cage (C,i))) ` by GOBOARD9:def_2;
A41: (Cl (LeftComp (Cage (C,i)))) \/ (RightComp (Cage (C,i))) = ((L~ (Cage (C,i))) \/ (LeftComp (Cage (C,i)))) \/ (RightComp (Cage (C,i))) by GOBRD14:22
.= ((L~ (Cage (C,i))) \/ (RightComp (Cage (C,i)))) \/ (LeftComp (Cage (C,i))) by XBOOLE_1:4
.= the carrier of (TOP-REAL 2) by GOBRD14:15 ;
assume not right_cell ((Cage (C,j)),i1) c= Cl (LeftComp (Cage (C,i))) ; ::_thesis: contradiction
then not cell ((Gauge (C,i)),i2,j2) c= Cl (LeftComp (Cage (C,i))) by A38, XBOOLE_1:1;
then A42: cell ((Gauge (C,i)),i2,j2) meets RightComp (Cage (C,i)) by A41, XBOOLE_1:73;
A43: ( i2 < len (Gauge (C,i)) & j2 < width (Gauge (C,i)) ) by A36, A37, NAT_1:13;
then cell ((Gauge (C,i)),i2,j2) = Cl (Int (cell ((Gauge (C,i)),i2,j2))) by GOBRD11:35;
then A44: Int (cell ((Gauge (C,i)),i2,j2)) meets RightComp (Cage (C,i)) by A42, TSEP_1:36;
A45: Int (cell ((Gauge (C,i)),i2,j2)) is convex by A43, GOBOARD9:17;
Int (cell ((Gauge (C,i)),i2,j2)) c= (L~ (Cage (C,i))) ` by A5, A43, GOBRD12:1;
then Int (cell ((Gauge (C,i)),i2,j2)) c= RightComp (Cage (C,i)) by A44, A40, A45, GOBOARD9:4;
then Int (right_cell ((Cage (C,j)),i1)) c= RightComp (Cage (C,i)) by A39, XBOOLE_1:1;
then Cl (Int (right_cell ((Cage (C,j)),i1))) c= Cl (RightComp (Cage (C,i))) by PRE_TOPC:19;
then A46: right_cell ((Cage (C,j)),i1) c= Cl (RightComp (Cage (C,i))) by A4, A8, A9, A12, JORDAN9:11;
( LSeg ((Cage (C,j)),i1) c= right_cell ((Cage (C,j)),i1,(Gauge (C,j))) & right_cell ((Cage (C,j)),i1,(Gauge (C,j))) c= right_cell ((Cage (C,j)),i1) ) by A4, A8, A9, Th22, GOBRD13:33;
then LSeg ((Cage (C,j)),i1) c= right_cell ((Cage (C,j)),i1) by XBOOLE_1:1;
then LSeg ((Cage (C,j)),i1) c= Cl (RightComp (Cage (C,i))) by A46, XBOOLE_1:1;
hence contradiction by A7, A10; ::_thesis: verum
end;
then A47: C meets Cl (LeftComp (Cage (C,i))) by A1, A8, A9, A12, JORDAN9:31, XBOOLE_1:63;
( Cl (LeftComp (Cage (C,i))) = (LeftComp (Cage (C,i))) \/ (L~ (Cage (C,i))) & C misses L~ (Cage (C,i)) ) by A1, GOBRD14:22, JORDAN10:5;
then A48: C meets LeftComp (Cage (C,i)) by A47, XBOOLE_1:70;
reconsider D = (L~ (Cage (C,i))) ` as Subset of (TOP-REAL 2) ;
D = (LeftComp (Cage (C,i))) \/ (RightComp (Cage (C,i))) by GOBRD12:10;
then A49: RightComp (Cage (C,i)) c= D by XBOOLE_1:7;
C c= RightComp (Cage (C,i)) by A1, JORDAN10:11;
then A50: C c= D by A49, XBOOLE_1:1;
C meets C ;
then A51: C meets RightComp (Cage (C,i)) by A1, JORDAN10:11, XBOOLE_1:63;
( LeftComp (Cage (C,i)) is_a_component_of D & RightComp (Cage (C,i)) is_a_component_of D ) by GOBOARD9:def_1, GOBOARD9:def_2;
hence contradiction by A1, A48, A50, A51, JORDAN9:1, SPRECT_4:6; ::_thesis: verum
end;
theorem Th47: :: JORDAN1H:47
for i, j being Element of NAT
for C being compact non horizontal non vertical Subset of (TOP-REAL 2) st C is connected & i <= j holds
LeftComp (Cage (C,i)) c= LeftComp (Cage (C,j))
proof
let i, j be Element of NAT ; ::_thesis: for C being compact non horizontal non vertical Subset of (TOP-REAL 2) st C is connected & i <= j holds
LeftComp (Cage (C,i)) c= LeftComp (Cage (C,j))
let C be compact non horizontal non vertical Subset of (TOP-REAL 2); ::_thesis: ( C is connected & i <= j implies LeftComp (Cage (C,i)) c= LeftComp (Cage (C,j)) )
assume that
A1: C is connected and
A2: i <= j ; ::_thesis: LeftComp (Cage (C,i)) c= LeftComp (Cage (C,j))
A3: (Cage (C,j)) /. 1 = N-min (L~ (Cage (C,j))) by A1, JORDAN9:32;
( i < j or i = j ) by A2, XXREAL_0:1;
then A4: ( E-bound (L~ (Cage (C,i))) > E-bound (L~ (Cage (C,j))) or E-bound (L~ (Cage (C,i))) = E-bound (L~ (Cage (C,j))) ) by A1, JORDAN1A:67;
set p = |[((E-bound (L~ (Cage (C,i)))) + 1),0]|;
A5: LeftComp (Cage (C,i)) misses RightComp (Cage (C,i)) by GOBRD14:14;
A6: |[((E-bound (L~ (Cage (C,i)))) + 1),0]| `1 = (E-bound (L~ (Cage (C,i)))) + 1 by EUCLID:52;
then |[((E-bound (L~ (Cage (C,i)))) + 1),0]| `1 > E-bound (L~ (Cage (C,i))) by XREAL_1:29;
then |[((E-bound (L~ (Cage (C,i)))) + 1),0]| `1 > E-bound (L~ (Cage (C,j))) by A4, XXREAL_0:2;
then A7: |[((E-bound (L~ (Cage (C,i)))) + 1),0]| in LeftComp (Cage (C,j)) by A3, JORDAN2C:111;
(Cage (C,i)) /. 1 = N-min (L~ (Cage (C,i))) by A1, JORDAN9:32;
then |[((E-bound (L~ (Cage (C,i)))) + 1),0]| in LeftComp (Cage (C,i)) by A6, JORDAN2C:111, XREAL_1:29;
then A8: LeftComp (Cage (C,i)) meets LeftComp (Cage (C,j)) by A7, XBOOLE_0:3;
( Cl (RightComp (Cage (C,i))) = (RightComp (Cage (C,i))) \/ (L~ (Cage (C,i))) & L~ (Cage (C,i)) misses LeftComp (Cage (C,i)) ) by GOBRD14:21, SPRECT_3:26;
then Cl (RightComp (Cage (C,i))) misses LeftComp (Cage (C,i)) by A5, XBOOLE_1:70;
then L~ (Cage (C,j)) misses LeftComp (Cage (C,i)) by A1, A2, Th46, XBOOLE_1:63;
then ( LeftComp (Cage (C,j)) is_a_component_of (L~ (Cage (C,j))) ` & LeftComp (Cage (C,i)) c= (L~ (Cage (C,j))) ` ) by GOBOARD9:def_1, SUBSET_1:23;
hence LeftComp (Cage (C,i)) c= LeftComp (Cage (C,j)) by A8, GOBOARD9:4; ::_thesis: verum
end;
theorem :: JORDAN1H:48
for i, j being Element of NAT
for C being compact non horizontal non vertical Subset of (TOP-REAL 2) st C is connected & i <= j holds
RightComp (Cage (C,j)) c= RightComp (Cage (C,i))
proof
let i, j be Element of NAT ; ::_thesis: for C being compact non horizontal non vertical Subset of (TOP-REAL 2) st C is connected & i <= j holds
RightComp (Cage (C,j)) c= RightComp (Cage (C,i))
let C be compact non horizontal non vertical Subset of (TOP-REAL 2); ::_thesis: ( C is connected & i <= j implies RightComp (Cage (C,j)) c= RightComp (Cage (C,i)) )
assume ( C is connected & i <= j ) ; ::_thesis: RightComp (Cage (C,j)) c= RightComp (Cage (C,i))
then A1: Cl (LeftComp (Cage (C,i))) c= Cl (LeftComp (Cage (C,j))) by Th47, PRE_TOPC:19;
( (Cl (LeftComp (Cage (C,i)))) ` = RightComp (Cage (C,i)) & (Cl (LeftComp (Cage (C,j)))) ` = RightComp (Cage (C,j)) ) by Th42;
hence RightComp (Cage (C,j)) c= RightComp (Cage (C,i)) by A1, SUBSET_1:12; ::_thesis: verum
end;
begin
definition
let C be compact non horizontal non vertical Subset of (TOP-REAL 2);
let n be Element of NAT ;
func X-SpanStart (C,n) -> Element of NAT equals :: JORDAN1H:def 2
(2 |^ (n -' 1)) + 2;
correctness
coherence
(2 |^ (n -' 1)) + 2 is Element of NAT ;
;
end;
:: deftheorem defines X-SpanStart JORDAN1H:def_2_:_
for C being compact non horizontal non vertical Subset of (TOP-REAL 2)
for n being Element of NAT holds X-SpanStart (C,n) = (2 |^ (n -' 1)) + 2;
theorem Th49: :: JORDAN1H:49
for n being Element of NAT
for C being compact non horizontal non vertical Subset of (TOP-REAL 2) holds
( 2 < X-SpanStart (C,n) & X-SpanStart (C,n) < len (Gauge (C,n)) )
proof
let n be Element of NAT ; ::_thesis: for C being compact non horizontal non vertical Subset of (TOP-REAL 2) holds
( 2 < X-SpanStart (C,n) & X-SpanStart (C,n) < len (Gauge (C,n)) )
let C be compact non horizontal non vertical Subset of (TOP-REAL 2); ::_thesis: ( 2 < X-SpanStart (C,n) & X-SpanStart (C,n) < len (Gauge (C,n)) )
2 |^ (n -' 1) > 0 by NEWTON:83;
then (2 |^ (n -' 1)) + 2 > 0 + 2 by XREAL_1:6;
hence 2 < X-SpanStart (C,n) ; ::_thesis: X-SpanStart (C,n) < len (Gauge (C,n))
n -' 1 <= n by NAT_D:44;
then ( len (Gauge (C,n)) = (2 |^ n) + 3 & 2 |^ (n -' 1) <= 2 |^ n ) by JORDAN8:def_1, PREPOWER:93;
hence X-SpanStart (C,n) < len (Gauge (C,n)) by XREAL_1:8; ::_thesis: verum
end;
theorem Th50: :: JORDAN1H:50
for n being Element of NAT
for C being compact non horizontal non vertical Subset of (TOP-REAL 2) holds
( 1 <= (X-SpanStart (C,n)) -' 1 & (X-SpanStart (C,n)) -' 1 < len (Gauge (C,n)) )
proof
let n be Element of NAT ; ::_thesis: for C being compact non horizontal non vertical Subset of (TOP-REAL 2) holds
( 1 <= (X-SpanStart (C,n)) -' 1 & (X-SpanStart (C,n)) -' 1 < len (Gauge (C,n)) )
let C be compact non horizontal non vertical Subset of (TOP-REAL 2); ::_thesis: ( 1 <= (X-SpanStart (C,n)) -' 1 & (X-SpanStart (C,n)) -' 1 < len (Gauge (C,n)) )
2 < X-SpanStart (C,n) by Th49;
then A1: ((X-SpanStart (C,n)) -' 1) + 1 = X-SpanStart (C,n) by XREAL_1:235, XXREAL_0:2;
1 < X-SpanStart (C,n) by Th49, XXREAL_0:2;
hence 1 <= (X-SpanStart (C,n)) -' 1 by A1, NAT_1:13; ::_thesis: (X-SpanStart (C,n)) -' 1 < len (Gauge (C,n))
( X-SpanStart (C,n) < len (Gauge (C,n)) & (X-SpanStart (C,n)) -' 1 <= X-SpanStart (C,n) ) by Th49, NAT_D:44;
hence (X-SpanStart (C,n)) -' 1 < len (Gauge (C,n)) by XXREAL_0:2; ::_thesis: verum
end;
definition
let C be compact non horizontal non vertical Subset of (TOP-REAL 2);
let n be Element of NAT ;
predn is_sufficiently_large_for C means :Def3: :: JORDAN1H:def 3
ex j being Element of NAT st
( j < width (Gauge (C,n)) & cell ((Gauge (C,n)),((X-SpanStart (C,n)) -' 1),j) c= BDD C );
end;
:: deftheorem Def3 defines is_sufficiently_large_for JORDAN1H:def_3_:_
for C being compact non horizontal non vertical Subset of (TOP-REAL 2)
for n being Element of NAT holds
( n is_sufficiently_large_for C iff ex j being Element of NAT st
( j < width (Gauge (C,n)) & cell ((Gauge (C,n)),((X-SpanStart (C,n)) -' 1),j) c= BDD C ) );
theorem :: JORDAN1H:51
for n being Element of NAT
for C being compact non horizontal non vertical Subset of (TOP-REAL 2) st n is_sufficiently_large_for C holds
n >= 1
proof
let n be Element of NAT ; ::_thesis: for C being compact non horizontal non vertical Subset of (TOP-REAL 2) st n is_sufficiently_large_for C holds
n >= 1
let C be compact non horizontal non vertical Subset of (TOP-REAL 2); ::_thesis: ( n is_sufficiently_large_for C implies n >= 1 )
A1: 2 |^ 0 = 1 by NEWTON:4;
assume n is_sufficiently_large_for C ; ::_thesis: n >= 1
then consider j being Element of NAT such that
A2: j < width (Gauge (C,n)) and
A3: cell ((Gauge (C,n)),((X-SpanStart (C,n)) -' 1),j) c= BDD C by Def3;
assume n < 1 ; ::_thesis: contradiction
then A4: n = 0 by NAT_1:14;
A5: j > 1
proof
A6: (X-SpanStart (C,n)) -' 1 <= len (Gauge (C,n)) by Th50;
assume A7: j <= 1 ; ::_thesis: contradiction
percases ( j = 0 or j = 1 ) by A7, NAT_1:25;
supposeA8: j = 0 ; ::_thesis: contradiction
0 <= width (Gauge (C,n)) ;
then A9: not cell ((Gauge (C,n)),((X-SpanStart (C,n)) -' 1),0) is empty by A6, JORDAN1A:24;
cell ((Gauge (C,n)),((X-SpanStart (C,n)) -' 1),0) c= UBD C by A6, JORDAN1A:49;
hence contradiction by A3, A8, A9, JORDAN2C:24, XBOOLE_1:68; ::_thesis: verum
end;
supposeA10: j = 1 ; ::_thesis: contradiction
set i1 = X-SpanStart (C,n);
UBD C is_outside_component_of C by JORDAN2C:68;
then A11: UBD C is_a_component_of C ` by JORDAN2C:def_3;
( X-SpanStart (C,n) < len (Gauge (C,n)) & (X-SpanStart (C,n)) -' 1 <= X-SpanStart (C,n) ) by Th49, NAT_D:44;
then A12: (X-SpanStart (C,n)) -' 1 < len (Gauge (C,n)) by XXREAL_0:2;
BDD C c= C ` by JORDAN2C:25;
then A13: cell ((Gauge (C,n)),((X-SpanStart (C,n)) -' 1),1) c= C ` by A3, A10, XBOOLE_1:1;
A14: width (Gauge (C,n)) <> 0 by GOBOARD1:def_3;
then A15: 0 + 1 <= width (Gauge (C,n)) by NAT_1:14;
then A16: not cell ((Gauge (C,n)),((X-SpanStart (C,n)) -' 1),1) is empty by A6, JORDAN1A:24;
1 <= (X-SpanStart (C,n)) -' 1 by Th50;
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 A14, A12, GOBOARD5:26;
then A17: 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 A6, JORDAN1A:49;
then cell ((Gauge (C,n)),((X-SpanStart (C,n)) -' 1),1) c= UBD C by A15, A12, A17, A11, A13, GOBOARD9:4, JORDAN1A:25;
hence contradiction by A3, A10, A16, JORDAN2C:24, XBOOLE_1:68; ::_thesis: verum
end;
end;
end;
A18: width (Gauge (C,n)) = (2 |^ n) + 3 by JORDAN1A:28;
then A19: j <= 3 + 1 by A2, A4, NEWTON:4;
A20: j + 1 < width (Gauge (C,n))
proof
assume j + 1 >= width (Gauge (C,n)) ; ::_thesis: contradiction
then A21: ( j + 1 > width (Gauge (C,n)) or j + 1 = width (Gauge (C,n)) ) by XXREAL_0:1;
A22: (X-SpanStart (C,n)) -' 1 <= len (Gauge (C,n)) by Th50;
percases ( j = width (Gauge (C,n)) or j + 1 = width (Gauge (C,n)) ) by A2, A21, NAT_1:13;
supposeA23: j = width (Gauge (C,n)) ; ::_thesis: contradiction
( not cell ((Gauge (C,n)),((X-SpanStart (C,n)) -' 1),(width (Gauge (C,n)))) is empty & cell ((Gauge (C,n)),((X-SpanStart (C,n)) -' 1),(width (Gauge (C,n)))) c= UBD C ) by A22, JORDAN1A:24, JORDAN1A:50;
hence contradiction by A3, A23, JORDAN2C:24, XBOOLE_1:68; ::_thesis: verum
end;
suppose j + 1 = width (Gauge (C,n)) ; ::_thesis: contradiction
then A24: cell ((Gauge (C,n)),((X-SpanStart (C,n)) -' 1),((width (Gauge (C,n))) -' 1)) c= BDD C by A3, NAT_D:34;
BDD C c= C ` by JORDAN2C:25;
then A25: cell ((Gauge (C,n)),((X-SpanStart (C,n)) -' 1),((width (Gauge (C,n))) -' 1)) c= C ` by A24, XBOOLE_1:1;
set i1 = X-SpanStart (C,n);
A26: (width (Gauge (C,n))) - 1 < width (Gauge (C,n)) by XREAL_1:146;
UBD C is_outside_component_of C by JORDAN2C:68;
then A27: 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 A28: not cell ((Gauge (C,n)),((X-SpanStart (C,n)) -' 1),((width (Gauge (C,n))) -' 1)) is empty by A22, JORDAN1A:24;
A29: cell ((Gauge (C,n)),((X-SpanStart (C,n)) -' 1),(width (Gauge (C,n)))) c= UBD C by A22, JORDAN1A:50;
A30: 1 <= (X-SpanStart (C,n)) -' 1 by Th50;
( X-SpanStart (C,n) < len (Gauge (C,n)) & (X-SpanStart (C,n)) -' 1 <= X-SpanStart (C,n) ) by Th49, NAT_D:44;
then A31: (X-SpanStart (C,n)) -' 1 < len (Gauge (C,n)) by XXREAL_0:2;
A32: 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 A31, A26, A30, GOBOARD5:26;
then A33: 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 A32, A26, 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 A29, A31, A33, A27, A25, GOBOARD9:4, JORDAN1A:25;
hence contradiction by A24, A28, JORDAN2C:24, XBOOLE_1:68; ::_thesis: verum
end;
end;
end;
percases ( j = 0 or j = 1 or j = 2 or j = 3 or j = 4 ) by A19, NAT_1:28;
suppose ( j = 0 or j = 1 ) ; ::_thesis: contradiction
hence contradiction by A5; ::_thesis: verum
end;
supposeA34: j = 2 ; ::_thesis: contradiction
A35: X-SpanStart (C,0) = 1 + 2 by A1, NAT_2:8;
then (X-SpanStart (C,0)) -' 1 = (X-SpanStart (C,0)) - 1 by NAT_D:39
.= 2 by A35 ;
hence contradiction by A3, A4, A34, JORDAN1B:18; ::_thesis: verum
end;
suppose ( j = 3 or j = 4 ) ; ::_thesis: contradiction
hence contradiction by A18, A20, A1, A4; ::_thesis: verum
end;
end;
end;
theorem :: JORDAN1H:52
for C being non empty compact non horizontal non vertical Subset of (TOP-REAL 2)
for n being Element of NAT
for f being FinSequence of (TOP-REAL 2) st f is_sequence_on Gauge (C,n) & len f > 1 holds
for i1, j1 being Element of NAT st left_cell (f,((len f) -' 1),(Gauge (C,n))) meets C & [i1,j1] in Indices (Gauge (C,n)) & f /. ((len f) -' 1) = (Gauge (C,n)) * (i1,j1) & [i1,(j1 + 1)] in Indices (Gauge (C,n)) & f /. (len f) = (Gauge (C,n)) * (i1,(j1 + 1)) holds
[(i1 -' 1),(j1 + 1)] in Indices (Gauge (C,n))
proof
let C be non empty compact non horizontal non vertical Subset of (TOP-REAL 2); ::_thesis: for n being Element of NAT
for f being FinSequence of (TOP-REAL 2) st f is_sequence_on Gauge (C,n) & len f > 1 holds
for i1, j1 being Element of NAT st left_cell (f,((len f) -' 1),(Gauge (C,n))) meets C & [i1,j1] in Indices (Gauge (C,n)) & f /. ((len f) -' 1) = (Gauge (C,n)) * (i1,j1) & [i1,(j1 + 1)] in Indices (Gauge (C,n)) & f /. (len f) = (Gauge (C,n)) * (i1,(j1 + 1)) holds
[(i1 -' 1),(j1 + 1)] in Indices (Gauge (C,n))
let n be Element of NAT ; ::_thesis: for f being FinSequence of (TOP-REAL 2) st f is_sequence_on Gauge (C,n) & len f > 1 holds
for i1, j1 being Element of NAT st left_cell (f,((len f) -' 1),(Gauge (C,n))) meets C & [i1,j1] in Indices (Gauge (C,n)) & f /. ((len f) -' 1) = (Gauge (C,n)) * (i1,j1) & [i1,(j1 + 1)] in Indices (Gauge (C,n)) & f /. (len f) = (Gauge (C,n)) * (i1,(j1 + 1)) holds
[(i1 -' 1),(j1 + 1)] in Indices (Gauge (C,n))
set G = Gauge (C,n);
let f be FinSequence of (TOP-REAL 2); ::_thesis: ( f is_sequence_on Gauge (C,n) & len f > 1 implies for i1, j1 being Element of NAT st left_cell (f,((len f) -' 1),(Gauge (C,n))) meets C & [i1,j1] in Indices (Gauge (C,n)) & f /. ((len f) -' 1) = (Gauge (C,n)) * (i1,j1) & [i1,(j1 + 1)] in Indices (Gauge (C,n)) & f /. (len f) = (Gauge (C,n)) * (i1,(j1 + 1)) holds
[(i1 -' 1),(j1 + 1)] in Indices (Gauge (C,n)) )
assume that
A1: f is_sequence_on Gauge (C,n) and
A2: len f > 1 ; ::_thesis: for i1, j1 being Element of NAT st left_cell (f,((len f) -' 1),(Gauge (C,n))) meets C & [i1,j1] in Indices (Gauge (C,n)) & f /. ((len f) -' 1) = (Gauge (C,n)) * (i1,j1) & [i1,(j1 + 1)] in Indices (Gauge (C,n)) & f /. (len f) = (Gauge (C,n)) * (i1,(j1 + 1)) holds
[(i1 -' 1),(j1 + 1)] in Indices (Gauge (C,n))
A3: ( 1 <= (len f) -' 1 & ((len f) -' 1) + 1 = len f ) by A2, NAT_D:49, XREAL_1:235;
let i1, j1 be Element of NAT ; ::_thesis: ( left_cell (f,((len f) -' 1),(Gauge (C,n))) meets C & [i1,j1] in Indices (Gauge (C,n)) & f /. ((len f) -' 1) = (Gauge (C,n)) * (i1,j1) & [i1,(j1 + 1)] in Indices (Gauge (C,n)) & f /. (len f) = (Gauge (C,n)) * (i1,(j1 + 1)) implies [(i1 -' 1),(j1 + 1)] in Indices (Gauge (C,n)) )
assume that
A4: left_cell (f,((len f) -' 1),(Gauge (C,n))) meets C and
A5: [i1,j1] in Indices (Gauge (C,n)) and
A6: f /. ((len f) -' 1) = (Gauge (C,n)) * (i1,j1) and
A7: [i1,(j1 + 1)] in Indices (Gauge (C,n)) and
A8: f /. (len f) = (Gauge (C,n)) * (i1,(j1 + 1)) ; ::_thesis: [(i1 -' 1),(j1 + 1)] in Indices (Gauge (C,n))
A9: 1 <= i1 by A7, MATRIX_1:38;
A10: ( len (Gauge (C,n)) = width (Gauge (C,n)) & j1 <= width (Gauge (C,n)) ) by A5, JORDAN8:def_1, MATRIX_1:38;
A11: now__::_thesis:_not_i1_-'_1_<_1
assume i1 -' 1 < 1 ; ::_thesis: contradiction
then i1 <= 1 by NAT_1:14, NAT_D:36;
then i1 = 1 by A9, XXREAL_0:1;
then cell ((Gauge (C,n)),(1 -' 1),j1) meets C by A1, A4, A5, A6, A7, A8, A3, GOBRD13:21;
then cell ((Gauge (C,n)),0,j1) meets C by XREAL_1:232;
hence contradiction by A10, JORDAN8:18; ::_thesis: verum
end;
A12: i1 -' 1 <= i1 by NAT_D:35;
i1 <= len (Gauge (C,n)) by A5, MATRIX_1:38;
then A13: i1 -' 1 <= len (Gauge (C,n)) by A12, XXREAL_0:2;
( 1 <= j1 + 1 & j1 + 1 <= width (Gauge (C,n)) ) by A7, MATRIX_1:38;
hence [(i1 -' 1),(j1 + 1)] in Indices (Gauge (C,n)) by A13, A11, MATRIX_1:36; ::_thesis: verum
end;
theorem :: JORDAN1H:53
for C being non empty compact non horizontal non vertical Subset of (TOP-REAL 2)
for n being Element of NAT
for f being FinSequence of (TOP-REAL 2) st f is_sequence_on Gauge (C,n) & len f > 1 holds
for i1, j1 being Element of NAT st left_cell (f,((len f) -' 1),(Gauge (C,n))) meets C & [i1,j1] in Indices (Gauge (C,n)) & f /. ((len f) -' 1) = (Gauge (C,n)) * (i1,j1) & [(i1 + 1),j1] in Indices (Gauge (C,n)) & f /. (len f) = (Gauge (C,n)) * ((i1 + 1),j1) holds
[(i1 + 1),(j1 + 1)] in Indices (Gauge (C,n))
proof
let C be non empty compact non horizontal non vertical Subset of (TOP-REAL 2); ::_thesis: for n being Element of NAT
for f being FinSequence of (TOP-REAL 2) st f is_sequence_on Gauge (C,n) & len f > 1 holds
for i1, j1 being Element of NAT st left_cell (f,((len f) -' 1),(Gauge (C,n))) meets C & [i1,j1] in Indices (Gauge (C,n)) & f /. ((len f) -' 1) = (Gauge (C,n)) * (i1,j1) & [(i1 + 1),j1] in Indices (Gauge (C,n)) & f /. (len f) = (Gauge (C,n)) * ((i1 + 1),j1) holds
[(i1 + 1),(j1 + 1)] in Indices (Gauge (C,n))
let n be Element of NAT ; ::_thesis: for f being FinSequence of (TOP-REAL 2) st f is_sequence_on Gauge (C,n) & len f > 1 holds
for i1, j1 being Element of NAT st left_cell (f,((len f) -' 1),(Gauge (C,n))) meets C & [i1,j1] in Indices (Gauge (C,n)) & f /. ((len f) -' 1) = (Gauge (C,n)) * (i1,j1) & [(i1 + 1),j1] in Indices (Gauge (C,n)) & f /. (len f) = (Gauge (C,n)) * ((i1 + 1),j1) holds
[(i1 + 1),(j1 + 1)] in Indices (Gauge (C,n))
set G = Gauge (C,n);
let f be FinSequence of (TOP-REAL 2); ::_thesis: ( f is_sequence_on Gauge (C,n) & len f > 1 implies for i1, j1 being Element of NAT st left_cell (f,((len f) -' 1),(Gauge (C,n))) meets C & [i1,j1] in Indices (Gauge (C,n)) & f /. ((len f) -' 1) = (Gauge (C,n)) * (i1,j1) & [(i1 + 1),j1] in Indices (Gauge (C,n)) & f /. (len f) = (Gauge (C,n)) * ((i1 + 1),j1) holds
[(i1 + 1),(j1 + 1)] in Indices (Gauge (C,n)) )
assume that
A1: f is_sequence_on Gauge (C,n) and
A2: len f > 1 ; ::_thesis: for i1, j1 being Element of NAT st left_cell (f,((len f) -' 1),(Gauge (C,n))) meets C & [i1,j1] in Indices (Gauge (C,n)) & f /. ((len f) -' 1) = (Gauge (C,n)) * (i1,j1) & [(i1 + 1),j1] in Indices (Gauge (C,n)) & f /. (len f) = (Gauge (C,n)) * ((i1 + 1),j1) holds
[(i1 + 1),(j1 + 1)] in Indices (Gauge (C,n))
A3: ( 1 <= (len f) -' 1 & ((len f) -' 1) + 1 = len f ) by A2, NAT_D:49, XREAL_1:235;
A4: len (Gauge (C,n)) = width (Gauge (C,n)) by JORDAN8:def_1;
let i1, j1 be Element of NAT ; ::_thesis: ( left_cell (f,((len f) -' 1),(Gauge (C,n))) meets C & [i1,j1] in Indices (Gauge (C,n)) & f /. ((len f) -' 1) = (Gauge (C,n)) * (i1,j1) & [(i1 + 1),j1] in Indices (Gauge (C,n)) & f /. (len f) = (Gauge (C,n)) * ((i1 + 1),j1) implies [(i1 + 1),(j1 + 1)] in Indices (Gauge (C,n)) )
assume that
A5: left_cell (f,((len f) -' 1),(Gauge (C,n))) meets C and
A6: [i1,j1] in Indices (Gauge (C,n)) and
A7: f /. ((len f) -' 1) = (Gauge (C,n)) * (i1,j1) and
A8: [(i1 + 1),j1] in Indices (Gauge (C,n)) and
A9: f /. (len f) = (Gauge (C,n)) * ((i1 + 1),j1) ; ::_thesis: [(i1 + 1),(j1 + 1)] in Indices (Gauge (C,n))
A10: j1 <= width (Gauge (C,n)) by A8, MATRIX_1:38;
A11: i1 <= len (Gauge (C,n)) by A6, MATRIX_1:38;
A12: now__::_thesis:_not_j1_+_1_>_len_(Gauge_(C,n))
assume j1 + 1 > len (Gauge (C,n)) ; ::_thesis: contradiction
then A13: (len (Gauge (C,n))) + 1 <= j1 + 1 by NAT_1:13;
j1 + 1 <= (len (Gauge (C,n))) + 1 by A4, A10, XREAL_1:6;
then j1 + 1 = (len (Gauge (C,n))) + 1 by A13, XXREAL_0:1;
then cell ((Gauge (C,n)),i1,(len (Gauge (C,n)))) meets C by A1, A5, A6, A7, A8, A9, A3, GOBRD13:23;
hence contradiction by A11, JORDAN8:15; ::_thesis: verum
end;
A14: 1 <= j1 + 1 by NAT_1:11;
( 1 <= i1 + 1 & i1 + 1 <= len (Gauge (C,n)) ) by A8, MATRIX_1:38;
hence [(i1 + 1),(j1 + 1)] in Indices (Gauge (C,n)) by A4, A14, A12, MATRIX_1:36; ::_thesis: verum
end;
theorem :: JORDAN1H:54
for C being non empty compact non horizontal non vertical Subset of (TOP-REAL 2)
for n being Element of NAT
for f being FinSequence of (TOP-REAL 2) st f is_sequence_on Gauge (C,n) & len f > 1 holds
for j1, i2 being Element of NAT st left_cell (f,((len f) -' 1),(Gauge (C,n))) meets C & [(i2 + 1),j1] in Indices (Gauge (C,n)) & f /. ((len f) -' 1) = (Gauge (C,n)) * ((i2 + 1),j1) & [i2,j1] in Indices (Gauge (C,n)) & f /. (len f) = (Gauge (C,n)) * (i2,j1) holds
[i2,(j1 -' 1)] in Indices (Gauge (C,n))
proof
let C be non empty compact non horizontal non vertical Subset of (TOP-REAL 2); ::_thesis: for n being Element of NAT
for f being FinSequence of (TOP-REAL 2) st f is_sequence_on Gauge (C,n) & len f > 1 holds
for j1, i2 being Element of NAT st left_cell (f,((len f) -' 1),(Gauge (C,n))) meets C & [(i2 + 1),j1] in Indices (Gauge (C,n)) & f /. ((len f) -' 1) = (Gauge (C,n)) * ((i2 + 1),j1) & [i2,j1] in Indices (Gauge (C,n)) & f /. (len f) = (Gauge (C,n)) * (i2,j1) holds
[i2,(j1 -' 1)] in Indices (Gauge (C,n))
let n be Element of NAT ; ::_thesis: for f being FinSequence of (TOP-REAL 2) st f is_sequence_on Gauge (C,n) & len f > 1 holds
for j1, i2 being Element of NAT st left_cell (f,((len f) -' 1),(Gauge (C,n))) meets C & [(i2 + 1),j1] in Indices (Gauge (C,n)) & f /. ((len f) -' 1) = (Gauge (C,n)) * ((i2 + 1),j1) & [i2,j1] in Indices (Gauge (C,n)) & f /. (len f) = (Gauge (C,n)) * (i2,j1) holds
[i2,(j1 -' 1)] in Indices (Gauge (C,n))
set G = Gauge (C,n);
let f be FinSequence of (TOP-REAL 2); ::_thesis: ( f is_sequence_on Gauge (C,n) & len f > 1 implies for j1, i2 being Element of NAT st left_cell (f,((len f) -' 1),(Gauge (C,n))) meets C & [(i2 + 1),j1] in Indices (Gauge (C,n)) & f /. ((len f) -' 1) = (Gauge (C,n)) * ((i2 + 1),j1) & [i2,j1] in Indices (Gauge (C,n)) & f /. (len f) = (Gauge (C,n)) * (i2,j1) holds
[i2,(j1 -' 1)] in Indices (Gauge (C,n)) )
assume that
A1: f is_sequence_on Gauge (C,n) and
A2: len f > 1 ; ::_thesis: for j1, i2 being Element of NAT st left_cell (f,((len f) -' 1),(Gauge (C,n))) meets C & [(i2 + 1),j1] in Indices (Gauge (C,n)) & f /. ((len f) -' 1) = (Gauge (C,n)) * ((i2 + 1),j1) & [i2,j1] in Indices (Gauge (C,n)) & f /. (len f) = (Gauge (C,n)) * (i2,j1) holds
[i2,(j1 -' 1)] in Indices (Gauge (C,n))
A3: ( 1 <= (len f) -' 1 & ((len f) -' 1) + 1 = len f ) by A2, NAT_D:49, XREAL_1:235;
let j1, i2 be Element of NAT ; ::_thesis: ( left_cell (f,((len f) -' 1),(Gauge (C,n))) meets C & [(i2 + 1),j1] in Indices (Gauge (C,n)) & f /. ((len f) -' 1) = (Gauge (C,n)) * ((i2 + 1),j1) & [i2,j1] in Indices (Gauge (C,n)) & f /. (len f) = (Gauge (C,n)) * (i2,j1) implies [i2,(j1 -' 1)] in Indices (Gauge (C,n)) )
assume that
A4: ( left_cell (f,((len f) -' 1),(Gauge (C,n))) meets C & [(i2 + 1),j1] in Indices (Gauge (C,n)) & f /. ((len f) -' 1) = (Gauge (C,n)) * ((i2 + 1),j1) ) and
A5: [i2,j1] in Indices (Gauge (C,n)) and
A6: f /. (len f) = (Gauge (C,n)) * (i2,j1) ; ::_thesis: [i2,(j1 -' 1)] in Indices (Gauge (C,n))
A7: i2 <= len (Gauge (C,n)) by A5, MATRIX_1:38;
A8: 1 <= j1 by A5, MATRIX_1:38;
A9: now__::_thesis:_not_j1_-'_1_<_1
assume j1 -' 1 < 1 ; ::_thesis: contradiction
then j1 <= 1 by NAT_1:14, NAT_D:36;
then j1 = 1 by A8, XXREAL_0:1;
then cell ((Gauge (C,n)),i2,(1 -' 1)) meets C by A1, A4, A5, A6, A3, GOBRD13:25;
then cell ((Gauge (C,n)),i2,0) meets C by XREAL_1:232;
hence contradiction by A7, JORDAN8:17; ::_thesis: verum
end;
A10: j1 -' 1 <= j1 by NAT_D:35;
j1 <= width (Gauge (C,n)) by A5, MATRIX_1:38;
then A11: j1 -' 1 <= width (Gauge (C,n)) by A10, XXREAL_0:2;
1 <= i2 by A5, MATRIX_1:38;
hence [i2,(j1 -' 1)] in Indices (Gauge (C,n)) by A7, A11, A9, MATRIX_1:36; ::_thesis: verum
end;
theorem :: JORDAN1H:55
for C being non empty compact non horizontal non vertical Subset of (TOP-REAL 2)
for n being Element of NAT
for f being FinSequence of (TOP-REAL 2) st f is_sequence_on Gauge (C,n) & len f > 1 holds
for i1, j2 being Element of NAT st left_cell (f,((len f) -' 1),(Gauge (C,n))) meets C & [i1,(j2 + 1)] in Indices (Gauge (C,n)) & f /. ((len f) -' 1) = (Gauge (C,n)) * (i1,(j2 + 1)) & [i1,j2] in Indices (Gauge (C,n)) & f /. (len f) = (Gauge (C,n)) * (i1,j2) holds
[(i1 + 1),j2] in Indices (Gauge (C,n))
proof
let C be non empty compact non horizontal non vertical Subset of (TOP-REAL 2); ::_thesis: for n being Element of NAT
for f being FinSequence of (TOP-REAL 2) st f is_sequence_on Gauge (C,n) & len f > 1 holds
for i1, j2 being Element of NAT st left_cell (f,((len f) -' 1),(Gauge (C,n))) meets C & [i1,(j2 + 1)] in Indices (Gauge (C,n)) & f /. ((len f) -' 1) = (Gauge (C,n)) * (i1,(j2 + 1)) & [i1,j2] in Indices (Gauge (C,n)) & f /. (len f) = (Gauge (C,n)) * (i1,j2) holds
[(i1 + 1),j2] in Indices (Gauge (C,n))
let n be Element of NAT ; ::_thesis: for f being FinSequence of (TOP-REAL 2) st f is_sequence_on Gauge (C,n) & len f > 1 holds
for i1, j2 being Element of NAT st left_cell (f,((len f) -' 1),(Gauge (C,n))) meets C & [i1,(j2 + 1)] in Indices (Gauge (C,n)) & f /. ((len f) -' 1) = (Gauge (C,n)) * (i1,(j2 + 1)) & [i1,j2] in Indices (Gauge (C,n)) & f /. (len f) = (Gauge (C,n)) * (i1,j2) holds
[(i1 + 1),j2] in Indices (Gauge (C,n))
set G = Gauge (C,n);
A1: len (Gauge (C,n)) = width (Gauge (C,n)) by JORDAN8:def_1;
let f be FinSequence of (TOP-REAL 2); ::_thesis: ( f is_sequence_on Gauge (C,n) & len f > 1 implies for i1, j2 being Element of NAT st left_cell (f,((len f) -' 1),(Gauge (C,n))) meets C & [i1,(j2 + 1)] in Indices (Gauge (C,n)) & f /. ((len f) -' 1) = (Gauge (C,n)) * (i1,(j2 + 1)) & [i1,j2] in Indices (Gauge (C,n)) & f /. (len f) = (Gauge (C,n)) * (i1,j2) holds
[(i1 + 1),j2] in Indices (Gauge (C,n)) )
assume that
A2: f is_sequence_on Gauge (C,n) and
A3: len f > 1 ; ::_thesis: for i1, j2 being Element of NAT st left_cell (f,((len f) -' 1),(Gauge (C,n))) meets C & [i1,(j2 + 1)] in Indices (Gauge (C,n)) & f /. ((len f) -' 1) = (Gauge (C,n)) * (i1,(j2 + 1)) & [i1,j2] in Indices (Gauge (C,n)) & f /. (len f) = (Gauge (C,n)) * (i1,j2) holds
[(i1 + 1),j2] in Indices (Gauge (C,n))
A4: ( 1 <= (len f) -' 1 & ((len f) -' 1) + 1 = len f ) by A3, NAT_D:49, XREAL_1:235;
let i1, j2 be Element of NAT ; ::_thesis: ( left_cell (f,((len f) -' 1),(Gauge (C,n))) meets C & [i1,(j2 + 1)] in Indices (Gauge (C,n)) & f /. ((len f) -' 1) = (Gauge (C,n)) * (i1,(j2 + 1)) & [i1,j2] in Indices (Gauge (C,n)) & f /. (len f) = (Gauge (C,n)) * (i1,j2) implies [(i1 + 1),j2] in Indices (Gauge (C,n)) )
assume that
A5: ( left_cell (f,((len f) -' 1),(Gauge (C,n))) meets C & [i1,(j2 + 1)] in Indices (Gauge (C,n)) & f /. ((len f) -' 1) = (Gauge (C,n)) * (i1,(j2 + 1)) ) and
A6: [i1,j2] in Indices (Gauge (C,n)) and
A7: f /. (len f) = (Gauge (C,n)) * (i1,j2) ; ::_thesis: [(i1 + 1),j2] in Indices (Gauge (C,n))
A8: j2 <= width (Gauge (C,n)) by A6, MATRIX_1:38;
A9: i1 <= len (Gauge (C,n)) by A6, MATRIX_1:38;
A10: now__::_thesis:_not_i1_+_1_>_len_(Gauge_(C,n))
assume i1 + 1 > len (Gauge (C,n)) ; ::_thesis: contradiction
then A11: (len (Gauge (C,n))) + 1 <= i1 + 1 by NAT_1:13;
i1 + 1 <= (len (Gauge (C,n))) + 1 by A9, XREAL_1:6;
then i1 + 1 = (len (Gauge (C,n))) + 1 by A11, XXREAL_0:1;
then cell ((Gauge (C,n)),(len (Gauge (C,n))),j2) meets C by A2, A5, A6, A7, A4, GOBRD13:27;
hence contradiction by A1, A8, JORDAN8:16; ::_thesis: verum
end;
A12: 1 <= i1 + 1 by NAT_1:11;
1 <= j2 by A6, MATRIX_1:38;
hence [(i1 + 1),j2] in Indices (Gauge (C,n)) by A8, A12, A10, MATRIX_1:36; ::_thesis: verum
end;
theorem :: JORDAN1H:56
for C being non empty compact non horizontal non vertical Subset of (TOP-REAL 2)
for n being Element of NAT
for f being FinSequence of (TOP-REAL 2) st f is_sequence_on Gauge (C,n) & len f > 1 holds
for i1, j1 being Element of NAT st front_left_cell (f,((len f) -' 1),(Gauge (C,n))) meets C & [i1,j1] in Indices (Gauge (C,n)) & f /. ((len f) -' 1) = (Gauge (C,n)) * (i1,j1) & [i1,(j1 + 1)] in Indices (Gauge (C,n)) & f /. (len f) = (Gauge (C,n)) * (i1,(j1 + 1)) holds
[i1,(j1 + 2)] in Indices (Gauge (C,n))
proof
let C be non empty compact non horizontal non vertical Subset of (TOP-REAL 2); ::_thesis: for n being Element of NAT
for f being FinSequence of (TOP-REAL 2) st f is_sequence_on Gauge (C,n) & len f > 1 holds
for i1, j1 being Element of NAT st front_left_cell (f,((len f) -' 1),(Gauge (C,n))) meets C & [i1,j1] in Indices (Gauge (C,n)) & f /. ((len f) -' 1) = (Gauge (C,n)) * (i1,j1) & [i1,(j1 + 1)] in Indices (Gauge (C,n)) & f /. (len f) = (Gauge (C,n)) * (i1,(j1 + 1)) holds
[i1,(j1 + 2)] in Indices (Gauge (C,n))
let n be Element of NAT ; ::_thesis: for f being FinSequence of (TOP-REAL 2) st f is_sequence_on Gauge (C,n) & len f > 1 holds
for i1, j1 being Element of NAT st front_left_cell (f,((len f) -' 1),(Gauge (C,n))) meets C & [i1,j1] in Indices (Gauge (C,n)) & f /. ((len f) -' 1) = (Gauge (C,n)) * (i1,j1) & [i1,(j1 + 1)] in Indices (Gauge (C,n)) & f /. (len f) = (Gauge (C,n)) * (i1,(j1 + 1)) holds
[i1,(j1 + 2)] in Indices (Gauge (C,n))
set G = Gauge (C,n);
A1: len (Gauge (C,n)) = width (Gauge (C,n)) by JORDAN8:def_1;
let f be FinSequence of (TOP-REAL 2); ::_thesis: ( f is_sequence_on Gauge (C,n) & len f > 1 implies for i1, j1 being Element of NAT st front_left_cell (f,((len f) -' 1),(Gauge (C,n))) meets C & [i1,j1] in Indices (Gauge (C,n)) & f /. ((len f) -' 1) = (Gauge (C,n)) * (i1,j1) & [i1,(j1 + 1)] in Indices (Gauge (C,n)) & f /. (len f) = (Gauge (C,n)) * (i1,(j1 + 1)) holds
[i1,(j1 + 2)] in Indices (Gauge (C,n)) )
assume that
A2: f is_sequence_on Gauge (C,n) and
A3: len f > 1 ; ::_thesis: for i1, j1 being Element of NAT st front_left_cell (f,((len f) -' 1),(Gauge (C,n))) meets C & [i1,j1] in Indices (Gauge (C,n)) & f /. ((len f) -' 1) = (Gauge (C,n)) * (i1,j1) & [i1,(j1 + 1)] in Indices (Gauge (C,n)) & f /. (len f) = (Gauge (C,n)) * (i1,(j1 + 1)) holds
[i1,(j1 + 2)] in Indices (Gauge (C,n))
A4: ( 1 <= (len f) -' 1 & ((len f) -' 1) + 1 = len f ) by A3, NAT_D:49, XREAL_1:235;
let i1, j1 be Element of NAT ; ::_thesis: ( front_left_cell (f,((len f) -' 1),(Gauge (C,n))) meets C & [i1,j1] in Indices (Gauge (C,n)) & f /. ((len f) -' 1) = (Gauge (C,n)) * (i1,j1) & [i1,(j1 + 1)] in Indices (Gauge (C,n)) & f /. (len f) = (Gauge (C,n)) * (i1,(j1 + 1)) implies [i1,(j1 + 2)] in Indices (Gauge (C,n)) )
assume that
A5: ( front_left_cell (f,((len f) -' 1),(Gauge (C,n))) meets C & [i1,j1] in Indices (Gauge (C,n)) & f /. ((len f) -' 1) = (Gauge (C,n)) * (i1,j1) ) and
A6: [i1,(j1 + 1)] in Indices (Gauge (C,n)) and
A7: f /. (len f) = (Gauge (C,n)) * (i1,(j1 + 1)) ; ::_thesis: [i1,(j1 + 2)] in Indices (Gauge (C,n))
A8: i1 <= len (Gauge (C,n)) by A6, MATRIX_1:38;
A9: i1 -' 1 <= i1 by NAT_D:35;
A10: j1 + 1 <= width (Gauge (C,n)) by A6, MATRIX_1:38;
A11: now__::_thesis:_not_(j1_+_1)_+_1_>_len_(Gauge_(C,n))
assume (j1 + 1) + 1 > len (Gauge (C,n)) ; ::_thesis: contradiction
then A12: (len (Gauge (C,n))) + 1 <= (j1 + 1) + 1 by NAT_1:13;
(j1 + 1) + 1 <= (len (Gauge (C,n))) + 1 by A1, A10, XREAL_1:6;
then (j1 + 1) + 1 = (len (Gauge (C,n))) + 1 by A12, XXREAL_0:1;
then cell ((Gauge (C,n)),(i1 -' 1),(len (Gauge (C,n)))) meets C by A2, A5, A6, A7, A4, GOBRD13:34;
hence contradiction by A8, A9, JORDAN8:15, XXREAL_0:2; ::_thesis: verum
end;
A13: 1 <= (j1 + 1) + 1 by NAT_1:12;
1 <= i1 by A6, MATRIX_1:38;
hence [i1,(j1 + 2)] in Indices (Gauge (C,n)) by A1, A8, A13, A11, MATRIX_1:36; ::_thesis: verum
end;
theorem :: JORDAN1H:57
for C being non empty compact non horizontal non vertical Subset of (TOP-REAL 2)
for n being Element of NAT
for f being FinSequence of (TOP-REAL 2) st f is_sequence_on Gauge (C,n) & len f > 1 holds
for i1, j1 being Element of NAT st front_left_cell (f,((len f) -' 1),(Gauge (C,n))) meets C & [i1,j1] in Indices (Gauge (C,n)) & f /. ((len f) -' 1) = (Gauge (C,n)) * (i1,j1) & [(i1 + 1),j1] in Indices (Gauge (C,n)) & f /. (len f) = (Gauge (C,n)) * ((i1 + 1),j1) holds
[(i1 + 2),j1] in Indices (Gauge (C,n))
proof
let C be non empty compact non horizontal non vertical Subset of (TOP-REAL 2); ::_thesis: for n being Element of NAT
for f being FinSequence of (TOP-REAL 2) st f is_sequence_on Gauge (C,n) & len f > 1 holds
for i1, j1 being Element of NAT st front_left_cell (f,((len f) -' 1),(Gauge (C,n))) meets C & [i1,j1] in Indices (Gauge (C,n)) & f /. ((len f) -' 1) = (Gauge (C,n)) * (i1,j1) & [(i1 + 1),j1] in Indices (Gauge (C,n)) & f /. (len f) = (Gauge (C,n)) * ((i1 + 1),j1) holds
[(i1 + 2),j1] in Indices (Gauge (C,n))
let n be Element of NAT ; ::_thesis: for f being FinSequence of (TOP-REAL 2) st f is_sequence_on Gauge (C,n) & len f > 1 holds
for i1, j1 being Element of NAT st front_left_cell (f,((len f) -' 1),(Gauge (C,n))) meets C & [i1,j1] in Indices (Gauge (C,n)) & f /. ((len f) -' 1) = (Gauge (C,n)) * (i1,j1) & [(i1 + 1),j1] in Indices (Gauge (C,n)) & f /. (len f) = (Gauge (C,n)) * ((i1 + 1),j1) holds
[(i1 + 2),j1] in Indices (Gauge (C,n))
set G = Gauge (C,n);
A1: len (Gauge (C,n)) = width (Gauge (C,n)) by JORDAN8:def_1;
let f be FinSequence of (TOP-REAL 2); ::_thesis: ( f is_sequence_on Gauge (C,n) & len f > 1 implies for i1, j1 being Element of NAT st front_left_cell (f,((len f) -' 1),(Gauge (C,n))) meets C & [i1,j1] in Indices (Gauge (C,n)) & f /. ((len f) -' 1) = (Gauge (C,n)) * (i1,j1) & [(i1 + 1),j1] in Indices (Gauge (C,n)) & f /. (len f) = (Gauge (C,n)) * ((i1 + 1),j1) holds
[(i1 + 2),j1] in Indices (Gauge (C,n)) )
assume that
A2: f is_sequence_on Gauge (C,n) and
A3: len f > 1 ; ::_thesis: for i1, j1 being Element of NAT st front_left_cell (f,((len f) -' 1),(Gauge (C,n))) meets C & [i1,j1] in Indices (Gauge (C,n)) & f /. ((len f) -' 1) = (Gauge (C,n)) * (i1,j1) & [(i1 + 1),j1] in Indices (Gauge (C,n)) & f /. (len f) = (Gauge (C,n)) * ((i1 + 1),j1) holds
[(i1 + 2),j1] in Indices (Gauge (C,n))
A4: ( 1 <= (len f) -' 1 & ((len f) -' 1) + 1 = len f ) by A3, NAT_D:49, XREAL_1:235;
let i1, j1 be Element of NAT ; ::_thesis: ( front_left_cell (f,((len f) -' 1),(Gauge (C,n))) meets C & [i1,j1] in Indices (Gauge (C,n)) & f /. ((len f) -' 1) = (Gauge (C,n)) * (i1,j1) & [(i1 + 1),j1] in Indices (Gauge (C,n)) & f /. (len f) = (Gauge (C,n)) * ((i1 + 1),j1) implies [(i1 + 2),j1] in Indices (Gauge (C,n)) )
assume that
A5: ( front_left_cell (f,((len f) -' 1),(Gauge (C,n))) meets C & [i1,j1] in Indices (Gauge (C,n)) & f /. ((len f) -' 1) = (Gauge (C,n)) * (i1,j1) ) and
A6: [(i1 + 1),j1] in Indices (Gauge (C,n)) and
A7: f /. (len f) = (Gauge (C,n)) * ((i1 + 1),j1) ; ::_thesis: [(i1 + 2),j1] in Indices (Gauge (C,n))
A8: j1 <= width (Gauge (C,n)) by A6, MATRIX_1:38;
A9: i1 + 1 <= len (Gauge (C,n)) by A6, MATRIX_1:38;
A10: now__::_thesis:_not_(i1_+_1)_+_1_>_len_(Gauge_(C,n))
assume (i1 + 1) + 1 > len (Gauge (C,n)) ; ::_thesis: contradiction
then A11: (len (Gauge (C,n))) + 1 <= (i1 + 1) + 1 by NAT_1:13;
(i1 + 1) + 1 <= (len (Gauge (C,n))) + 1 by A9, XREAL_1:6;
then (i1 + 1) + 1 = (len (Gauge (C,n))) + 1 by A11, XXREAL_0:1;
then cell ((Gauge (C,n)),(len (Gauge (C,n))),j1) meets C by A2, A5, A6, A7, A4, GOBRD13:36;
hence contradiction by A1, A8, JORDAN8:16; ::_thesis: verum
end;
A12: 1 <= (i1 + 1) + 1 by NAT_1:12;
1 <= j1 by A6, MATRIX_1:38;
hence [(i1 + 2),j1] in Indices (Gauge (C,n)) by A8, A12, A10, MATRIX_1:36; ::_thesis: verum
end;
theorem :: JORDAN1H:58
for C being non empty compact non horizontal non vertical Subset of (TOP-REAL 2)
for n being Element of NAT
for f being FinSequence of (TOP-REAL 2) st f is_sequence_on Gauge (C,n) & len f > 1 holds
for j1, i2 being Element of NAT st front_left_cell (f,((len f) -' 1),(Gauge (C,n))) meets C & [(i2 + 1),j1] in Indices (Gauge (C,n)) & f /. ((len f) -' 1) = (Gauge (C,n)) * ((i2 + 1),j1) & [i2,j1] in Indices (Gauge (C,n)) & f /. (len f) = (Gauge (C,n)) * (i2,j1) holds
[(i2 -' 1),j1] in Indices (Gauge (C,n))
proof
let C be non empty compact non horizontal non vertical Subset of (TOP-REAL 2); ::_thesis: for n being Element of NAT
for f being FinSequence of (TOP-REAL 2) st f is_sequence_on Gauge (C,n) & len f > 1 holds
for j1, i2 being Element of NAT st front_left_cell (f,((len f) -' 1),(Gauge (C,n))) meets C & [(i2 + 1),j1] in Indices (Gauge (C,n)) & f /. ((len f) -' 1) = (Gauge (C,n)) * ((i2 + 1),j1) & [i2,j1] in Indices (Gauge (C,n)) & f /. (len f) = (Gauge (C,n)) * (i2,j1) holds
[(i2 -' 1),j1] in Indices (Gauge (C,n))
let n be Element of NAT ; ::_thesis: for f being FinSequence of (TOP-REAL 2) st f is_sequence_on Gauge (C,n) & len f > 1 holds
for j1, i2 being Element of NAT st front_left_cell (f,((len f) -' 1),(Gauge (C,n))) meets C & [(i2 + 1),j1] in Indices (Gauge (C,n)) & f /. ((len f) -' 1) = (Gauge (C,n)) * ((i2 + 1),j1) & [i2,j1] in Indices (Gauge (C,n)) & f /. (len f) = (Gauge (C,n)) * (i2,j1) holds
[(i2 -' 1),j1] in Indices (Gauge (C,n))
set G = Gauge (C,n);
A1: len (Gauge (C,n)) = width (Gauge (C,n)) by JORDAN8:def_1;
let f be FinSequence of (TOP-REAL 2); ::_thesis: ( f is_sequence_on Gauge (C,n) & len f > 1 implies for j1, i2 being Element of NAT st front_left_cell (f,((len f) -' 1),(Gauge (C,n))) meets C & [(i2 + 1),j1] in Indices (Gauge (C,n)) & f /. ((len f) -' 1) = (Gauge (C,n)) * ((i2 + 1),j1) & [i2,j1] in Indices (Gauge (C,n)) & f /. (len f) = (Gauge (C,n)) * (i2,j1) holds
[(i2 -' 1),j1] in Indices (Gauge (C,n)) )
assume that
A2: f is_sequence_on Gauge (C,n) and
A3: len f > 1 ; ::_thesis: for j1, i2 being Element of NAT st front_left_cell (f,((len f) -' 1),(Gauge (C,n))) meets C & [(i2 + 1),j1] in Indices (Gauge (C,n)) & f /. ((len f) -' 1) = (Gauge (C,n)) * ((i2 + 1),j1) & [i2,j1] in Indices (Gauge (C,n)) & f /. (len f) = (Gauge (C,n)) * (i2,j1) holds
[(i2 -' 1),j1] in Indices (Gauge (C,n))
A4: ( 1 <= (len f) -' 1 & ((len f) -' 1) + 1 = len f ) by A3, NAT_D:49, XREAL_1:235;
let j1, i2 be Element of NAT ; ::_thesis: ( front_left_cell (f,((len f) -' 1),(Gauge (C,n))) meets C & [(i2 + 1),j1] in Indices (Gauge (C,n)) & f /. ((len f) -' 1) = (Gauge (C,n)) * ((i2 + 1),j1) & [i2,j1] in Indices (Gauge (C,n)) & f /. (len f) = (Gauge (C,n)) * (i2,j1) implies [(i2 -' 1),j1] in Indices (Gauge (C,n)) )
assume that
A5: ( front_left_cell (f,((len f) -' 1),(Gauge (C,n))) meets C & [(i2 + 1),j1] in Indices (Gauge (C,n)) & f /. ((len f) -' 1) = (Gauge (C,n)) * ((i2 + 1),j1) ) and
A6: [i2,j1] in Indices (Gauge (C,n)) and
A7: f /. (len f) = (Gauge (C,n)) * (i2,j1) ; ::_thesis: [(i2 -' 1),j1] in Indices (Gauge (C,n))
A8: j1 <= width (Gauge (C,n)) by A6, MATRIX_1:38;
A9: 1 <= i2 by A6, MATRIX_1:38;
A10: now__::_thesis:_not_i2_-'_1_<_1
assume i2 -' 1 < 1 ; ::_thesis: contradiction
then i2 <= 1 by NAT_1:14, NAT_D:36;
then i2 = 1 by A9, XXREAL_0:1;
then cell ((Gauge (C,n)),(1 -' 1),(j1 -' 1)) meets C by A2, A5, A6, A7, A4, GOBRD13:38;
then cell ((Gauge (C,n)),0,(j1 -' 1)) meets C by XREAL_1:232;
hence contradiction by A1, A8, JORDAN8:18, NAT_D:44; ::_thesis: verum
end;
i2 <= len (Gauge (C,n)) by A6, MATRIX_1:38;
then A11: i2 -' 1 <= len (Gauge (C,n)) by NAT_D:44;
1 <= j1 by A6, MATRIX_1:38;
hence [(i2 -' 1),j1] in Indices (Gauge (C,n)) by A8, A11, A10, MATRIX_1:36; ::_thesis: verum
end;
theorem :: JORDAN1H:59
for C being non empty compact non horizontal non vertical Subset of (TOP-REAL 2)
for n being Element of NAT
for f being FinSequence of (TOP-REAL 2) st f is_sequence_on Gauge (C,n) & len f > 1 holds
for i1, j2 being Element of NAT st front_left_cell (f,((len f) -' 1),(Gauge (C,n))) meets C & [i1,(j2 + 1)] in Indices (Gauge (C,n)) & f /. ((len f) -' 1) = (Gauge (C,n)) * (i1,(j2 + 1)) & [i1,j2] in Indices (Gauge (C,n)) & f /. (len f) = (Gauge (C,n)) * (i1,j2) holds
[i1,(j2 -' 1)] in Indices (Gauge (C,n))
proof
let C be non empty compact non horizontal non vertical Subset of (TOP-REAL 2); ::_thesis: for n being Element of NAT
for f being FinSequence of (TOP-REAL 2) st f is_sequence_on Gauge (C,n) & len f > 1 holds
for i1, j2 being Element of NAT st front_left_cell (f,((len f) -' 1),(Gauge (C,n))) meets C & [i1,(j2 + 1)] in Indices (Gauge (C,n)) & f /. ((len f) -' 1) = (Gauge (C,n)) * (i1,(j2 + 1)) & [i1,j2] in Indices (Gauge (C,n)) & f /. (len f) = (Gauge (C,n)) * (i1,j2) holds
[i1,(j2 -' 1)] in Indices (Gauge (C,n))
let n be Element of NAT ; ::_thesis: for f being FinSequence of (TOP-REAL 2) st f is_sequence_on Gauge (C,n) & len f > 1 holds
for i1, j2 being Element of NAT st front_left_cell (f,((len f) -' 1),(Gauge (C,n))) meets C & [i1,(j2 + 1)] in Indices (Gauge (C,n)) & f /. ((len f) -' 1) = (Gauge (C,n)) * (i1,(j2 + 1)) & [i1,j2] in Indices (Gauge (C,n)) & f /. (len f) = (Gauge (C,n)) * (i1,j2) holds
[i1,(j2 -' 1)] in Indices (Gauge (C,n))
set G = Gauge (C,n);
let f be FinSequence of (TOP-REAL 2); ::_thesis: ( f is_sequence_on Gauge (C,n) & len f > 1 implies for i1, j2 being Element of NAT st front_left_cell (f,((len f) -' 1),(Gauge (C,n))) meets C & [i1,(j2 + 1)] in Indices (Gauge (C,n)) & f /. ((len f) -' 1) = (Gauge (C,n)) * (i1,(j2 + 1)) & [i1,j2] in Indices (Gauge (C,n)) & f /. (len f) = (Gauge (C,n)) * (i1,j2) holds
[i1,(j2 -' 1)] in Indices (Gauge (C,n)) )
assume that
A1: f is_sequence_on Gauge (C,n) and
A2: len f > 1 ; ::_thesis: for i1, j2 being Element of NAT st front_left_cell (f,((len f) -' 1),(Gauge (C,n))) meets C & [i1,(j2 + 1)] in Indices (Gauge (C,n)) & f /. ((len f) -' 1) = (Gauge (C,n)) * (i1,(j2 + 1)) & [i1,j2] in Indices (Gauge (C,n)) & f /. (len f) = (Gauge (C,n)) * (i1,j2) holds
[i1,(j2 -' 1)] in Indices (Gauge (C,n))
A3: ( 1 <= (len f) -' 1 & ((len f) -' 1) + 1 = len f ) by A2, NAT_D:49, XREAL_1:235;
let i1, j2 be Element of NAT ; ::_thesis: ( front_left_cell (f,((len f) -' 1),(Gauge (C,n))) meets C & [i1,(j2 + 1)] in Indices (Gauge (C,n)) & f /. ((len f) -' 1) = (Gauge (C,n)) * (i1,(j2 + 1)) & [i1,j2] in Indices (Gauge (C,n)) & f /. (len f) = (Gauge (C,n)) * (i1,j2) implies [i1,(j2 -' 1)] in Indices (Gauge (C,n)) )
assume that
A4: front_left_cell (f,((len f) -' 1),(Gauge (C,n))) meets C and
A5: [i1,(j2 + 1)] in Indices (Gauge (C,n)) and
A6: f /. ((len f) -' 1) = (Gauge (C,n)) * (i1,(j2 + 1)) and
A7: [i1,j2] in Indices (Gauge (C,n)) and
A8: f /. (len f) = (Gauge (C,n)) * (i1,j2) ; ::_thesis: [i1,(j2 -' 1)] in Indices (Gauge (C,n))
A9: 1 <= j2 by A7, MATRIX_1:38;
A10: i1 <= len (Gauge (C,n)) by A5, MATRIX_1:38;
A11: now__::_thesis:_not_j2_-'_1_<_1
assume j2 -' 1 < 1 ; ::_thesis: contradiction
then j2 <= 1 by NAT_1:14, NAT_D:36;
then j2 = 1 by A9, XXREAL_0:1;
then cell ((Gauge (C,n)),i1,(1 -' 1)) meets C by A1, A4, A5, A6, A7, A8, A3, GOBRD13:40;
then cell ((Gauge (C,n)),i1,0) meets C by XREAL_1:232;
hence contradiction by A10, JORDAN8:17; ::_thesis: verum
end;
j2 <= width (Gauge (C,n)) by A7, MATRIX_1:38;
then A12: j2 -' 1 <= width (Gauge (C,n)) by NAT_D:44;
( 1 <= i1 & i1 <= len (Gauge (C,n)) ) by A7, MATRIX_1:38;
hence [i1,(j2 -' 1)] in Indices (Gauge (C,n)) by A12, A11, MATRIX_1:36; ::_thesis: verum
end;
theorem :: JORDAN1H:60
for C being non empty compact non horizontal non vertical Subset of (TOP-REAL 2)
for n being Element of NAT
for f being FinSequence of (TOP-REAL 2) st f is_sequence_on Gauge (C,n) & len f > 1 holds
for i1, j1 being Element of NAT st front_right_cell (f,((len f) -' 1),(Gauge (C,n))) meets C & [i1,j1] in Indices (Gauge (C,n)) & f /. ((len f) -' 1) = (Gauge (C,n)) * (i1,j1) & [i1,(j1 + 1)] in Indices (Gauge (C,n)) & f /. (len f) = (Gauge (C,n)) * (i1,(j1 + 1)) holds
[(i1 + 1),(j1 + 1)] in Indices (Gauge (C,n))
proof
let C be non empty compact non horizontal non vertical Subset of (TOP-REAL 2); ::_thesis: for n being Element of NAT
for f being FinSequence of (TOP-REAL 2) st f is_sequence_on Gauge (C,n) & len f > 1 holds
for i1, j1 being Element of NAT st front_right_cell (f,((len f) -' 1),(Gauge (C,n))) meets C & [i1,j1] in Indices (Gauge (C,n)) & f /. ((len f) -' 1) = (Gauge (C,n)) * (i1,j1) & [i1,(j1 + 1)] in Indices (Gauge (C,n)) & f /. (len f) = (Gauge (C,n)) * (i1,(j1 + 1)) holds
[(i1 + 1),(j1 + 1)] in Indices (Gauge (C,n))
let n be Element of NAT ; ::_thesis: for f being FinSequence of (TOP-REAL 2) st f is_sequence_on Gauge (C,n) & len f > 1 holds
for i1, j1 being Element of NAT st front_right_cell (f,((len f) -' 1),(Gauge (C,n))) meets C & [i1,j1] in Indices (Gauge (C,n)) & f /. ((len f) -' 1) = (Gauge (C,n)) * (i1,j1) & [i1,(j1 + 1)] in Indices (Gauge (C,n)) & f /. (len f) = (Gauge (C,n)) * (i1,(j1 + 1)) holds
[(i1 + 1),(j1 + 1)] in Indices (Gauge (C,n))
set G = Gauge (C,n);
A1: len (Gauge (C,n)) = width (Gauge (C,n)) by JORDAN8:def_1;
let f be FinSequence of (TOP-REAL 2); ::_thesis: ( f is_sequence_on Gauge (C,n) & len f > 1 implies for i1, j1 being Element of NAT st front_right_cell (f,((len f) -' 1),(Gauge (C,n))) meets C & [i1,j1] in Indices (Gauge (C,n)) & f /. ((len f) -' 1) = (Gauge (C,n)) * (i1,j1) & [i1,(j1 + 1)] in Indices (Gauge (C,n)) & f /. (len f) = (Gauge (C,n)) * (i1,(j1 + 1)) holds
[(i1 + 1),(j1 + 1)] in Indices (Gauge (C,n)) )
assume that
A2: f is_sequence_on Gauge (C,n) and
A3: len f > 1 ; ::_thesis: for i1, j1 being Element of NAT st front_right_cell (f,((len f) -' 1),(Gauge (C,n))) meets C & [i1,j1] in Indices (Gauge (C,n)) & f /. ((len f) -' 1) = (Gauge (C,n)) * (i1,j1) & [i1,(j1 + 1)] in Indices (Gauge (C,n)) & f /. (len f) = (Gauge (C,n)) * (i1,(j1 + 1)) holds
[(i1 + 1),(j1 + 1)] in Indices (Gauge (C,n))
A4: ( 1 <= (len f) -' 1 & ((len f) -' 1) + 1 = len f ) by A3, NAT_D:49, XREAL_1:235;
let i1, j1 be Element of NAT ; ::_thesis: ( front_right_cell (f,((len f) -' 1),(Gauge (C,n))) meets C & [i1,j1] in Indices (Gauge (C,n)) & f /. ((len f) -' 1) = (Gauge (C,n)) * (i1,j1) & [i1,(j1 + 1)] in Indices (Gauge (C,n)) & f /. (len f) = (Gauge (C,n)) * (i1,(j1 + 1)) implies [(i1 + 1),(j1 + 1)] in Indices (Gauge (C,n)) )
assume that
A5: ( front_right_cell (f,((len f) -' 1),(Gauge (C,n))) meets C & [i1,j1] in Indices (Gauge (C,n)) & f /. ((len f) -' 1) = (Gauge (C,n)) * (i1,j1) ) and
A6: [i1,(j1 + 1)] in Indices (Gauge (C,n)) and
A7: f /. (len f) = (Gauge (C,n)) * (i1,(j1 + 1)) ; ::_thesis: [(i1 + 1),(j1 + 1)] in Indices (Gauge (C,n))
A8: j1 + 1 <= width (Gauge (C,n)) by A6, MATRIX_1:38;
A9: i1 <= len (Gauge (C,n)) by A6, MATRIX_1:38;
A10: now__::_thesis:_not_i1_+_1_>_len_(Gauge_(C,n))
assume i1 + 1 > len (Gauge (C,n)) ; ::_thesis: contradiction
then A11: (len (Gauge (C,n))) + 1 <= i1 + 1 by NAT_1:13;
i1 + 1 <= (len (Gauge (C,n))) + 1 by A9, XREAL_1:6;
then i1 + 1 = (len (Gauge (C,n))) + 1 by A11, XXREAL_0:1;
then cell ((Gauge (C,n)),(len (Gauge (C,n))),(j1 + 1)) meets C by A2, A5, A6, A7, A4, GOBRD13:35;
hence contradiction by A1, A8, JORDAN8:16; ::_thesis: verum
end;
A12: 1 <= i1 + 1 by NAT_1:11;
1 <= j1 + 1 by A6, MATRIX_1:38;
hence [(i1 + 1),(j1 + 1)] in Indices (Gauge (C,n)) by A8, A12, A10, MATRIX_1:36; ::_thesis: verum
end;
theorem :: JORDAN1H:61
for C being non empty compact non horizontal non vertical Subset of (TOP-REAL 2)
for n being Element of NAT
for f being FinSequence of (TOP-REAL 2) st f is_sequence_on Gauge (C,n) & len f > 1 holds
for i1, j1 being Element of NAT st front_right_cell (f,((len f) -' 1),(Gauge (C,n))) meets C & [i1,j1] in Indices (Gauge (C,n)) & f /. ((len f) -' 1) = (Gauge (C,n)) * (i1,j1) & [(i1 + 1),j1] in Indices (Gauge (C,n)) & f /. (len f) = (Gauge (C,n)) * ((i1 + 1),j1) holds
[(i1 + 1),(j1 -' 1)] in Indices (Gauge (C,n))
proof
let C be non empty compact non horizontal non vertical Subset of (TOP-REAL 2); ::_thesis: for n being Element of NAT
for f being FinSequence of (TOP-REAL 2) st f is_sequence_on Gauge (C,n) & len f > 1 holds
for i1, j1 being Element of NAT st front_right_cell (f,((len f) -' 1),(Gauge (C,n))) meets C & [i1,j1] in Indices (Gauge (C,n)) & f /. ((len f) -' 1) = (Gauge (C,n)) * (i1,j1) & [(i1 + 1),j1] in Indices (Gauge (C,n)) & f /. (len f) = (Gauge (C,n)) * ((i1 + 1),j1) holds
[(i1 + 1),(j1 -' 1)] in Indices (Gauge (C,n))
let n be Element of NAT ; ::_thesis: for f being FinSequence of (TOP-REAL 2) st f is_sequence_on Gauge (C,n) & len f > 1 holds
for i1, j1 being Element of NAT st front_right_cell (f,((len f) -' 1),(Gauge (C,n))) meets C & [i1,j1] in Indices (Gauge (C,n)) & f /. ((len f) -' 1) = (Gauge (C,n)) * (i1,j1) & [(i1 + 1),j1] in Indices (Gauge (C,n)) & f /. (len f) = (Gauge (C,n)) * ((i1 + 1),j1) holds
[(i1 + 1),(j1 -' 1)] in Indices (Gauge (C,n))
set G = Gauge (C,n);
let f be FinSequence of (TOP-REAL 2); ::_thesis: ( f is_sequence_on Gauge (C,n) & len f > 1 implies for i1, j1 being Element of NAT st front_right_cell (f,((len f) -' 1),(Gauge (C,n))) meets C & [i1,j1] in Indices (Gauge (C,n)) & f /. ((len f) -' 1) = (Gauge (C,n)) * (i1,j1) & [(i1 + 1),j1] in Indices (Gauge (C,n)) & f /. (len f) = (Gauge (C,n)) * ((i1 + 1),j1) holds
[(i1 + 1),(j1 -' 1)] in Indices (Gauge (C,n)) )
assume that
A1: f is_sequence_on Gauge (C,n) and
A2: len f > 1 ; ::_thesis: for i1, j1 being Element of NAT st front_right_cell (f,((len f) -' 1),(Gauge (C,n))) meets C & [i1,j1] in Indices (Gauge (C,n)) & f /. ((len f) -' 1) = (Gauge (C,n)) * (i1,j1) & [(i1 + 1),j1] in Indices (Gauge (C,n)) & f /. (len f) = (Gauge (C,n)) * ((i1 + 1),j1) holds
[(i1 + 1),(j1 -' 1)] in Indices (Gauge (C,n))
A3: ( 1 <= (len f) -' 1 & ((len f) -' 1) + 1 = len f ) by A2, NAT_D:49, XREAL_1:235;
let i1, j1 be Element of NAT ; ::_thesis: ( front_right_cell (f,((len f) -' 1),(Gauge (C,n))) meets C & [i1,j1] in Indices (Gauge (C,n)) & f /. ((len f) -' 1) = (Gauge (C,n)) * (i1,j1) & [(i1 + 1),j1] in Indices (Gauge (C,n)) & f /. (len f) = (Gauge (C,n)) * ((i1 + 1),j1) implies [(i1 + 1),(j1 -' 1)] in Indices (Gauge (C,n)) )
assume that
A4: ( front_right_cell (f,((len f) -' 1),(Gauge (C,n))) meets C & [i1,j1] in Indices (Gauge (C,n)) & f /. ((len f) -' 1) = (Gauge (C,n)) * (i1,j1) ) and
A5: [(i1 + 1),j1] in Indices (Gauge (C,n)) and
A6: f /. (len f) = (Gauge (C,n)) * ((i1 + 1),j1) ; ::_thesis: [(i1 + 1),(j1 -' 1)] in Indices (Gauge (C,n))
A7: i1 + 1 <= len (Gauge (C,n)) by A5, MATRIX_1:38;
A8: 1 <= j1 by A5, MATRIX_1:38;
A9: now__::_thesis:_not_j1_-'_1_<_1
assume j1 -' 1 < 1 ; ::_thesis: contradiction
then j1 <= 1 by NAT_1:14, NAT_D:36;
then j1 = 1 by A8, XXREAL_0:1;
then cell ((Gauge (C,n)),(i1 + 1),(1 -' 1)) meets C by A1, A4, A5, A6, A3, GOBRD13:37;
then cell ((Gauge (C,n)),(i1 + 1),0) meets C by XREAL_1:232;
hence contradiction by A7, JORDAN8:17; ::_thesis: verum
end;
A10: j1 -' 1 <= j1 by NAT_D:35;
j1 <= width (Gauge (C,n)) by A5, MATRIX_1:38;
then A11: j1 -' 1 <= width (Gauge (C,n)) by A10, XXREAL_0:2;
1 <= i1 + 1 by A5, MATRIX_1:38;
hence [(i1 + 1),(j1 -' 1)] in Indices (Gauge (C,n)) by A7, A11, A9, MATRIX_1:36; ::_thesis: verum
end;
theorem :: JORDAN1H:62
for C being non empty compact non horizontal non vertical Subset of (TOP-REAL 2)
for n being Element of NAT
for f being FinSequence of (TOP-REAL 2) st f is_sequence_on Gauge (C,n) & len f > 1 holds
for j1, i2 being Element of NAT st front_right_cell (f,((len f) -' 1),(Gauge (C,n))) meets C & [(i2 + 1),j1] in Indices (Gauge (C,n)) & f /. ((len f) -' 1) = (Gauge (C,n)) * ((i2 + 1),j1) & [i2,j1] in Indices (Gauge (C,n)) & f /. (len f) = (Gauge (C,n)) * (i2,j1) holds
[i2,(j1 + 1)] in Indices (Gauge (C,n))
proof
let C be non empty compact non horizontal non vertical Subset of (TOP-REAL 2); ::_thesis: for n being Element of NAT
for f being FinSequence of (TOP-REAL 2) st f is_sequence_on Gauge (C,n) & len f > 1 holds
for j1, i2 being Element of NAT st front_right_cell (f,((len f) -' 1),(Gauge (C,n))) meets C & [(i2 + 1),j1] in Indices (Gauge (C,n)) & f /. ((len f) -' 1) = (Gauge (C,n)) * ((i2 + 1),j1) & [i2,j1] in Indices (Gauge (C,n)) & f /. (len f) = (Gauge (C,n)) * (i2,j1) holds
[i2,(j1 + 1)] in Indices (Gauge (C,n))
let n be Element of NAT ; ::_thesis: for f being FinSequence of (TOP-REAL 2) st f is_sequence_on Gauge (C,n) & len f > 1 holds
for j1, i2 being Element of NAT st front_right_cell (f,((len f) -' 1),(Gauge (C,n))) meets C & [(i2 + 1),j1] in Indices (Gauge (C,n)) & f /. ((len f) -' 1) = (Gauge (C,n)) * ((i2 + 1),j1) & [i2,j1] in Indices (Gauge (C,n)) & f /. (len f) = (Gauge (C,n)) * (i2,j1) holds
[i2,(j1 + 1)] in Indices (Gauge (C,n))
set G = Gauge (C,n);
let f be FinSequence of (TOP-REAL 2); ::_thesis: ( f is_sequence_on Gauge (C,n) & len f > 1 implies for j1, i2 being Element of NAT st front_right_cell (f,((len f) -' 1),(Gauge (C,n))) meets C & [(i2 + 1),j1] in Indices (Gauge (C,n)) & f /. ((len f) -' 1) = (Gauge (C,n)) * ((i2 + 1),j1) & [i2,j1] in Indices (Gauge (C,n)) & f /. (len f) = (Gauge (C,n)) * (i2,j1) holds
[i2,(j1 + 1)] in Indices (Gauge (C,n)) )
assume that
A1: f is_sequence_on Gauge (C,n) and
A2: len f > 1 ; ::_thesis: for j1, i2 being Element of NAT st front_right_cell (f,((len f) -' 1),(Gauge (C,n))) meets C & [(i2 + 1),j1] in Indices (Gauge (C,n)) & f /. ((len f) -' 1) = (Gauge (C,n)) * ((i2 + 1),j1) & [i2,j1] in Indices (Gauge (C,n)) & f /. (len f) = (Gauge (C,n)) * (i2,j1) holds
[i2,(j1 + 1)] in Indices (Gauge (C,n))
A3: ( 1 <= (len f) -' 1 & ((len f) -' 1) + 1 = len f ) by A2, NAT_D:49, XREAL_1:235;
A4: len (Gauge (C,n)) = width (Gauge (C,n)) by JORDAN8:def_1;
let j1, i2 be Element of NAT ; ::_thesis: ( front_right_cell (f,((len f) -' 1),(Gauge (C,n))) meets C & [(i2 + 1),j1] in Indices (Gauge (C,n)) & f /. ((len f) -' 1) = (Gauge (C,n)) * ((i2 + 1),j1) & [i2,j1] in Indices (Gauge (C,n)) & f /. (len f) = (Gauge (C,n)) * (i2,j1) implies [i2,(j1 + 1)] in Indices (Gauge (C,n)) )
assume that
A5: ( front_right_cell (f,((len f) -' 1),(Gauge (C,n))) meets C & [(i2 + 1),j1] in Indices (Gauge (C,n)) & f /. ((len f) -' 1) = (Gauge (C,n)) * ((i2 + 1),j1) ) and
A6: [i2,j1] in Indices (Gauge (C,n)) and
A7: f /. (len f) = (Gauge (C,n)) * (i2,j1) ; ::_thesis: [i2,(j1 + 1)] in Indices (Gauge (C,n))
A8: i2 <= len (Gauge (C,n)) by A6, MATRIX_1:38;
A9: j1 <= width (Gauge (C,n)) by A6, MATRIX_1:38;
A10: now__::_thesis:_not_j1_+_1_>_len_(Gauge_(C,n))
assume j1 + 1 > len (Gauge (C,n)) ; ::_thesis: contradiction
then A11: (len (Gauge (C,n))) + 1 <= j1 + 1 by NAT_1:13;
j1 + 1 <= (len (Gauge (C,n))) + 1 by A9, A4, XREAL_1:6;
then j1 + 1 = (len (Gauge (C,n))) + 1 by A11, XXREAL_0:1;
then cell ((Gauge (C,n)),(i2 -' 1),(len (Gauge (C,n)))) meets C by A1, A5, A6, A7, A3, GOBRD13:39;
hence contradiction by A8, JORDAN8:15, NAT_D:44; ::_thesis: verum
end;
A12: 1 <= j1 + 1 by NAT_1:11;
1 <= i2 by A6, MATRIX_1:38;
hence [i2,(j1 + 1)] in Indices (Gauge (C,n)) by A8, A12, A4, A10, MATRIX_1:36; ::_thesis: verum
end;
theorem :: JORDAN1H:63
for C being non empty compact non horizontal non vertical Subset of (TOP-REAL 2)
for n being Element of NAT
for f being FinSequence of (TOP-REAL 2) st f is_sequence_on Gauge (C,n) & len f > 1 holds
for i1, j2 being Element of NAT st front_right_cell (f,((len f) -' 1),(Gauge (C,n))) meets C & [i1,(j2 + 1)] in Indices (Gauge (C,n)) & f /. ((len f) -' 1) = (Gauge (C,n)) * (i1,(j2 + 1)) & [i1,j2] in Indices (Gauge (C,n)) & f /. (len f) = (Gauge (C,n)) * (i1,j2) holds
[(i1 -' 1),j2] in Indices (Gauge (C,n))
proof
let C be non empty compact non horizontal non vertical Subset of (TOP-REAL 2); ::_thesis: for n being Element of NAT
for f being FinSequence of (TOP-REAL 2) st f is_sequence_on Gauge (C,n) & len f > 1 holds
for i1, j2 being Element of NAT st front_right_cell (f,((len f) -' 1),(Gauge (C,n))) meets C & [i1,(j2 + 1)] in Indices (Gauge (C,n)) & f /. ((len f) -' 1) = (Gauge (C,n)) * (i1,(j2 + 1)) & [i1,j2] in Indices (Gauge (C,n)) & f /. (len f) = (Gauge (C,n)) * (i1,j2) holds
[(i1 -' 1),j2] in Indices (Gauge (C,n))
let n be Element of NAT ; ::_thesis: for f being FinSequence of (TOP-REAL 2) st f is_sequence_on Gauge (C,n) & len f > 1 holds
for i1, j2 being Element of NAT st front_right_cell (f,((len f) -' 1),(Gauge (C,n))) meets C & [i1,(j2 + 1)] in Indices (Gauge (C,n)) & f /. ((len f) -' 1) = (Gauge (C,n)) * (i1,(j2 + 1)) & [i1,j2] in Indices (Gauge (C,n)) & f /. (len f) = (Gauge (C,n)) * (i1,j2) holds
[(i1 -' 1),j2] in Indices (Gauge (C,n))
set G = Gauge (C,n);
A1: len (Gauge (C,n)) = width (Gauge (C,n)) by JORDAN8:def_1;
let f be FinSequence of (TOP-REAL 2); ::_thesis: ( f is_sequence_on Gauge (C,n) & len f > 1 implies for i1, j2 being Element of NAT st front_right_cell (f,((len f) -' 1),(Gauge (C,n))) meets C & [i1,(j2 + 1)] in Indices (Gauge (C,n)) & f /. ((len f) -' 1) = (Gauge (C,n)) * (i1,(j2 + 1)) & [i1,j2] in Indices (Gauge (C,n)) & f /. (len f) = (Gauge (C,n)) * (i1,j2) holds
[(i1 -' 1),j2] in Indices (Gauge (C,n)) )
assume that
A2: f is_sequence_on Gauge (C,n) and
A3: len f > 1 ; ::_thesis: for i1, j2 being Element of NAT st front_right_cell (f,((len f) -' 1),(Gauge (C,n))) meets C & [i1,(j2 + 1)] in Indices (Gauge (C,n)) & f /. ((len f) -' 1) = (Gauge (C,n)) * (i1,(j2 + 1)) & [i1,j2] in Indices (Gauge (C,n)) & f /. (len f) = (Gauge (C,n)) * (i1,j2) holds
[(i1 -' 1),j2] in Indices (Gauge (C,n))
A4: ( 1 <= (len f) -' 1 & ((len f) -' 1) + 1 = len f ) by A3, NAT_D:49, XREAL_1:235;
let i1, j2 be Element of NAT ; ::_thesis: ( front_right_cell (f,((len f) -' 1),(Gauge (C,n))) meets C & [i1,(j2 + 1)] in Indices (Gauge (C,n)) & f /. ((len f) -' 1) = (Gauge (C,n)) * (i1,(j2 + 1)) & [i1,j2] in Indices (Gauge (C,n)) & f /. (len f) = (Gauge (C,n)) * (i1,j2) implies [(i1 -' 1),j2] in Indices (Gauge (C,n)) )
assume that
A5: ( front_right_cell (f,((len f) -' 1),(Gauge (C,n))) meets C & [i1,(j2 + 1)] in Indices (Gauge (C,n)) & f /. ((len f) -' 1) = (Gauge (C,n)) * (i1,(j2 + 1)) ) and
A6: [i1,j2] in Indices (Gauge (C,n)) and
A7: f /. (len f) = (Gauge (C,n)) * (i1,j2) ; ::_thesis: [(i1 -' 1),j2] in Indices (Gauge (C,n))
A8: j2 <= width (Gauge (C,n)) by A6, MATRIX_1:38;
A9: 1 <= i1 by A6, MATRIX_1:38;
A10: now__::_thesis:_not_i1_-'_1_<_1
assume i1 -' 1 < 1 ; ::_thesis: contradiction
then i1 <= 1 by NAT_1:14, NAT_D:36;
then i1 = 1 by A9, XXREAL_0:1;
then cell ((Gauge (C,n)),(1 -' 1),(j2 -' 1)) meets C by A2, A5, A6, A7, A4, GOBRD13:41;
then cell ((Gauge (C,n)),0,(j2 -' 1)) meets C by XREAL_1:232;
hence contradiction by A1, A8, JORDAN8:18, NAT_D:44; ::_thesis: verum
end;
i1 <= len (Gauge (C,n)) by A6, MATRIX_1:38;
then A11: i1 -' 1 <= len (Gauge (C,n)) by NAT_D:44;
1 <= j2 by A6, MATRIX_1:38;
hence [(i1 -' 1),j2] in Indices (Gauge (C,n)) by A8, A11, A10, MATRIX_1:36; ::_thesis: verum
end;