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

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

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

for p being Point of (TOP-REAL 2) st p in L~ f holds

L_Cut (f,p) <> {}

proof end;

theorem :: JORDAN1E:4

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

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

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

f . 1 = p

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;

(Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) -: (E-max (L~ (Cage (C,n)))) is FinSequence of (TOP-REAL 2) ;

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

(Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) -: (E-max (L~ (Cage (C,n)))) is FinSequence of (TOP-REAL 2) ;

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

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

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;

(Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) :- (E-max (L~ (Cage (C,n)))) is FinSequence of (TOP-REAL 2) ;

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

(Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) :- (E-max (L~ (Cage (C,n)))) is FinSequence of (TOP-REAL 2) ;

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

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

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;

coherence

not Upper_Seq (C,n) is empty

not Lower_Seq (C,n) is empty

end;
let n be Nat;

coherence

not Upper_Seq (C,n) is empty

proof end;

coherence not Lower_Seq (C,n) is empty

proof end;

registration

let C be compact non horizontal non vertical Subset of (TOP-REAL 2);

let n be Element of NAT ;

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

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

end;
let n be Element of NAT ;

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;

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;

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

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

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

for n being Element of NAT holds L~ (Cage (C,n)) = L~ ((Upper_Seq (C,n)) ^' (Lower_Seq (C,n)))

proof end;

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

for n being Element of NAT holds L~ (Cage (C,n)) = (L~ (Upper_Seq (C,n))) \/ (L~ (Lower_Seq (C,n)))

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

( len (Upper_Seq (C,n)) >= 3 & len (Lower_Seq (C,n)) >= 3 )

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 ;

coherence

Upper_Seq (C,n) is being_S-Seq

Lower_Seq (C,n) is being_S-Seq

end;
let n be Element of NAT ;

coherence

Upper_Seq (C,n) is being_S-Seq

proof end;

coherence Lower_Seq (C,n) is being_S-Seq

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~ (Upper_Seq (C,n))) /\ (L~ (Lower_Seq (C,n))) = {(W-min (L~ (Cage (C,n)))),(E-max (L~ (Cage (C,n))))}

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

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

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

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

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

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

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;