:: Upper and Lower Sequence on the Cage, Upper and Lower Arcs :: by Robert Milewski :: :: Received April 5, 2002 :: Copyright (c) 2002-2012 Association of Mizar Users begin theorem Th1: :: JORDAN1J:1 for G being Go-board for i1, i2, j1, j2 being Element of NAT st 1 <= j1 & j1 <= width G & 1 <= j2 & j2 <= width G & 1 <= i1 & i1 < i2 & i2 <= len G holds (G * (i1,j1)) `1 < (G * (i2,j2)) `1 proofend; theorem Th2: :: JORDAN1J:2 for G being Go-board for i1, i2, j1, j2 being Element of NAT st 1 <= i1 & i1 <= len G & 1 <= i2 & i2 <= len G & 1 <= j1 & j1 < j2 & j2 <= width G holds (G * (i1,j1)) `2 < (G * (i2,j2)) `2 proofend; registration let f be non empty FinSequence; let g be FinSequence; clusterf ^' g -> non empty ; coherence not f ^' g is empty proofend; end; theorem Th3: :: JORDAN1J:3 for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) for n being Element of NAT holds (L~ ((Cage (C,n)) -: (E-max (L~ (Cage (C,n)))))) /\ (L~ ((Cage (C,n)) :- (E-max (L~ (Cage (C,n)))))) = {(N-min (L~ (Cage (C,n)))),(E-max (L~ (Cage (C,n))))} proofend; theorem Th4: :: JORDAN1J:4 for n being Element of NAT for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) holds Upper_Seq (C,n) = (Rotate ((Cage (C,n)),(E-max (L~ (Cage (C,n)))))) :- (W-min (L~ (Cage (C,n)))) proofend; theorem :: JORDAN1J:5 for n being Element of NAT for C being compact non horizontal non vertical Subset of (TOP-REAL 2) holds ( W-min (L~ (Cage (C,n))) in rng (Upper_Seq (C,n)) & W-min (L~ (Cage (C,n))) in L~ (Upper_Seq (C,n)) ) proofend; theorem :: JORDAN1J:6 for n being Element of NAT for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) holds ( W-max (L~ (Cage (C,n))) in rng (Upper_Seq (C,n)) & W-max (L~ (Cage (C,n))) in L~ (Upper_Seq (C,n)) ) proofend; theorem Th7: :: JORDAN1J:7 for n being Element of NAT for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) holds ( N-min (L~ (Cage (C,n))) in rng (Upper_Seq (C,n)) & N-min (L~ (Cage (C,n))) in L~ (Upper_Seq (C,n)) ) proofend; theorem :: JORDAN1J:8 for n being Element of NAT for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) holds ( N-max (L~ (Cage (C,n))) in rng (Upper_Seq (C,n)) & N-max (L~ (Cage (C,n))) in L~ (Upper_Seq (C,n)) ) proofend; theorem :: JORDAN1J:9 for n being Element of NAT for C being compact non horizontal non vertical Subset of (TOP-REAL 2) holds ( E-max (L~ (Cage (C,n))) in rng (Upper_Seq (C,n)) & E-max (L~ (Cage (C,n))) in L~ (Upper_Seq (C,n)) ) proofend; theorem :: JORDAN1J:10 for n being Element of NAT for C being compact non horizontal non vertical Subset of (TOP-REAL 2) holds ( E-max (L~ (Cage (C,n))) in rng (Lower_Seq (C,n)) & E-max (L~ (Cage (C,n))) in L~ (Lower_Seq (C,n)) ) proofend; theorem :: JORDAN1J:11 for n being Element of NAT for C being compact non horizontal non vertical Subset of (TOP-REAL 2) holds ( E-min (L~ (Cage (C,n))) in rng (Lower_Seq (C,n)) & E-min (L~ (Cage (C,n))) in L~ (Lower_Seq (C,n)) ) proofend; theorem Th12: :: JORDAN1J:12 for n being Element of NAT for C being compact non horizontal non vertical Subset of (TOP-REAL 2) holds ( S-max (L~ (Cage (C,n))) in rng (Lower_Seq (C,n)) & S-max (L~ (Cage (C,n))) in L~ (Lower_Seq (C,n)) ) proofend; theorem :: JORDAN1J:13 for n being Element of NAT for C being compact non horizontal non vertical Subset of (TOP-REAL 2) holds ( S-min (L~ (Cage (C,n))) in rng (Lower_Seq (C,n)) & S-min (L~ (Cage (C,n))) in L~ (Lower_Seq (C,n)) ) proofend; theorem :: JORDAN1J:14 for n being Element of NAT for C being compact non horizontal non vertical Subset of (TOP-REAL 2) holds ( W-min (L~ (Cage (C,n))) in rng (Lower_Seq (C,n)) & W-min (L~ (Cage (C,n))) in L~ (Lower_Seq (C,n)) ) proofend; theorem Th15: :: JORDAN1J:15 for X, Y being non empty compact Subset of (TOP-REAL 2) st X c= Y & N-min Y in X holds N-min X = N-min Y proofend; theorem Th16: :: JORDAN1J:16 for X, Y being non empty compact Subset of (TOP-REAL 2) st X c= Y & N-max Y in X holds N-max X = N-max Y proofend; theorem Th17: :: JORDAN1J:17 for X, Y being non empty compact Subset of (TOP-REAL 2) st X c= Y & E-min Y in X holds E-min X = E-min Y proofend; theorem Th18: :: JORDAN1J:18 for X, Y being non empty compact Subset of (TOP-REAL 2) st X c= Y & E-max Y in X holds E-max X = E-max Y proofend; theorem Th19: :: JORDAN1J:19 for X, Y being non empty compact Subset of (TOP-REAL 2) st X c= Y & S-min Y in X holds S-min X = S-min Y proofend; theorem Th20: :: JORDAN1J:20 for X, Y being non empty compact Subset of (TOP-REAL 2) st X c= Y & S-max Y in X holds S-max X = S-max Y proofend; theorem Th21: :: JORDAN1J:21 for X, Y being non empty compact Subset of (TOP-REAL 2) st X c= Y & W-min Y in X holds W-min X = W-min Y proofend; theorem Th22: :: JORDAN1J:22 for X, Y being non empty compact Subset of (TOP-REAL 2) st X c= Y & W-max Y in X holds W-max X = W-max Y proofend; theorem Th23: :: JORDAN1J:23 for X, Y being non empty compact Subset of (TOP-REAL 2) st N-bound X <= N-bound Y holds N-bound (X \/ Y) = N-bound Y proofend; theorem Th24: :: JORDAN1J:24 for X, Y being non empty compact Subset of (TOP-REAL 2) st E-bound X <= E-bound Y holds E-bound (X \/ Y) = E-bound Y proofend; theorem Th25: :: JORDAN1J:25 for X, Y being non empty compact Subset of (TOP-REAL 2) st S-bound X <= S-bound Y holds S-bound (X \/ Y) = S-bound X proofend; theorem Th26: :: JORDAN1J:26 for X, Y being non empty compact Subset of (TOP-REAL 2) st W-bound X <= W-bound Y holds W-bound (X \/ Y) = W-bound X proofend; theorem :: JORDAN1J:27 for X, Y being non empty compact Subset of (TOP-REAL 2) st N-bound X < N-bound Y holds N-min (X \/ Y) = N-min Y proofend; theorem :: JORDAN1J:28 for X, Y being non empty compact Subset of (TOP-REAL 2) st N-bound X < N-bound Y holds N-max (X \/ Y) = N-max Y proofend; theorem :: JORDAN1J:29 for X, Y being non empty compact Subset of (TOP-REAL 2) st E-bound X < E-bound Y holds E-min (X \/ Y) = E-min Y proofend; theorem :: JORDAN1J:30 for X, Y being non empty compact Subset of (TOP-REAL 2) st E-bound X < E-bound Y holds E-max (X \/ Y) = E-max Y proofend; theorem :: JORDAN1J:31 for X, Y being non empty compact Subset of (TOP-REAL 2) st S-bound X < S-bound Y holds S-min (X \/ Y) = S-min X proofend; theorem :: JORDAN1J:32 for X, Y being non empty compact Subset of (TOP-REAL 2) st S-bound X < S-bound Y holds S-max (X \/ Y) = S-max X proofend; theorem Th33: :: JORDAN1J:33 for X, Y being non empty compact Subset of (TOP-REAL 2) st W-bound X < W-bound Y holds W-min (X \/ Y) = W-min X proofend; theorem :: JORDAN1J:34 for X, Y being non empty compact Subset of (TOP-REAL 2) st W-bound X < W-bound Y holds W-max (X \/ Y) = W-max X proofend; theorem Th35: :: JORDAN1J:35 for f being FinSequence of (TOP-REAL 2) for p being Point of (TOP-REAL 2) st f is being_S-Seq & p in L~ f holds (L_Cut (f,p)) /. (len (L_Cut (f,p))) = f /. (len f) proofend; theorem Th36: :: JORDAN1J:36 for f being non constant standard special_circular_sequence for p, q being Point of (TOP-REAL 2) for g being connected Subset of (TOP-REAL 2) st p in RightComp f & q in LeftComp f & p in g & q in g holds g meets L~ f proofend; registration cluster non empty non trivial V13() V16( NAT ) V17( the U1 of (TOP-REAL 2)) Function-like one-to-one non constant V26() FinSequence-like FinSubsequence-like special unfolded s.n.c. being_S-Seq s.c.c. standard for FinSequence of the U1 of (TOP-REAL 2); existence ex b1 being being_S-Seq FinSequence of (TOP-REAL 2) st ( not b1 is constant & b1 is standard & b1 is s.c.c. ) proofend; end; theorem Th37: :: JORDAN1J:37 for f being S-Sequence_in_R2 for p being Point of (TOP-REAL 2) st p in rng f holds L_Cut (f,p) = mid (f,(p .. f),(len f)) proofend; theorem Th38: :: JORDAN1J:38 for M being Go-board for f being S-Sequence_in_R2 st f is_sequence_on M holds for p being Point of (TOP-REAL 2) st p in rng f holds R_Cut (f,p) is_sequence_on M proofend; theorem Th39: :: JORDAN1J:39 for M being Go-board for f being S-Sequence_in_R2 st f is_sequence_on M holds for p being Point of (TOP-REAL 2) st p in rng f holds L_Cut (f,p) is_sequence_on M proofend; theorem Th40: :: JORDAN1J:40 for G being Go-board for f being FinSequence of (TOP-REAL 2) st f is_sequence_on G holds for i, j being Element of NAT st 1 <= i & i <= len G & 1 <= j & j <= width G & G * (i,j) in L~ f holds G * (i,j) in rng f proofend; theorem :: JORDAN1J:41 for f being S-Sequence_in_R2 for g being FinSequence of (TOP-REAL 2) st g is unfolded & g is s.n.c. & g is one-to-one & (L~ f) /\ (L~ g) = {(f /. 1)} & f /. 1 = g /. (len g) & ( for i being Element of NAT st 1 <= i & i + 2 <= len f holds (LSeg (f,i)) /\ (LSeg ((f /. (len f)),(g /. 1))) = {} ) & ( for i being Element of NAT st 2 <= i & i + 1 <= len g holds (LSeg (g,i)) /\ (LSeg ((f /. (len f)),(g /. 1))) = {} ) holds f ^ g is s.c.c. proofend; theorem :: JORDAN1J:42 for n being Element of NAT for C being non empty compact non horizontal non vertical Subset of (TOP-REAL 2) ex i being Element of NAT st ( 1 <= i & i + 1 <= len (Gauge (C,n)) & W-min C in cell ((Gauge (C,n)),1,i) & W-min C <> (Gauge (C,n)) * (2,i) ) proofend; theorem Th43: :: JORDAN1J:43 for f being S-Sequence_in_R2 for p being Point of (TOP-REAL 2) st p in L~ f & f . (len f) in L~ (R_Cut (f,p)) holds f . (len f) = p proofend; theorem Th44: :: JORDAN1J:44 for f being FinSequence of (TOP-REAL 2) for p being Point of (TOP-REAL 2) holds R_Cut (f,p) <> {} proofend; theorem Th45: :: JORDAN1J:45 for f being FinSequence of (TOP-REAL 2) for p being Point of (TOP-REAL 2) st p in L~ f holds (R_Cut (f,p)) /. (len (R_Cut (f,p))) = p proofend; theorem Th46: :: JORDAN1J:46 for n being Element of NAT for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) for p being Point of (TOP-REAL 2) st p in L~ (Upper_Seq (C,n)) & p `1 = E-bound (L~ (Cage (C,n))) holds p = E-max (L~ (Cage (C,n))) proofend; theorem :: JORDAN1J:47 for n being Element of NAT for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) for p being Point of (TOP-REAL 2) st p in L~ (Lower_Seq (C,n)) & p `1 = W-bound (L~ (Cage (C,n))) holds p = W-min (L~ (Cage (C,n))) proofend; theorem :: JORDAN1J:48 for G being Go-board for f, g being FinSequence of (TOP-REAL 2) for k being Element of NAT st 1 <= k & k < len f & f ^ g is_sequence_on G holds ( left_cell ((f ^ g),k,G) = left_cell (f,k,G) & right_cell ((f ^ g),k,G) = right_cell (f,k,G) ) proofend; theorem Th49: :: JORDAN1J:49 for D being set for f, g being FinSequence of D for i being Element of NAT st i <= len f holds (f ^' g) | i = f | i proofend; theorem Th50: :: JORDAN1J:50 for D being set for f, g being FinSequence of D holds (f ^' g) | (len f) = f proofend; theorem Th51: :: JORDAN1J:51 for G being Go-board for f, g being FinSequence of (TOP-REAL 2) for k being Element of NAT st 1 <= k & k < len f & f ^' g is_sequence_on G holds ( left_cell ((f ^' g),k,G) = left_cell (f,k,G) & right_cell ((f ^' g),k,G) = right_cell (f,k,G) ) proofend; theorem Th52: :: JORDAN1J:52 for G being Go-board for f being S-Sequence_in_R2 for p being Point of (TOP-REAL 2) for k being Element of NAT st 1 <= k & k < p .. f & f is_sequence_on G & p in rng f holds ( left_cell ((R_Cut (f,p)),k,G) = left_cell (f,k,G) & right_cell ((R_Cut (f,p)),k,G) = right_cell (f,k,G) ) proofend; theorem Th53: :: JORDAN1J:53 for G being Go-board for f being FinSequence of (TOP-REAL 2) for p being Point of (TOP-REAL 2) for k being Element of NAT st 1 <= k & k < p .. f & f is_sequence_on G holds ( left_cell ((f -: p),k,G) = left_cell (f,k,G) & right_cell ((f -: p),k,G) = right_cell (f,k,G) ) proofend; theorem Th54: :: JORDAN1J:54 for f, g being FinSequence of (TOP-REAL 2) st f is unfolded & f is s.n.c. & f is one-to-one & g is unfolded & g is s.n.c. & g is one-to-one & f /. (len f) = g /. 1 & (L~ f) /\ (L~ g) = {(g /. 1)} holds f ^' g is s.n.c. proofend; theorem Th55: :: JORDAN1J:55 for f, g being FinSequence of (TOP-REAL 2) st f is one-to-one & g is one-to-one & (rng f) /\ (rng g) c= {(g /. 1)} holds f ^' g is one-to-one proofend; theorem Th56: :: JORDAN1J:56 for f being FinSequence of (TOP-REAL 2) for p being Point of (TOP-REAL 2) st f is being_S-Seq & p in rng f & p <> f . 1 holds (Index (p,f)) + 1 = p .. f proofend; theorem Th57: :: JORDAN1J:57 for n being Element of NAT for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) for i, j, k being Element of NAT st 1 < i & i < len (Gauge (C,n)) & 1 <= j & k <= width (Gauge (C,n)) & (Gauge (C,n)) * (i,k) in L~ (Upper_Seq (C,n)) & (Gauge (C,n)) * (i,j) in L~ (Lower_Seq (C,n)) holds j <> k proofend; theorem Th58: :: JORDAN1J:58 for n being Element of NAT for C being Simple_closed_curve for i, j, k being Element of NAT st 1 < i & i < len (Gauge (C,n)) & 1 <= j & j <= k & k <= width (Gauge (C,n)) & (LSeg (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * (i,k)))) /\ (L~ (Upper_Seq (C,n))) = {((Gauge (C,n)) * (i,k))} & (LSeg (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * (i,k)))) /\ (L~ (Lower_Seq (C,n))) = {((Gauge (C,n)) * (i,j))} holds LSeg (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * (i,k))) meets Lower_Arc C proofend; theorem Th59: :: JORDAN1J:59 for n being Element of NAT for C being Simple_closed_curve for i, j, k being Element of NAT st 1 < i & i < len (Gauge (C,n)) & 1 <= j & j <= k & k <= width (Gauge (C,n)) & (LSeg (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * (i,k)))) /\ (L~ (Upper_Seq (C,n))) = {((Gauge (C,n)) * (i,k))} & (LSeg (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * (i,k)))) /\ (L~ (Lower_Seq (C,n))) = {((Gauge (C,n)) * (i,j))} holds LSeg (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * (i,k))) meets Upper_Arc C proofend; theorem Th60: :: JORDAN1J:60 for n being Element of NAT for C being Simple_closed_curve for i, j, k being Element of NAT st 1 < i & i < len (Gauge (C,n)) & 1 <= j & j <= k & k <= width (Gauge (C,n)) & n > 0 & (LSeg (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * (i,k)))) /\ (Upper_Arc (L~ (Cage (C,n)))) = {((Gauge (C,n)) * (i,k))} & (LSeg (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * (i,k)))) /\ (Lower_Arc (L~ (Cage (C,n)))) = {((Gauge (C,n)) * (i,j))} holds LSeg (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * (i,k))) meets Lower_Arc C proofend; theorem Th61: :: JORDAN1J:61 for n being Element of NAT for C being Simple_closed_curve for i, j, k being Element of NAT st 1 < i & i < len (Gauge (C,n)) & 1 <= j & j <= k & k <= width (Gauge (C,n)) & n > 0 & (LSeg (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * (i,k)))) /\ (Upper_Arc (L~ (Cage (C,n)))) = {((Gauge (C,n)) * (i,k))} & (LSeg (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * (i,k)))) /\ (Lower_Arc (L~ (Cage (C,n)))) = {((Gauge (C,n)) * (i,j))} holds LSeg (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * (i,k))) meets Upper_Arc C proofend; theorem :: JORDAN1J:62 for n being Element of NAT for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) for j being Element of NAT st (Gauge (C,(n + 1))) * ((Center (Gauge (C,(n + 1)))),j) in Upper_Arc (L~ (Cage (C,(n + 1)))) & 1 <= j & j <= width (Gauge (C,(n + 1))) holds LSeg (((Gauge (C,1)) * ((Center (Gauge (C,1))),1)),((Gauge (C,(n + 1))) * ((Center (Gauge (C,(n + 1)))),j))) meets Lower_Arc (L~ (Cage (C,(n + 1)))) proofend; theorem :: JORDAN1J:63 for n being Element of NAT for C being Simple_closed_curve for j, k being Element of NAT st 1 <= j & j <= k & k <= width (Gauge (C,(n + 1))) & (LSeg (((Gauge (C,(n + 1))) * ((Center (Gauge (C,(n + 1)))),j)),((Gauge (C,(n + 1))) * ((Center (Gauge (C,(n + 1)))),k)))) /\ (Upper_Arc (L~ (Cage (C,(n + 1))))) = {((Gauge (C,(n + 1))) * ((Center (Gauge (C,(n + 1)))),k))} & (LSeg (((Gauge (C,(n + 1))) * ((Center (Gauge (C,(n + 1)))),j)),((Gauge (C,(n + 1))) * ((Center (Gauge (C,(n + 1)))),k)))) /\ (Lower_Arc (L~ (Cage (C,(n + 1))))) = {((Gauge (C,(n + 1))) * ((Center (Gauge (C,(n + 1)))),j))} holds LSeg (((Gauge (C,(n + 1))) * ((Center (Gauge (C,(n + 1)))),j)),((Gauge (C,(n + 1))) * ((Center (Gauge (C,(n + 1)))),k))) meets Lower_Arc C proofend; theorem :: JORDAN1J:64 for n being Element of NAT for C being Simple_closed_curve for j, k being Element of NAT st 1 <= j & j <= k & k <= width (Gauge (C,(n + 1))) & (LSeg (((Gauge (C,(n + 1))) * ((Center (Gauge (C,(n + 1)))),j)),((Gauge (C,(n + 1))) * ((Center (Gauge (C,(n + 1)))),k)))) /\ (Upper_Arc (L~ (Cage (C,(n + 1))))) = {((Gauge (C,(n + 1))) * ((Center (Gauge (C,(n + 1)))),k))} & (LSeg (((Gauge (C,(n + 1))) * ((Center (Gauge (C,(n + 1)))),j)),((Gauge (C,(n + 1))) * ((Center (Gauge (C,(n + 1)))),k)))) /\ (Lower_Arc (L~ (Cage (C,(n + 1))))) = {((Gauge (C,(n + 1))) * ((Center (Gauge (C,(n + 1)))),j))} holds LSeg (((Gauge (C,(n + 1))) * ((Center (Gauge (C,(n + 1)))),j)),((Gauge (C,(n + 1))) * ((Center (Gauge (C,(n + 1)))),k))) meets Upper_Arc C proofend; :: Moved from JORDAN, AG 20.01.2006 theorem :: JORDAN1J:65 for X, Y being non empty compact Subset of (TOP-REAL 2) st X c= Y & ( W-min Y in X or W-max Y in X ) holds W-bound X = W-bound Y proofend; theorem :: JORDAN1J:66 for X, Y being non empty compact Subset of (TOP-REAL 2) st X c= Y & ( E-min Y in X or E-max Y in X ) holds E-bound X = E-bound Y proofend; theorem :: JORDAN1J:67 for X, Y being non empty compact Subset of (TOP-REAL 2) st X c= Y & ( N-min Y in X or N-max Y in X ) holds N-bound X = N-bound Y proofend; theorem :: JORDAN1J:68 for X, Y being non empty compact Subset of (TOP-REAL 2) st X c= Y & ( S-min Y in X or S-max Y in X ) holds S-bound X = S-bound Y proofend;