:: Upper and Lower Sequence on the Cage. Part II
:: by Robert Milewski
::
:: Copyright (c) 2001-2017 Association of Mizar Users

registration
existence
ex b1 being FinSequence st b1 is trivial
proof end;
end;

theorem Th1: :: JORDAN1G:1
for f being trivial FinSequence holds
( f is empty or ex x being object st f = <*x*> )
proof end;

registration
let p be non trivial FinSequence;
cluster Rev p -> non trivial ;
coherence
not Rev p is trivial
proof end;
end;

theorem Th2: :: JORDAN1G:2
for D being non empty set
for f being FinSequence of D
for G being Matrix of D
for p being set st f is_sequence_on G holds
f -: p is_sequence_on G
proof end;

theorem Th3: :: JORDAN1G:3
for D being non empty set
for f being FinSequence of D
for G being Matrix of D
for p being Element of D st p in rng f & f is_sequence_on G holds
f :- p is_sequence_on G
proof end;

theorem Th4: :: JORDAN1G:4
for n being Nat
for C being connected compact non horizontal non vertical Subset of () holds Upper_Seq (C,n) is_sequence_on Gauge (C,n)
proof end;

theorem Th5: :: JORDAN1G:5
for n being Nat
for C being connected compact non horizontal non vertical Subset of () holds Lower_Seq (C,n) is_sequence_on Gauge (C,n)
proof end;

registration
let C be connected compact non horizontal non vertical Subset of ();
let n be Nat;
cluster Upper_Seq (C,n) -> standard ;
coherence
Upper_Seq (C,n) is standard
proof end;
cluster Lower_Seq (C,n) -> standard ;
coherence
Lower_Seq (C,n) is standard
proof end;
end;

theorem Th6: :: JORDAN1G:6
for G being Y_equal-in-column Y_increasing-in-line Matrix of ()
for i1, i2, j1, j2 being Nat st [i1,j1] in Indices G & [i2,j2] in Indices G & (G * (i1,j1)) `2 = (G * (i2,j2)) `2 holds
j1 = j2
proof end;

theorem Th7: :: JORDAN1G:7
for G being X_equal-in-line X_increasing-in-column Matrix of ()
for i1, i2, j1, j2 being Nat st [i1,j1] in Indices G & [i2,j2] in Indices G & (G * (i1,j1)) `1 = (G * (i2,j2)) `1 holds
i1 = i2
proof end;

theorem Th8: :: JORDAN1G:8
for f being non trivial special unfolded standard FinSequence of () st ( ( f /. 1 <> N-min (L~ f) & f /. (len f) <> N-min (L~ f) ) or ( f /. 1 <> N-max (L~ f) & f /. (len f) <> N-max (L~ f) ) ) holds
(N-min (L~ f)) `1 < (N-max (L~ f)) `1
proof end;

theorem :: JORDAN1G:9
for f being non trivial special unfolded standard FinSequence of () st ( ( f /. 1 <> N-min (L~ f) & f /. (len f) <> N-min (L~ f) ) or ( f /. 1 <> N-max (L~ f) & f /. (len f) <> N-max (L~ f) ) ) holds
N-min (L~ f) <> N-max (L~ f)
proof end;

theorem Th10: :: JORDAN1G:10
for f being non trivial special unfolded standard FinSequence of () st ( ( f /. 1 <> S-min (L~ f) & f /. (len f) <> S-min (L~ f) ) or ( f /. 1 <> S-max (L~ f) & f /. (len f) <> S-max (L~ f) ) ) holds
(S-min (L~ f)) `1 < (S-max (L~ f)) `1
proof end;

theorem :: JORDAN1G:11
for f being non trivial special unfolded standard FinSequence of () st ( ( f /. 1 <> S-min (L~ f) & f /. (len f) <> S-min (L~ f) ) or ( f /. 1 <> S-max (L~ f) & f /. (len f) <> S-max (L~ f) ) ) holds
S-min (L~ f) <> S-max (L~ f)
proof end;

theorem Th12: :: JORDAN1G:12
for f being non trivial special unfolded standard FinSequence of () st ( ( f /. 1 <> W-min (L~ f) & f /. (len f) <> W-min (L~ f) ) or ( f /. 1 <> W-max (L~ f) & f /. (len f) <> W-max (L~ f) ) ) holds
(W-min (L~ f)) `2 < (W-max (L~ f)) `2
proof end;

theorem :: JORDAN1G:13
for f being non trivial special unfolded standard FinSequence of () st ( ( f /. 1 <> W-min (L~ f) & f /. (len f) <> W-min (L~ f) ) or ( f /. 1 <> W-max (L~ f) & f /. (len f) <> W-max (L~ f) ) ) holds
W-min (L~ f) <> W-max (L~ f)
proof end;

theorem Th14: :: JORDAN1G:14
for f being non trivial special unfolded standard FinSequence of () st ( ( f /. 1 <> E-min (L~ f) & f /. (len f) <> E-min (L~ f) ) or ( f /. 1 <> E-max (L~ f) & f /. (len f) <> E-max (L~ f) ) ) holds
(E-min (L~ f)) `2 < (E-max (L~ f)) `2
proof end;

theorem :: JORDAN1G:15
for f being non trivial special unfolded standard FinSequence of () st ( ( f /. 1 <> E-min (L~ f) & f /. (len f) <> E-min (L~ f) ) or ( f /. 1 <> E-max (L~ f) & f /. (len f) <> E-max (L~ f) ) ) holds
E-min (L~ f) <> E-max (L~ f)
proof end;

theorem Th16: :: JORDAN1G:16
for D being non empty set
for f being FinSequence of D
for p, q being Element of D st p in rng f & q in rng f & q .. f <= p .. f holds
(f -: p) :- q = (f :- q) -: p
proof end;

theorem Th17: :: JORDAN1G:17
for C being connected compact non horizontal non vertical Subset of ()
for n being Nat holds (L~ ((Cage (C,n)) -: (W-min (L~ (Cage (C,n)))))) /\ (L~ ((Cage (C,n)) :- (W-min (L~ (Cage (C,n)))))) = {(N-min (L~ (Cage (C,n)))),(W-min (L~ (Cage (C,n))))}
proof end;

theorem Th18: :: JORDAN1G:18
for n being Nat
for C being connected compact non horizontal non vertical Subset of () holds Lower_Seq (C,n) = (Rotate ((Cage (C,n)),(E-max (L~ (Cage (C,n)))))) -: (W-min (L~ (Cage (C,n))))
proof end;

theorem Th19: :: JORDAN1G:19
for n being Nat
for C being compact non horizontal non vertical Subset of () holds (W-min (L~ (Cage (C,n)))) .. (Upper_Seq (C,n)) = 1
proof end;

theorem Th20: :: JORDAN1G:20
for n being Nat
for C being compact non horizontal non vertical Subset of () holds (W-min (L~ (Cage (C,n)))) .. (Upper_Seq (C,n)) < (W-max (L~ (Cage (C,n)))) .. (Upper_Seq (C,n))
proof end;

theorem Th21: :: JORDAN1G:21
for n being Nat
for C being compact non horizontal non vertical Subset of () holds (W-max (L~ (Cage (C,n)))) .. (Upper_Seq (C,n)) <= (N-min (L~ (Cage (C,n)))) .. (Upper_Seq (C,n))
proof end;

theorem Th22: :: JORDAN1G:22
for n being Nat
for C being compact non horizontal non vertical Subset of () holds (N-min (L~ (Cage (C,n)))) .. (Upper_Seq (C,n)) < (N-max (L~ (Cage (C,n)))) .. (Upper_Seq (C,n))
proof end;

theorem Th23: :: JORDAN1G:23
for n being Nat
for C being compact non horizontal non vertical Subset of () holds (N-max (L~ (Cage (C,n)))) .. (Upper_Seq (C,n)) <= (E-max (L~ (Cage (C,n)))) .. (Upper_Seq (C,n))
proof end;

theorem Th24: :: JORDAN1G:24
for n being Nat
for C being compact non horizontal non vertical Subset of () holds (E-max (L~ (Cage (C,n)))) .. (Upper_Seq (C,n)) = len (Upper_Seq (C,n))
proof end;

theorem Th25: :: JORDAN1G:25
for n being Nat
for C being compact non horizontal non vertical Subset of () holds (E-max (L~ (Cage (C,n)))) .. (Lower_Seq (C,n)) = 1
proof end;

theorem Th26: :: JORDAN1G:26
for n being Nat
for C being connected compact non horizontal non vertical Subset of () holds (E-max (L~ (Cage (C,n)))) .. (Lower_Seq (C,n)) < (E-min (L~ (Cage (C,n)))) .. (Lower_Seq (C,n))
proof end;

theorem Th27: :: JORDAN1G:27
for n being Nat
for C being connected compact non horizontal non vertical Subset of () holds (E-min (L~ (Cage (C,n)))) .. (Lower_Seq (C,n)) <= (S-max (L~ (Cage (C,n)))) .. (Lower_Seq (C,n))
proof end;

theorem Th28: :: JORDAN1G:28
for n being Nat
for C being connected compact non horizontal non vertical Subset of () holds (S-max (L~ (Cage (C,n)))) .. (Lower_Seq (C,n)) < (S-min (L~ (Cage (C,n)))) .. (Lower_Seq (C,n))
proof end;

theorem Th29: :: JORDAN1G:29
for n being Nat
for C being connected compact non horizontal non vertical Subset of () holds (S-min (L~ (Cage (C,n)))) .. (Lower_Seq (C,n)) <= (W-min (L~ (Cage (C,n)))) .. (Lower_Seq (C,n))
proof end;

theorem Th30: :: JORDAN1G:30
for n being Nat
for C being connected compact non horizontal non vertical Subset of () holds (W-min (L~ (Cage (C,n)))) .. (Lower_Seq (C,n)) = len (Lower_Seq (C,n))
proof end;

theorem Th31: :: JORDAN1G:31
for n being Nat
for C being connected compact non horizontal non vertical Subset of () holds ((Upper_Seq (C,n)) /. 2) `1 = W-bound (L~ (Cage (C,n)))
proof end;

theorem :: JORDAN1G:32
for n being Nat
for C being connected compact non horizontal non vertical Subset of () holds ((Lower_Seq (C,n)) /. 2) `1 = E-bound (L~ (Cage (C,n)))
proof end;

theorem Th33: :: JORDAN1G:33
for n being Nat
for C being connected compact non horizontal non vertical Subset of () holds (W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n)))) = () + ()
proof end;

theorem :: JORDAN1G:34
for n being Nat
for C being connected compact non horizontal non vertical Subset of () holds (S-bound (L~ (Cage (C,n)))) + (N-bound (L~ (Cage (C,n)))) = () + ()
proof end;

theorem Th35: :: JORDAN1G:35
for C being connected compact non horizontal non vertical Subset of ()
for n, i being Nat st 1 <= i & i <= width (Gauge (C,n)) & n > 0 holds
((Gauge (C,n)) * ((Center (Gauge (C,n))),i)) `1 = (() + ()) / 2
proof end;

theorem :: JORDAN1G:36
for C being connected compact non horizontal non vertical Subset of ()
for n, i being Nat st 1 <= i & i <= len (Gauge (C,n)) & n > 0 holds
((Gauge (C,n)) * (i,(Center (Gauge (C,n))))) `2 = (() + ()) / 2
proof end;

theorem Th37: :: JORDAN1G:37
for f being S-Sequence_in_R2
for k1, k2 being Nat st 1 <= k1 & k1 <= len f & 1 <= k2 & k2 <= len f & f /. 1 in L~ (mid (f,k1,k2)) & not k1 = 1 holds
k2 = 1
proof end;

theorem Th38: :: JORDAN1G:38
for f being S-Sequence_in_R2
for k1, k2 being Nat st 1 <= k1 & k1 <= len f & 1 <= k2 & k2 <= len f & f /. (len f) in L~ (mid (f,k1,k2)) & not k1 = len f holds
k2 = len f
proof end;

theorem Th39: :: JORDAN1G:39
for C being compact non horizontal non vertical Subset of ()
for n being Nat holds
( rng (Upper_Seq (C,n)) c= rng (Cage (C,n)) & rng (Lower_Seq (C,n)) c= rng (Cage (C,n)) )
proof end;

theorem Th40: :: JORDAN1G:40
for n being Nat
for C being compact non horizontal non vertical Subset of () holds Upper_Seq (C,n) is_a_h.c._for Cage (C,n)
proof end;

theorem Th41: :: JORDAN1G:41
for n being Nat
for C being compact non horizontal non vertical Subset of () holds Rev (Lower_Seq (C,n)) is_a_h.c._for Cage (C,n)
proof end;

theorem Th42: :: JORDAN1G:42
for n being Nat
for C being connected compact non horizontal non vertical Subset of ()
for i being Nat st 1 < i & i <= len (Gauge (C,n)) holds
not (Gauge (C,n)) * (i,1) in rng (Upper_Seq (C,n))
proof end;

theorem Th43: :: JORDAN1G:43
for n being Nat
for C being connected compact non horizontal non vertical Subset of ()
for i being Nat st 1 <= i & i < len (Gauge (C,n)) holds
not (Gauge (C,n)) * (i,(width (Gauge (C,n)))) in rng (Lower_Seq (C,n))
proof end;

theorem Th44: :: JORDAN1G:44
for n being Nat
for C being connected compact non horizontal non vertical Subset of ()
for i being Nat st 1 < i & i <= len (Gauge (C,n)) holds
not (Gauge (C,n)) * (i,1) in L~ (Upper_Seq (C,n))
proof end;

theorem :: JORDAN1G:45
for n being Nat
for C being connected compact non horizontal non vertical Subset of ()
for i being Nat st 1 <= i & i < len (Gauge (C,n)) holds
not (Gauge (C,n)) * (i,(width (Gauge (C,n)))) in L~ (Lower_Seq (C,n))
proof end;

theorem Th46: :: JORDAN1G:46
for n being Nat
for C being connected compact non horizontal non vertical Subset of ()
for i, j being Nat st 1 <= i & i <= len (Gauge (C,n)) & 1 <= j & j <= width (Gauge (C,n)) & (Gauge (C,n)) * (i,j) in L~ (Cage (C,n)) holds
LSeg (((Gauge (C,n)) * (i,1)),((Gauge (C,n)) * (i,j))) meets L~ (Lower_Seq (C,n))
proof end;

theorem Th47: :: JORDAN1G:47
for C being connected compact non horizontal non vertical Subset of ()
for n being Nat st n > 0 holds
First_Point ((L~ (Upper_Seq (C,n))),(W-min (L~ (Cage (C,n)))),(E-max (L~ (Cage (C,n)))),(Vertical_Line (((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2))) in rng (Upper_Seq (C,n))
proof end;

theorem Th48: :: JORDAN1G:48
for C being connected compact non horizontal non vertical Subset of ()
for n being Nat st n > 0 holds
Last_Point ((L~ (Lower_Seq (C,n))),(E-max (L~ (Cage (C,n)))),(W-min (L~ (Cage (C,n)))),(Vertical_Line (((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2))) in rng (Lower_Seq (C,n))
proof end;

theorem Th49: :: JORDAN1G:49
for f being S-Sequence_in_R2
for p being Point of () st p in rng f holds
R_Cut (f,p) = mid (f,1,(p .. f))
proof end;

theorem Th50: :: JORDAN1G:50
for f being S-Sequence_in_R2
for Q being closed Subset of () st L~ f meets Q & not f /. 1 in Q & First_Point ((L~ f),(f /. 1),(f /. (len f)),Q) in rng f holds
(L~ (mid (f,1,((First_Point ((L~ f),(f /. 1),(f /. (len f)),Q)) .. f)))) /\ Q = {(First_Point ((L~ f),(f /. 1),(f /. (len f)),Q))}
proof end;

theorem Th51: :: JORDAN1G:51
for C being connected compact non horizontal non vertical Subset of ()
for n being Nat st n > 0 holds
for k being Nat st 1 <= k & k < (First_Point ((L~ (Upper_Seq (C,n))),(W-min (L~ (Cage (C,n)))),(E-max (L~ (Cage (C,n)))),(Vertical_Line (((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2)))) .. (Upper_Seq (C,n)) holds
((Upper_Seq (C,n)) /. k) `1 < ((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2
proof end;

theorem Th52: :: JORDAN1G:52
for C being connected compact non horizontal non vertical Subset of ()
for n being Nat st n > 0 holds
for k being Nat st 1 <= k & k < (First_Point ((L~ (Rev (Lower_Seq (C,n)))),(W-min (L~ (Cage (C,n)))),(E-max (L~ (Cage (C,n)))),(Vertical_Line (((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2)))) .. (Rev (Lower_Seq (C,n))) holds
((Rev (Lower_Seq (C,n))) /. k) `1 < ((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2
proof end;

theorem Th53: :: JORDAN1G:53
for C being connected compact non horizontal non vertical Subset of ()
for n being Nat st n > 0 holds
for q being Point of () st q in rng (mid ((Upper_Seq (C,n)),2,((First_Point ((L~ (Upper_Seq (C,n))),(W-min (L~ (Cage (C,n)))),(E-max (L~ (Cage (C,n)))),(Vertical_Line (((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2)))) .. (Upper_Seq (C,n))))) holds
q `1 <= ((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2
proof end;

theorem Th54: :: JORDAN1G:54
for C being connected compact non horizontal non vertical Subset of ()
for n being Nat st n > 0 holds
(First_Point ((L~ (Upper_Seq (C,n))),(W-min (L~ (Cage (C,n)))),(E-max (L~ (Cage (C,n)))),(Vertical_Line (((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2)))) `2 > (Last_Point ((L~ (Lower_Seq (C,n))),(E-max (L~ (Cage (C,n)))),(W-min (L~ (Cage (C,n)))),(Vertical_Line (((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2)))) `2
proof end;

theorem Th55: :: JORDAN1G:55
for C being connected compact non horizontal non vertical Subset of ()
for n being Nat st n > 0 holds
L~ (Upper_Seq (C,n)) = Upper_Arc (L~ (Cage (C,n)))
proof end;

theorem Th56: :: JORDAN1G:56
for C being connected compact non horizontal non vertical Subset of ()
for n being Nat st n > 0 holds
L~ (Lower_Seq (C,n)) = Lower_Arc (L~ (Cage (C,n)))
proof end;

theorem :: JORDAN1G:57
for C being connected compact non horizontal non vertical Subset of ()
for n being Nat st n > 0 holds
for i, j being Nat st 1 <= i & i <= len (Gauge (C,n)) & 1 <= j & j <= width (Gauge (C,n)) & (Gauge (C,n)) * (i,j) in L~ (Cage (C,n)) holds
LSeg (((Gauge (C,n)) * (i,1)),((Gauge (C,n)) * (i,j))) meets Lower_Arc (L~ (Cage (C,n)))
proof end;