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


begin

registration
cluster trivial V13() V16( NAT ) Function-like V26() FinSequence-like FinSubsequence-like for set ;
existence
 ex b1 being FinSequence st b1 is trivial
proofend;
end;

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

registration
let p be non trivial FinSequence;
cluster Rev p ->  non trivial ;
coherence
 not Rev p is trivial
proofend;
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
proofend;

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 &amp; f is_sequence_on G holds
f :- p is_sequence_on G
proofend;

theorem Th4: :: JORDAN1G: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) is_sequence_on Gauge (C,n)
proofend;

theorem Th5: :: JORDAN1G:5
for n being Element of NAT
for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) holds Lower_Seq (C,n) is_sequence_on Gauge (C,n)
proofend;

registration
let C be connected compact non horizontal non vertical Subset of (TOP-REAL 2);
let n be Element of NAT ;
cluster Upper_Seq (C,n) ->  standard ;
coherence
 Upper_Seq (C,n) is standard
proofend;
cluster Lower_Seq (C,n) ->  standard ;
coherence
 Lower_Seq (C,n) is standard
proofend;
end;

theorem Th6: :: JORDAN1G:6
for G being Y_equal-in-column Y_increasing-in-line Matrix of (TOP-REAL 2)
for i1, i2, j1, j2 being Element of NAT st [i1,j1] in Indices G &amp; [i2,j2] in Indices G &amp; (G * (i1,j1)) `2 = (G * (i2,j2)) `2 holds
j1 = j2
proofend;

theorem Th7: :: JORDAN1G:7
for G being X_equal-in-line X_increasing-in-column Matrix of (TOP-REAL 2)
for i1, i2, j1, j2 being Element of NAT st [i1,j1] in Indices G &amp; [i2,j2] in Indices G &amp; (G * (i1,j1)) `1 = (G * (i2,j2)) `1 holds
i1 = i2
proofend;

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

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

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

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

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

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

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

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

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 &amp; q in rng f &amp; q .. f <= p .. f holds
(f -: p) :- q = (f :- q) -: p
proofend;

theorem Th17: :: JORDAN1G:17
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)) -: (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))))}
proofend;

theorem Th18: :: JORDAN1G:18
for n being Element of NAT
for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) holds Lower_Seq (C,n) = (Rotate ((Cage (C,n)),(E-max (L~ (Cage (C,n)))))) -: (W-min (L~ (Cage (C,n))))
proofend;

theorem Th19: :: JORDAN1G:19
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)))) .. (Upper_Seq (C,n)) = 1
proofend;

theorem Th20: :: JORDAN1G:20
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)))) .. (Upper_Seq (C,n)) < (W-max (L~ (Cage (C,n)))) .. (Upper_Seq (C,n))
proofend;

theorem Th21: :: JORDAN1G:21
for n being Element of NAT
for C being compact non horizontal non vertical Subset of (TOP-REAL 2) holds (W-max (L~ (Cage (C,n)))) .. (Upper_Seq (C,n)) <= (N-min (L~ (Cage (C,n)))) .. (Upper_Seq (C,n))
proofend;

theorem Th22: :: JORDAN1G:22
for n being Element of NAT
for C being compact non horizontal non vertical Subset of (TOP-REAL 2) holds (N-min (L~ (Cage (C,n)))) .. (Upper_Seq (C,n)) < (N-max (L~ (Cage (C,n)))) .. (Upper_Seq (C,n))
proofend;

theorem Th23: :: JORDAN1G:23
for n being Element of NAT
for C being compact non horizontal non vertical Subset of (TOP-REAL 2) holds (N-max (L~ (Cage (C,n)))) .. (Upper_Seq (C,n)) <= (E-max (L~ (Cage (C,n)))) .. (Upper_Seq (C,n))
proofend;

theorem Th24: :: JORDAN1G:24
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)))) .. (Upper_Seq (C,n)) = len (Upper_Seq (C,n))
proofend;

theorem Th25: :: JORDAN1G:25
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)))) .. (Lower_Seq (C,n)) = 1
proofend;

theorem Th26: :: JORDAN1G:26
for n being Element of NAT
for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) holds (E-max (L~ (Cage (C,n)))) .. (Lower_Seq (C,n)) < (E-min (L~ (Cage (C,n)))) .. (Lower_Seq (C,n))
proofend;

theorem Th27: :: JORDAN1G:27
for n being Element of NAT
for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) holds (E-min (L~ (Cage (C,n)))) .. (Lower_Seq (C,n)) <= (S-max (L~ (Cage (C,n)))) .. (Lower_Seq (C,n))
proofend;

theorem Th28: :: JORDAN1G:28
for n being Element of NAT
for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) holds (S-max (L~ (Cage (C,n)))) .. (Lower_Seq (C,n)) < (S-min (L~ (Cage (C,n)))) .. (Lower_Seq (C,n))
proofend;

theorem Th29: :: JORDAN1G:29
for n being Element of NAT
for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) holds (S-min (L~ (Cage (C,n)))) .. (Lower_Seq (C,n)) <= (W-min (L~ (Cage (C,n)))) .. (Lower_Seq (C,n))
proofend;

theorem Th30: :: JORDAN1G:30
for n being Element of NAT
for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) holds (W-min (L~ (Cage (C,n)))) .. (Lower_Seq (C,n)) = len (Lower_Seq (C,n))
proofend;

theorem Th31: :: JORDAN1G:31
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)) /. 2) `1 = W-bound (L~ (Cage (C,n)))
proofend;

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

theorem Th33: :: JORDAN1G:33
for n being Element of NAT
for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) holds (W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n)))) = (W-bound C) + (E-bound C)
proofend;

theorem :: JORDAN1G:34
for n being Element of NAT
for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) holds (S-bound (L~ (Cage (C,n)))) + (N-bound (L~ (Cage (C,n)))) = (S-bound C) + (N-bound C)
proofend;

theorem Th35: :: JORDAN1G:35
for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2)
for n being Element of NAT
for i being Nat st 1 <= i &amp; i <= width (Gauge (C,n)) &amp; n > 0 holds
((Gauge (C,n)) * ((Center (Gauge (C,n))),i)) `1 = ((W-bound C) + (E-bound C)) / 2
proofend;

theorem :: JORDAN1G:36
for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2)
for n, i being Element of NAT st 1 <= i &amp; i <= len (Gauge (C,n)) &amp; n > 0 holds
((Gauge (C,n)) * (i,(Center (Gauge (C,n))))) `2 = ((S-bound C) + (N-bound C)) / 2
proofend;

theorem Th37: :: JORDAN1G:37
for f being S-Sequence_in_R2
for k1, k2 being Element of NAT st 1 <= k1 &amp; k1 <= len f &amp; 1 <= k2 &amp; k2 <= len f &amp; f /. 1 in L~ (mid (f,k1,k2)) &amp; not k1 = 1 holds
k2 = 1
proofend;

theorem Th38: :: JORDAN1G:38
for f being S-Sequence_in_R2
for k1, k2 being Element of NAT st 1 <= k1 &amp; k1 <= len f &amp; 1 <= k2 &amp; k2 <= len f &amp; f /. (len f) in L~ (mid (f,k1,k2)) &amp; not k1 = len f holds
k2 = len f
proofend;

theorem Th39: :: JORDAN1G:39
for C being compact non horizontal non vertical Subset of (TOP-REAL 2)
for n being Element of NAT holds
( rng (Upper_Seq (C,n)) c= rng (Cage (C,n)) &amp; rng (Lower_Seq (C,n)) c= rng (Cage (C,n)) )
proofend;

theorem Th40: :: JORDAN1G:40
for n being Element of NAT
for C being compact non horizontal non vertical Subset of (TOP-REAL 2) holds Upper_Seq (C,n) is_a_h.c._for Cage (C,n)
proofend;

theorem Th41: :: JORDAN1G:41
for n being Element of NAT
for C being compact non horizontal non vertical Subset of (TOP-REAL 2) holds Rev (Lower_Seq (C,n)) is_a_h.c._for Cage (C,n)
proofend;

theorem Th42: :: JORDAN1G:42
for n being Element of NAT
for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2)
for i being Element of NAT st 1 < i &amp; i <= len (Gauge (C,n)) holds
not (Gauge (C,n)) * (i,1) in rng (Upper_Seq (C,n))
proofend;

theorem Th43: :: JORDAN1G:43
for n being Element of NAT
for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2)
for i being Element of NAT st 1 <= i &amp; i < len (Gauge (C,n)) holds
not (Gauge (C,n)) * (i,(width (Gauge (C,n)))) in rng (Lower_Seq (C,n))
proofend;

theorem Th44: :: JORDAN1G:44
for n being Element of NAT
for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2)
for i being Element of NAT st 1 < i &amp; i <= len (Gauge (C,n)) holds
not (Gauge (C,n)) * (i,1) in L~ (Upper_Seq (C,n))
proofend;

theorem :: JORDAN1G:45
for n being Element of NAT
for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2)
for i being Element of NAT st 1 <= i &amp; i < len (Gauge (C,n)) holds
not (Gauge (C,n)) * (i,(width (Gauge (C,n)))) in L~ (Lower_Seq (C,n))
proofend;

theorem Th46: :: JORDAN1G:46
for n being Element of NAT
for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2)
for i, j being Element of NAT st 1 <= i &amp; i <= len (Gauge (C,n)) &amp; 1 <= j &amp; j <= width (Gauge (C,n)) &amp; (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))
proofend;

theorem Th47: :: JORDAN1G:47
for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2)
for n being Element of 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))
proofend;

theorem Th48: :: JORDAN1G:48
for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2)
for n being Element of 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))
proofend;

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

theorem Th50: :: JORDAN1G:50
for f being S-Sequence_in_R2
for Q being closed Subset of (TOP-REAL 2) st L~ f meets Q &amp; not f /. 1 in Q &amp; 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))}
proofend;

theorem Th51: :: JORDAN1G:51
for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2)
for n being Element of NAT st n > 0 holds
for k being Element of NAT st 1 <= k &amp; 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
proofend;

theorem Th52: :: JORDAN1G:52
for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2)
for n being Element of NAT st n > 0 holds
for k being Nat st 1 <= k &amp; 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
proofend;

theorem Th53: :: JORDAN1G:53
for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2)
for n being Element of NAT st n > 0 holds
for q being Point of (TOP-REAL 2) 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
proofend;

theorem Th54: :: JORDAN1G:54
for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2)
for n being Element of 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
proofend;

theorem Th55: :: JORDAN1G:55
for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2)
for n being Element of NAT st n > 0 holds
L~ (Upper_Seq (C,n)) = Upper_Arc (L~ (Cage (C,n)))
proofend;

theorem Th56: :: JORDAN1G:56
for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2)
for n being Element of NAT st n > 0 holds
L~ (Lower_Seq (C,n)) = Lower_Arc (L~ (Cage (C,n)))
proofend;

theorem :: JORDAN1G:57
for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2)
for n being Element of NAT st n > 0 holds
for i, j being Element of NAT st 1 <= i &amp; i <= len (Gauge (C,n)) &amp; 1 <= j &amp; j <= width (Gauge (C,n)) &amp; (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)))
proofend;