:: Upper and Lower Sequence on the Cage, Upper and Lower Arcs
:: by Robert Milewski
::
:: Received April 5, 2002
:: Copyright (c) 2002-2012 Association of Mizar Users


begin

theorem Th1: :: JORDAN1J:1
for G being Go-board
for i1, i2, j1, j2 being Element of NAT st 1 <= j1 & j1 <= width G & 1 <= j2 & j2 <= width G & 1 <= i1 & i1 < i2 & i2 <= len G holds
(G * (i1,j1)) `1 < (G * (i2,j2)) `1
proof end;

theorem Th2: :: JORDAN1J:2
for G being Go-board
for i1, i2, j1, j2 being Element of NAT st 1 <= i1 & i1 <= len G & 1 <= i2 & i2 <= len G & 1 <= j1 & j1 < j2 & j2 <= width G holds
(G * (i1,j1)) `2 < (G * (i2,j2)) `2
proof end;

registration
let f be non empty FinSequence;
let g be FinSequence;
cluster f ^' g -> non empty ;
coherence
not f ^' g is empty
proof end;
end;

theorem Th3: :: JORDAN1J:3
for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2)
for n being Element of NAT holds (L~ ((Cage (C,n)) -: (E-max (L~ (Cage (C,n)))))) /\ (L~ ((Cage (C,n)) :- (E-max (L~ (Cage (C,n)))))) = {(N-min (L~ (Cage (C,n)))),(E-max (L~ (Cage (C,n))))}
proof end;

theorem Th4: :: JORDAN1J:4
for n being Element of NAT
for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) holds Upper_Seq (C,n) = (Rotate ((Cage (C,n)),(E-max (L~ (Cage (C,n)))))) :- (W-min (L~ (Cage (C,n))))
proof end;

theorem :: JORDAN1J:5
for n being Element of NAT
for C being compact non horizontal non vertical Subset of (TOP-REAL 2) holds
( W-min (L~ (Cage (C,n))) in rng (Upper_Seq (C,n)) & W-min (L~ (Cage (C,n))) in L~ (Upper_Seq (C,n)) )
proof end;

theorem :: JORDAN1J:6
for n being Element of NAT
for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) holds
( W-max (L~ (Cage (C,n))) in rng (Upper_Seq (C,n)) & W-max (L~ (Cage (C,n))) in L~ (Upper_Seq (C,n)) )
proof end;

theorem Th7: :: JORDAN1J:7
for n being Element of NAT
for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) holds
( N-min (L~ (Cage (C,n))) in rng (Upper_Seq (C,n)) & N-min (L~ (Cage (C,n))) in L~ (Upper_Seq (C,n)) )
proof end;

theorem :: JORDAN1J:8
for n being Element of NAT
for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) holds
( N-max (L~ (Cage (C,n))) in rng (Upper_Seq (C,n)) & N-max (L~ (Cage (C,n))) in L~ (Upper_Seq (C,n)) )
proof end;

theorem :: JORDAN1J:9
for n being Element of NAT
for C being compact non horizontal non vertical Subset of (TOP-REAL 2) holds
( E-max (L~ (Cage (C,n))) in rng (Upper_Seq (C,n)) & E-max (L~ (Cage (C,n))) in L~ (Upper_Seq (C,n)) )
proof end;

theorem :: JORDAN1J:10
for n being Element of NAT
for C being compact non horizontal non vertical Subset of (TOP-REAL 2) holds
( E-max (L~ (Cage (C,n))) in rng (Lower_Seq (C,n)) & E-max (L~ (Cage (C,n))) in L~ (Lower_Seq (C,n)) )
proof end;

theorem :: JORDAN1J:11
for n being Element of NAT
for C being compact non horizontal non vertical Subset of (TOP-REAL 2) holds
( E-min (L~ (Cage (C,n))) in rng (Lower_Seq (C,n)) & E-min (L~ (Cage (C,n))) in L~ (Lower_Seq (C,n)) )
proof end;

theorem Th12: :: JORDAN1J:12
for n being Element of NAT
for C being compact non horizontal non vertical Subset of (TOP-REAL 2) holds
( S-max (L~ (Cage (C,n))) in rng (Lower_Seq (C,n)) & S-max (L~ (Cage (C,n))) in L~ (Lower_Seq (C,n)) )
proof end;

theorem :: JORDAN1J:13
for n being Element of NAT
for C being compact non horizontal non vertical Subset of (TOP-REAL 2) holds
( S-min (L~ (Cage (C,n))) in rng (Lower_Seq (C,n)) & S-min (L~ (Cage (C,n))) in L~ (Lower_Seq (C,n)) )
proof end;

theorem :: JORDAN1J:14
for n being Element of NAT
for C being compact non horizontal non vertical Subset of (TOP-REAL 2) holds
( W-min (L~ (Cage (C,n))) in rng (Lower_Seq (C,n)) & W-min (L~ (Cage (C,n))) in L~ (Lower_Seq (C,n)) )
proof end;

theorem Th15: :: JORDAN1J:15
for X, Y being non empty compact Subset of (TOP-REAL 2) st X c= Y & N-min Y in X holds
N-min X = N-min Y
proof end;

theorem Th16: :: JORDAN1J:16
for X, Y being non empty compact Subset of (TOP-REAL 2) st X c= Y & N-max Y in X holds
N-max X = N-max Y
proof end;

theorem Th17: :: JORDAN1J:17
for X, Y being non empty compact Subset of (TOP-REAL 2) st X c= Y & E-min Y in X holds
E-min X = E-min Y
proof end;

theorem Th18: :: JORDAN1J:18
for X, Y being non empty compact Subset of (TOP-REAL 2) st X c= Y & E-max Y in X holds
E-max X = E-max Y
proof end;

theorem Th19: :: JORDAN1J:19
for X, Y being non empty compact Subset of (TOP-REAL 2) st X c= Y & S-min Y in X holds
S-min X = S-min Y
proof end;

theorem Th20: :: JORDAN1J:20
for X, Y being non empty compact Subset of (TOP-REAL 2) st X c= Y & S-max Y in X holds
S-max X = S-max Y
proof end;

theorem Th21: :: JORDAN1J:21
for X, Y being non empty compact Subset of (TOP-REAL 2) st X c= Y & W-min Y in X holds
W-min X = W-min Y
proof end;

theorem Th22: :: JORDAN1J:22
for X, Y being non empty compact Subset of (TOP-REAL 2) st X c= Y & W-max Y in X holds
W-max X = W-max Y
proof end;

theorem Th23: :: JORDAN1J:23
for X, Y being non empty compact Subset of (TOP-REAL 2) st N-bound X <= N-bound Y holds
N-bound (X \/ Y) = N-bound Y
proof end;

theorem Th24: :: JORDAN1J:24
for X, Y being non empty compact Subset of (TOP-REAL 2) st E-bound X <= E-bound Y holds
E-bound (X \/ Y) = E-bound Y
proof end;

theorem Th25: :: JORDAN1J:25
for X, Y being non empty compact Subset of (TOP-REAL 2) st S-bound X <= S-bound Y holds
S-bound (X \/ Y) = S-bound X
proof end;

theorem Th26: :: JORDAN1J:26
for X, Y being non empty compact Subset of (TOP-REAL 2) st W-bound X <= W-bound Y holds
W-bound (X \/ Y) = W-bound X
proof end;

theorem :: JORDAN1J:27
for X, Y being non empty compact Subset of (TOP-REAL 2) st N-bound X < N-bound Y holds
N-min (X \/ Y) = N-min Y
proof end;

theorem :: JORDAN1J:28
for X, Y being non empty compact Subset of (TOP-REAL 2) st N-bound X < N-bound Y holds
N-max (X \/ Y) = N-max Y
proof end;

theorem :: JORDAN1J:29
for X, Y being non empty compact Subset of (TOP-REAL 2) st E-bound X < E-bound Y holds
E-min (X \/ Y) = E-min Y
proof end;

theorem :: JORDAN1J:30
for X, Y being non empty compact Subset of (TOP-REAL 2) st E-bound X < E-bound Y holds
E-max (X \/ Y) = E-max Y
proof end;

theorem :: JORDAN1J:31
for X, Y being non empty compact Subset of (TOP-REAL 2) st S-bound X < S-bound Y holds
S-min (X \/ Y) = S-min X
proof end;

theorem :: JORDAN1J:32
for X, Y being non empty compact Subset of (TOP-REAL 2) st S-bound X < S-bound Y holds
S-max (X \/ Y) = S-max X
proof end;

theorem Th33: :: JORDAN1J:33
for X, Y being non empty compact Subset of (TOP-REAL 2) st W-bound X < W-bound Y holds
W-min (X \/ Y) = W-min X
proof end;

theorem :: JORDAN1J:34
for X, Y being non empty compact Subset of (TOP-REAL 2) st W-bound X < W-bound Y holds
W-max (X \/ Y) = W-max X
proof end;

theorem Th35: :: JORDAN1J:35
for f being FinSequence of (TOP-REAL 2)
for p being Point of (TOP-REAL 2) st f is being_S-Seq & p in L~ f holds
(L_Cut (f,p)) /. (len (L_Cut (f,p))) = f /. (len f)
proof end;

theorem Th36: :: JORDAN1J:36
for f being non constant standard special_circular_sequence
for p, q being Point of (TOP-REAL 2)
for g being connected Subset of (TOP-REAL 2) st p in RightComp f & q in LeftComp f & p in g & q in g holds
g meets L~ f
proof end;

registration
cluster non empty non trivial V13() V16( NAT ) V17( the U1 of (TOP-REAL 2)) Function-like one-to-one non constant V26() FinSequence-like FinSubsequence-like special unfolded s.n.c. being_S-Seq s.c.c. standard for FinSequence of the U1 of (TOP-REAL 2);
existence
ex b1 being being_S-Seq FinSequence of (TOP-REAL 2) st
( not b1 is constant & b1 is standard & b1 is s.c.c. )
proof end;
end;

theorem Th37: :: JORDAN1J:37
for f being S-Sequence_in_R2
for p being Point of (TOP-REAL 2) st p in rng f holds
L_Cut (f,p) = mid (f,(p .. f),(len f))
proof end;

theorem Th38: :: JORDAN1J:38
for M being Go-board
for f being S-Sequence_in_R2 st f is_sequence_on M holds
for p being Point of (TOP-REAL 2) st p in rng f holds
R_Cut (f,p) is_sequence_on M
proof end;

theorem Th39: :: JORDAN1J:39
for M being Go-board
for f being S-Sequence_in_R2 st f is_sequence_on M holds
for p being Point of (TOP-REAL 2) st p in rng f holds
L_Cut (f,p) is_sequence_on M
proof end;

theorem Th40: :: JORDAN1J:40
for G being Go-board
for f being FinSequence of (TOP-REAL 2) st f is_sequence_on G holds
for i, j being Element of NAT st 1 <= i & i <= len G & 1 <= j & j <= width G & G * (i,j) in L~ f holds
G * (i,j) in rng f
proof end;

theorem :: JORDAN1J:41
for f being S-Sequence_in_R2
for g being FinSequence of (TOP-REAL 2) st g is unfolded & g is s.n.c. & g is one-to-one & (L~ f) /\ (L~ g) = {(f /. 1)} & f /. 1 = g /. (len g) & ( for i being Element of NAT st 1 <= i & i + 2 <= len f holds
(LSeg (f,i)) /\ (LSeg ((f /. (len f)),(g /. 1))) = {} ) & ( for i being Element of NAT st 2 <= i & i + 1 <= len g holds
(LSeg (g,i)) /\ (LSeg ((f /. (len f)),(g /. 1))) = {} ) holds
f ^ g is s.c.c.
proof end;

theorem :: JORDAN1J:42
for n being Element of NAT
for C being non empty compact non horizontal non vertical Subset of (TOP-REAL 2) ex i being Element of NAT st
( 1 <= i & i + 1 <= len (Gauge (C,n)) & W-min C in cell ((Gauge (C,n)),1,i) & W-min C <> (Gauge (C,n)) * (2,i) )
proof end;

theorem Th43: :: JORDAN1J:43
for f being S-Sequence_in_R2
for p being Point of (TOP-REAL 2) st p in L~ f & f . (len f) in L~ (R_Cut (f,p)) holds
f . (len f) = p
proof end;

theorem Th44: :: JORDAN1J:44
for f being FinSequence of (TOP-REAL 2)
for p being Point of (TOP-REAL 2) holds R_Cut (f,p) <> {}
proof end;

theorem Th45: :: JORDAN1J:45
for f being FinSequence of (TOP-REAL 2)
for p being Point of (TOP-REAL 2) st p in L~ f holds
(R_Cut (f,p)) /. (len (R_Cut (f,p))) = p
proof end;

theorem Th46: :: JORDAN1J:46
for n being Element of NAT
for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2)
for p being Point of (TOP-REAL 2) st p in L~ (Upper_Seq (C,n)) & p `1 = E-bound (L~ (Cage (C,n))) holds
p = E-max (L~ (Cage (C,n)))
proof end;

theorem :: JORDAN1J:47
for n being Element of NAT
for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2)
for p being Point of (TOP-REAL 2) st p in L~ (Lower_Seq (C,n)) & p `1 = W-bound (L~ (Cage (C,n))) holds
p = W-min (L~ (Cage (C,n)))
proof end;

theorem :: JORDAN1J:48
for G being Go-board
for f, g being FinSequence of (TOP-REAL 2)
for k being Element of NAT st 1 <= k & k < len f & f ^ g is_sequence_on G holds
( left_cell ((f ^ g),k,G) = left_cell (f,k,G) & right_cell ((f ^ g),k,G) = right_cell (f,k,G) )
proof end;

theorem Th49: :: JORDAN1J:49
for D being set
for f, g being FinSequence of D
for i being Element of NAT st i <= len f holds
(f ^' g) | i = f | i
proof end;

theorem Th50: :: JORDAN1J:50
for D being set
for f, g being FinSequence of D holds (f ^' g) | (len f) = f
proof end;

theorem Th51: :: JORDAN1J:51
for G being Go-board
for f, g being FinSequence of (TOP-REAL 2)
for k being Element of NAT st 1 <= k & k < len f & f ^' g is_sequence_on G holds
( left_cell ((f ^' g),k,G) = left_cell (f,k,G) & right_cell ((f ^' g),k,G) = right_cell (f,k,G) )
proof end;

theorem Th52: :: JORDAN1J:52
for G being Go-board
for f being S-Sequence_in_R2
for p being Point of (TOP-REAL 2)
for k being Element of NAT st 1 <= k & k < p .. f & f is_sequence_on G & p in rng f holds
( left_cell ((R_Cut (f,p)),k,G) = left_cell (f,k,G) & right_cell ((R_Cut (f,p)),k,G) = right_cell (f,k,G) )
proof end;

theorem Th53: :: JORDAN1J:53
for G being Go-board
for f being FinSequence of (TOP-REAL 2)
for p being Point of (TOP-REAL 2)
for k being Element of NAT st 1 <= k & k < p .. f & f is_sequence_on G holds
( left_cell ((f -: p),k,G) = left_cell (f,k,G) & right_cell ((f -: p),k,G) = right_cell (f,k,G) )
proof end;

theorem Th54: :: JORDAN1J:54
for f, g being FinSequence of (TOP-REAL 2) st f is unfolded & f is s.n.c. & f is one-to-one & g is unfolded & g is s.n.c. & g is one-to-one & f /. (len f) = g /. 1 & (L~ f) /\ (L~ g) = {(g /. 1)} holds
f ^' g is s.n.c.
proof end;

theorem Th55: :: JORDAN1J:55
for f, g being FinSequence of (TOP-REAL 2) st f is one-to-one & g is one-to-one & (rng f) /\ (rng g) c= {(g /. 1)} holds
f ^' g is one-to-one
proof end;

theorem Th56: :: JORDAN1J:56
for f being FinSequence of (TOP-REAL 2)
for p being Point of (TOP-REAL 2) st f is being_S-Seq & p in rng f & p <> f . 1 holds
(Index (p,f)) + 1 = p .. f
proof end;

theorem Th57: :: JORDAN1J:57
for n being Element of NAT
for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2)
for i, j, k being Element of NAT st 1 < i & i < len (Gauge (C,n)) & 1 <= j & k <= width (Gauge (C,n)) & (Gauge (C,n)) * (i,k) in L~ (Upper_Seq (C,n)) & (Gauge (C,n)) * (i,j) in L~ (Lower_Seq (C,n)) holds
j <> k
proof end;

theorem Th58: :: JORDAN1J:58
for n being Element of NAT
for C being Simple_closed_curve
for i, j, k being Element of NAT st 1 < i & i < len (Gauge (C,n)) & 1 <= j & j <= k & k <= width (Gauge (C,n)) & (LSeg (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * (i,k)))) /\ (L~ (Upper_Seq (C,n))) = {((Gauge (C,n)) * (i,k))} & (LSeg (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * (i,k)))) /\ (L~ (Lower_Seq (C,n))) = {((Gauge (C,n)) * (i,j))} holds
LSeg (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * (i,k))) meets Lower_Arc C
proof end;

theorem Th59: :: JORDAN1J:59
for n being Element of NAT
for C being Simple_closed_curve
for i, j, k being Element of NAT st 1 < i & i < len (Gauge (C,n)) & 1 <= j & j <= k & k <= width (Gauge (C,n)) & (LSeg (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * (i,k)))) /\ (L~ (Upper_Seq (C,n))) = {((Gauge (C,n)) * (i,k))} & (LSeg (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * (i,k)))) /\ (L~ (Lower_Seq (C,n))) = {((Gauge (C,n)) * (i,j))} holds
LSeg (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * (i,k))) meets Upper_Arc C
proof end;

theorem Th60: :: JORDAN1J:60
for n being Element of NAT
for C being Simple_closed_curve
for i, j, k being Element of NAT st 1 < i & i < len (Gauge (C,n)) & 1 <= j & j <= k & k <= width (Gauge (C,n)) & n > 0 & (LSeg (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * (i,k)))) /\ (Upper_Arc (L~ (Cage (C,n)))) = {((Gauge (C,n)) * (i,k))} & (LSeg (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * (i,k)))) /\ (Lower_Arc (L~ (Cage (C,n)))) = {((Gauge (C,n)) * (i,j))} holds
LSeg (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * (i,k))) meets Lower_Arc C
proof end;

theorem Th61: :: JORDAN1J:61
for n being Element of NAT
for C being Simple_closed_curve
for i, j, k being Element of NAT st 1 < i & i < len (Gauge (C,n)) & 1 <= j & j <= k & k <= width (Gauge (C,n)) & n > 0 & (LSeg (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * (i,k)))) /\ (Upper_Arc (L~ (Cage (C,n)))) = {((Gauge (C,n)) * (i,k))} & (LSeg (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * (i,k)))) /\ (Lower_Arc (L~ (Cage (C,n)))) = {((Gauge (C,n)) * (i,j))} holds
LSeg (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * (i,k))) meets Upper_Arc C
proof end;

theorem :: JORDAN1J:62
for n being Element of NAT
for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2)
for j being Element of NAT st (Gauge (C,(n + 1))) * ((Center (Gauge (C,(n + 1)))),j) in Upper_Arc (L~ (Cage (C,(n + 1)))) & 1 <= j & j <= width (Gauge (C,(n + 1))) holds
LSeg (((Gauge (C,1)) * ((Center (Gauge (C,1))),1)),((Gauge (C,(n + 1))) * ((Center (Gauge (C,(n + 1)))),j))) meets Lower_Arc (L~ (Cage (C,(n + 1))))
proof end;

theorem :: JORDAN1J:63
for n being Element of NAT
for C being Simple_closed_curve
for j, k being Element of NAT st 1 <= j & j <= k & k <= width (Gauge (C,(n + 1))) & (LSeg (((Gauge (C,(n + 1))) * ((Center (Gauge (C,(n + 1)))),j)),((Gauge (C,(n + 1))) * ((Center (Gauge (C,(n + 1)))),k)))) /\ (Upper_Arc (L~ (Cage (C,(n + 1))))) = {((Gauge (C,(n + 1))) * ((Center (Gauge (C,(n + 1)))),k))} & (LSeg (((Gauge (C,(n + 1))) * ((Center (Gauge (C,(n + 1)))),j)),((Gauge (C,(n + 1))) * ((Center (Gauge (C,(n + 1)))),k)))) /\ (Lower_Arc (L~ (Cage (C,(n + 1))))) = {((Gauge (C,(n + 1))) * ((Center (Gauge (C,(n + 1)))),j))} holds
LSeg (((Gauge (C,(n + 1))) * ((Center (Gauge (C,(n + 1)))),j)),((Gauge (C,(n + 1))) * ((Center (Gauge (C,(n + 1)))),k))) meets Lower_Arc C
proof end;

theorem :: JORDAN1J:64
for n being Element of NAT
for C being Simple_closed_curve
for j, k being Element of NAT st 1 <= j & j <= k & k <= width (Gauge (C,(n + 1))) & (LSeg (((Gauge (C,(n + 1))) * ((Center (Gauge (C,(n + 1)))),j)),((Gauge (C,(n + 1))) * ((Center (Gauge (C,(n + 1)))),k)))) /\ (Upper_Arc (L~ (Cage (C,(n + 1))))) = {((Gauge (C,(n + 1))) * ((Center (Gauge (C,(n + 1)))),k))} & (LSeg (((Gauge (C,(n + 1))) * ((Center (Gauge (C,(n + 1)))),j)),((Gauge (C,(n + 1))) * ((Center (Gauge (C,(n + 1)))),k)))) /\ (Lower_Arc (L~ (Cage (C,(n + 1))))) = {((Gauge (C,(n + 1))) * ((Center (Gauge (C,(n + 1)))),j))} holds
LSeg (((Gauge (C,(n + 1))) * ((Center (Gauge (C,(n + 1)))),j)),((Gauge (C,(n + 1))) * ((Center (Gauge (C,(n + 1)))),k))) meets Upper_Arc C
proof end;

:: Moved from JORDAN, AG 20.01.2006
theorem :: JORDAN1J:65
for X, Y being non empty compact Subset of (TOP-REAL 2) st X c= Y & ( W-min Y in X or W-max Y in X ) holds
W-bound X = W-bound Y
proof end;

theorem :: JORDAN1J:66
for X, Y being non empty compact Subset of (TOP-REAL 2) st X c= Y & ( E-min Y in X or E-max Y in X ) holds
E-bound X = E-bound Y
proof end;

theorem :: JORDAN1J:67
for X, Y being non empty compact Subset of (TOP-REAL 2) st X c= Y & ( N-min Y in X or N-max Y in X ) holds
N-bound X = N-bound Y
proof end;

theorem :: JORDAN1J:68
for X, Y being non empty compact Subset of (TOP-REAL 2) st X c= Y & ( S-min Y in X or S-max Y in X ) holds
S-bound X = S-bound Y
proof end;