JORDAN1E: Upper and Lower Sequence of a Cage

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

environ

vocabularies HIDDEN, NUMBERS, SUBSET_1, FINSEQ_1, EUCLID, SPRECT_2, RELAT_1, FINSEQ_5, FINSEQ_4, XXREAL_0, PARTFUN1, CARD_1, ARYTM_3, ARYTM_1, PRE_TOPC, TOPREAL1, JORDAN3, XBOOLE_0, FUNCT_1, GROUP_2, ORDINAL4, NAT_1, RLTOPSP1, TARSKI, RCOMP_1, SPPOL_1, FINSEQ_6, JORDAN9, PSCOMP_1, GRAPH_2, TOPREAL2, RELAT_2, MCART_1, GOBOARD1, JORDAN8, TREES_1, MATRIX_1, JORDAN1E;
notations HIDDEN, TARSKI, XBOOLE_0, ENUMSET1, SUBSET_1, CARD_1, ORDINAL1, NUMBERS, XCMPLX_0, XXREAL_0, NAT_1, NAT_D, FUNCT_1, PARTFUN1, FINSEQ_1, FINSEQ_4, FINSEQ_5, MATRIX_0, MATRIX_1, FINSEQ_6, STRUCT_0, GRAPH_2, PRE_TOPC, TOPREAL2, CONNSP_1, COMPTS_1, RLTOPSP1, EUCLID, PSCOMP_1, SPRECT_2, GOBOARD1, TOPREAL1, SPPOL_1, JORDAN3, JORDAN8, JORDAN9;
definitions TARSKI, TOPREAL1, SPRECT_2, XBOOLE_0;
theorems JORDAN8, PSCOMP_1, JORDAN1A, NAT_1, GOBOARD5, FINSEQ_1, FINSEQ_2, SPRECT_2, FINSEQ_4, FINSEQ_5, FINSEQ_6, GOBOARD7, SPPOL_2, REVROT_1, TOPREAL1, SPRECT_3, JORDAN5B, JORDAN3, JORDAN9, GOBOARD1, TARSKI, FINSEQ_3, FUNCT_1, TOPREAL5, JORDAN10, GRAPH_2, CARD_1, CARD_2, ENUMSET1, JORDAN1B, SPRECT_5, XBOOLE_0, XREAL_1, XXREAL_0, EUCLID, PARTFUN1, XREAL_0, MATRIX_0;
schemes ;
registrations RELSET_1, XXREAL_0, XREAL_0, FINSEQ_1, FINSEQ_6, STRUCT_0, TOPREAL2, SPPOL_2, SPRECT_2, REVROT_1, TOPREAL6, JORDAN8, JORDAN1A, CARD_1, FUNCT_1, EUCLID, NAT_1, ORDINAL1;
constructors HIDDEN, FINSEQ_4, NEWTON, FINSEQ_5, CONNSP_1, REALSET2, TOPREAL2, PSCOMP_1, GRAPH_2, JORDAN3, JORDAN8, GOBRD13, JORDAN9, NAT_D, RELSET_1, REAL_1, MATRIX_1;
requirements HIDDEN, NUMERALS, BOOLE, SUBSET, REAL, ARITHM;
equalities XBOOLE_0, PSCOMP_1, CARD_1, ORDINAL1;
expansions TARSKI, TOPREAL1, SPRECT_2, XBOOLE_0;

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

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

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

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

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

proof end;

theorem Th6: :: JORDAN1E:6

for i, j, m, n being Nat st i + j = m + n & i <= m & j <= n holds
i = m

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

proof end;

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

end;

:: deftheorem defines Upper_Seq JORDAN1E:def 1 :

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

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

end;

:: deftheorem defines Lower_Seq JORDAN1E:def 2 :

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

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 ;

proof end;

cluster Lower_Seq (C,n) -> non empty ;

proof end;

end;

registration

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

cluster Upper_Seq (C,n) -> one-to-one special unfolded s.n.c. ;

proof end;

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

proof end;

end;

theorem Th10: :: JORDAN1E:10

for C being compact non horizontal non vertical Subset of (TOP-REAL 2)
for n being 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 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 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 Nat holds L~ (Cage (C,n)) = (L~ (Upper_Seq (C,n))) \/ (L~ (Lower_Seq (C,n)))

proof end;

theorem Th14: :: JORDAN1E:14

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

proof end;

theorem Th15: :: JORDAN1E:15

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

cluster Upper_Seq (C,n) -> being_S-Seq ;

proof end;

cluster Lower_Seq (C,n) -> being_S-Seq ;

proof end;

end;

theorem :: JORDAN1E:16

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

for n being 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:19

for n being 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:20

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