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

theorem Th1: :: JORDAN1J:1

for G being Go-board
for i1, i2, j1, j2 being 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 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 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 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 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 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 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 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 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 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 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 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 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 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 V22() 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 V1() V4( NAT ) V5( the U1 of (TOP-REAL 2)) non empty non trivial V16() Function-like one-to-one V22() V28() 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 b₁ being being_S-Seq FinSequence of (TOP-REAL 2) st
( b₁ is V22() & b₁ is standard & b₁ 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 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 Nat st 1 <= i & i + 2 <= len f holds
(LSeg (f,i)) /\ (LSeg ((f /. (len f)),(g /. 1))) = {} ) & ( for i being 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 Nat
for C being non empty compact non horizontal non vertical Subset of (TOP-REAL 2) ex i being 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 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 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 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 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 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 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 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 Nat
for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2)
for i, j, k being 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 Nat
for C being Simple_closed_curve
for i, j, k being 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 Nat
for C being Simple_closed_curve
for i, j, k being 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 Nat
for C being Simple_closed_curve
for i, j, k being 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 Nat
for C being Simple_closed_curve
for i, j, k being 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 Nat
for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2)
for j being 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 Nat
for C being Simple_closed_curve
for j, k being 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 Nat
for C being Simple_closed_curve
for j, k being 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;