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

registration

cluster V1() V4( NAT ) trivial Function-like V28() FinSequence-like FinSubsequence-like for set ;

existence
ex b₁ being FinSequence st b₁ 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 (TOP-REAL 2) 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 (TOP-REAL 2) 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 (TOP-REAL 2);
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 (TOP-REAL 2)
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 (TOP-REAL 2)
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 (TOP-REAL 2) 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 (TOP-REAL 2) 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 (TOP-REAL 2) 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 (TOP-REAL 2) 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 (TOP-REAL 2) 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 (TOP-REAL 2) 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 (TOP-REAL 2) 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 (TOP-REAL 2) 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 (TOP-REAL 2)
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 (TOP-REAL 2) 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 (TOP-REAL 2) 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 (TOP-REAL 2) 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 (TOP-REAL 2) 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 (TOP-REAL 2) 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 (TOP-REAL 2) 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 (TOP-REAL 2) 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 (TOP-REAL 2) 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 (TOP-REAL 2) 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 (TOP-REAL 2) 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 (TOP-REAL 2) 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 (TOP-REAL 2) 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 (TOP-REAL 2) 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 (TOP-REAL 2) 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 (TOP-REAL 2) 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 (TOP-REAL 2) holds (W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n)))) = (W-bound C) + (E-bound C)

proof end;

theorem :: JORDAN1G:34

for n being 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)

proof end;

theorem Th35: :: JORDAN1G:35

for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2)
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 = ((W-bound C) + (E-bound C)) / 2

proof end;

theorem :: JORDAN1G:36

for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2)
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 = ((S-bound C) + (N-bound C)) / 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 (TOP-REAL 2)
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 (TOP-REAL 2) 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 (TOP-REAL 2) 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 (TOP-REAL 2)
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 (TOP-REAL 2)
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 (TOP-REAL 2)
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 (TOP-REAL 2)
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 (TOP-REAL 2)
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 (TOP-REAL 2)
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 (TOP-REAL 2)
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 (TOP-REAL 2) 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 (TOP-REAL 2) 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 (TOP-REAL 2)
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 (TOP-REAL 2)
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 (TOP-REAL 2)
for n being 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

proof end;

theorem Th54: :: JORDAN1G:54

for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2)
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 (TOP-REAL 2)
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 (TOP-REAL 2)
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 (TOP-REAL 2)
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;