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

begin

theorem :: JORDAN1E:1

canceled;

theorem :: JORDAN1E:2

canceled;

theorem :: JORDAN1E:3

canceled;

theorem :: JORDAN1E:4

canceled;

theorem Th5: :: JORDAN1E:5

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

proof end;

theorem Th6: :: JORDAN1E:6

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

proof end;

theorem :: JORDAN1E:7

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 <> {}

proof end;

theorem :: JORDAN1E:8

for f being FinSequence of (TOP-REAL 2)
for p being Point of (TOP-REAL 2) st p in L~ f & len (R_Cut f,p) >= 2 holds
f . 1 in L~ (R_Cut f,p)

proof end;

theorem Th9: :: JORDAN1E:9

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))

proof end;

theorem Th10: :: JORDAN1E:10

for i, j, m, n being Element of NAT st i + j = m + n & i <= m & j <= n holds
i = m

proof end;

theorem :: JORDAN1E:11

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 & f . 1 in L~ (L_Cut f,p) holds
f . 1 = p

proof end;

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 Th12: :: JORDAN1E:12

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))))

proof end;

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 Th13: :: JORDAN1E:13

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

proof end;

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

proof end;

cluster Lower_Seq C,n -> non empty ;
coherence
not Lower_Seq C,n is empty

proof end;

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 & Upper_Seq C,n is special & Upper_Seq C,n is unfolded & Upper_Seq C,n is s.n.c. )

proof end;

cluster Lower_Seq C,n -> one-to-one special unfolded s.n.c. ;
coherence
( Lower_Seq C,n is one-to-one & Lower_Seq C,n is special & Lower_Seq C,n is unfolded & Lower_Seq C,n is s.n.c. )

proof end;

end;

theorem Th14: :: JORDAN1E:14

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

proof end;

theorem Th15: :: JORDAN1E:15

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)

proof 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~ (Cage C,n) = L~ ((Upper_Seq C,n) ^' (Lower_Seq C,n))

proof end;

theorem :: JORDAN1E:17

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))

proof end;

theorem Th18: :: JORDAN1E:18

for P being Simple_closed_curve holds W-min P <> E-min P

proof end;

theorem Th19: :: JORDAN1E:19

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 & len (Lower_Seq C,n) >= 3 )

proof 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 -> being_S-Seq ;
coherence
Upper_Seq C,n is being_S-Seq

proof end;

cluster Lower_Seq C,n -> being_S-Seq ;
coherence
Lower_Seq C,n is being_S-Seq

proof end;

end;

theorem :: JORDAN1E:20

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)))}

proof end;

theorem :: JORDAN1E:21

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

proof end;

theorem :: JORDAN1E:22

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

proof end;

theorem :: JORDAN1E:23

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))

proof end;

theorem :: JORDAN1E:24

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 & k + 1 <= len (Cage C,n) & (Cage C,n) /. k = E-max (L~ (Cage C,n)) holds
((Cage C,n) /. (k + 1)) `1 = E-bound (L~ (Cage C,n))

proof end;

theorem :: JORDAN1E:25

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 & k + 1 <= len (Cage C,n) & (Cage C,n) /. k = S-max (L~ (Cage C,n)) holds
((Cage C,n) /. (k + 1)) `2 = S-bound (L~ (Cage C,n))

proof end;

theorem :: JORDAN1E:26

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 & k + 1 <= len (Cage C,n) & (Cage C,n) /. k = W-min (L~ (Cage C,n)) holds
((Cage C,n) /. (k + 1)) `1 = W-bound (L~ (Cage C,n))

proof end;