:: Upper and Lower Sequence of a Cage
:: by Robert Milewski
::
:: Received August 8, 2001
:: Copyright (c) 2001-2012 Association of Mizar Users


begin

theorem Th1: :: JORDAN1E:1
for f, g being FinSequence of (TOP-REAL 2) st f is_in_the_area_of g holds
for p being Element of (TOP-REAL 2) st p in rng f holds
f -: p is_in_the_area_of g
proofend;

theorem Th2: :: JORDAN1E:2
for f, g being FinSequence of (TOP-REAL 2) st f is_in_the_area_of g holds
for p being Element of (TOP-REAL 2) st p in rng f holds
f :- p is_in_the_area_of g
proofend;

theorem :: JORDAN1E:3
for f being FinSequence of (TOP-REAL 2)
for p being Point of (TOP-REAL 2) st p in L~ f holds
L_Cut (f,p) <> {}
proofend;

theorem :: JORDAN1E:4
for f being FinSequence of (TOP-REAL 2)
for p being Point of (TOP-REAL 2) st p in L~ f &amp; len (R_Cut (f,p)) >= 2 holds
f . 1 in L~ (R_Cut (f,p))
proofend;

theorem Th5: :: JORDAN1E:5
for f being FinSequence of (TOP-REAL 2) st f is being_S-Seq holds
for p being Point of (TOP-REAL 2) st p in L~ f holds
not f . 1 in L~ (mid (f,((Index (p,f)) + 1),(len f)))
proofend;

theorem Th6: :: JORDAN1E:6
for i, j, m, n being Element of NAT st i + j = m + n &amp; i <= m &amp; j <= n holds
i = m
proofend;

theorem :: JORDAN1E:7
for f being FinSequence of (TOP-REAL 2) st f is being_S-Seq holds
for p being Point of (TOP-REAL 2) st p in L~ f &amp; f . 1 in L~ (L_Cut (f,p)) holds
f . 1 = p
proofend;

begin

definition
let C be compact non horizontal non vertical Subset of (TOP-REAL 2);
let n be Nat;
func Upper_Seq (C,n) ->  FinSequence of (TOP-REAL 2) equals :: JORDAN1E:def 1
(Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) -: (E-max (L~ (Cage (C,n))));
coherence
 (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) -: (E-max (L~ (Cage (C,n)))) is FinSequence of (TOP-REAL 2) ;
end;

:: deftheorem  defines Upper_Seq JORDAN1E:def_1_:_
 for C being compact non horizontal non vertical Subset of (TOP-REAL 2)
for n being Nat holds Upper_Seq (C,n) = (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) -: (E-max (L~ (Cage (C,n))));

theorem Th8: :: JORDAN1E:8
for C being compact non horizontal non vertical Subset of (TOP-REAL 2)
for n being Nat holds len (Upper_Seq (C,n)) = (E-max (L~ (Cage (C,n)))) .. (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n))))))
proofend;

definition
let C be compact non horizontal non vertical Subset of (TOP-REAL 2);
let n be Nat;
func Lower_Seq (C,n) ->  FinSequence of (TOP-REAL 2) equals :: JORDAN1E:def 2
(Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) :- (E-max (L~ (Cage (C,n))));
coherence
 (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) :- (E-max (L~ (Cage (C,n)))) is FinSequence of (TOP-REAL 2) ;
end;

:: deftheorem  defines Lower_Seq JORDAN1E:def_2_:_
 for C being compact non horizontal non vertical Subset of (TOP-REAL 2)
for n being Nat holds Lower_Seq (C,n) = (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) :- (E-max (L~ (Cage (C,n))));

theorem Th9: :: JORDAN1E:9
for C being compact non horizontal non vertical Subset of (TOP-REAL 2)
for n being Nat holds len (Lower_Seq (C,n)) = ((len (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n))))))) - ((E-max (L~ (Cage (C,n)))) .. (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))))) + 1
proofend;

registration
let C be compact non horizontal non vertical Subset of (TOP-REAL 2);
let n be Nat;
cluster Upper_Seq (C,n) ->  non empty ;
coherence
 not Upper_Seq (C,n) is empty
proofend;
cluster Lower_Seq (C,n) ->  non empty ;
coherence
 not Lower_Seq (C,n) is empty
proofend;
end;

registration
let C be compact non horizontal non vertical Subset of (TOP-REAL 2);
let n be Element of NAT ;
cluster Upper_Seq (C,n) ->  one-to-one special unfolded s.n.c. ;
coherence
 ( Upper_Seq (C,n) is one-to-one &amp; Upper_Seq (C,n) is special &amp; Upper_Seq (C,n) is unfolded &amp; Upper_Seq (C,n) is s.n.c. )
proofend;
cluster Lower_Seq (C,n) ->  one-to-one special unfolded s.n.c. ;
coherence
 ( Lower_Seq (C,n) is one-to-one &amp; Lower_Seq (C,n) is special &amp; Lower_Seq (C,n) is unfolded &amp; Lower_Seq (C,n) is s.n.c. )
proofend;
end;

theorem Th10: :: JORDAN1E:10
for C being compact non horizontal non vertical Subset of (TOP-REAL 2)
for n being Element of NAT holds (len (Upper_Seq (C,n))) + (len (Lower_Seq (C,n))) = (len (Cage (C,n))) + 1
proofend;

theorem Th11: :: JORDAN1E:11
for C being compact non horizontal non vertical Subset of (TOP-REAL 2)
for n being Element of NAT holds Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n))))) = (Upper_Seq (C,n)) ^' (Lower_Seq (C,n))
proofend;

theorem :: JORDAN1E:12
for C being compact non horizontal non vertical Subset of (TOP-REAL 2)
for n being Element of NAT holds L~ (Cage (C,n)) = L~ ((Upper_Seq (C,n)) ^' (Lower_Seq (C,n)))
proofend;

theorem :: JORDAN1E:13
for C being non empty compact non horizontal non vertical Subset of (TOP-REAL 2)
for n being Element of NAT holds L~ (Cage (C,n)) = (L~ (Upper_Seq (C,n))) \/ (L~ (Lower_Seq (C,n)))
proofend;

theorem Th14: :: JORDAN1E:14
for P being Simple_closed_curve holds W-min P <> E-min P
proofend;

theorem Th15: :: JORDAN1E:15
for C being compact non horizontal non vertical Subset of (TOP-REAL 2)
for n being Element of NAT holds
( len (Upper_Seq (C,n)) >= 3 &amp; len (Lower_Seq (C,n)) >= 3 )
proofend;

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

theorem :: JORDAN1E:16
for C being compact non horizontal non vertical Subset of (TOP-REAL 2)
for n being Element of NAT holds (L~ (Upper_Seq (C,n))) /\ (L~ (Lower_Seq (C,n))) = {(W-min (L~ (Cage (C,n)))),(E-max (L~ (Cage (C,n))))}
proofend;

theorem :: JORDAN1E:17
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_in_the_area_of Cage (C,n)
proofend;

theorem :: JORDAN1E:18
for n being Element of NAT
for C being compact non horizontal non vertical Subset of (TOP-REAL 2) holds Lower_Seq (C,n) is_in_the_area_of Cage (C,n)
proofend;

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

theorem :: JORDAN1E:20
for n being Element of NAT
for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2)
for k being Element of NAT st 1 <= k &amp; k + 1 <= len (Cage (C,n)) &amp; (Cage (C,n)) /. k = E-max (L~ (Cage (C,n))) holds
((Cage (C,n)) /. (k + 1)) `1 = E-bound (L~ (Cage (C,n)))
proofend;

theorem :: JORDAN1E:21
for n being Element of NAT
for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2)
for k being Element of NAT st 1 <= k &amp; k + 1 <= len (Cage (C,n)) &amp; (Cage (C,n)) /. k = S-max (L~ (Cage (C,n))) holds
((Cage (C,n)) /. (k + 1)) `2 = S-bound (L~ (Cage (C,n)))
proofend;

theorem :: JORDAN1E:22
for n being Element of NAT
for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2)
for k being Element of NAT st 1 <= k &amp; k + 1 <= len (Cage (C,n)) &amp; (Cage (C,n)) /. k = W-min (L~ (Cage (C,n))) holds
((Cage (C,n)) /. (k + 1)) `1 = W-bound (L~ (Cage (C,n)))
proofend;