:: More on External Approximation of a Continuum :: by Andrzej Trybulec :: :: Received October 7, 2001 :: Copyright (c) 2001-2012 Association of Mizar Users begin registration let D be non empty with_non-empty_element set ; cluster non empty Relation-like non-empty NAT -defined D * -valued Function-like finite FinSequence-like FinSubsequence-like Function-yielding V81() FinSequence-yielding finite-support for FinSequence of D * ; existence ex b1 being FinSequence of D * st ( not b1 is empty & b1 is non-empty ) proofend; end; registration let F be non-empty Function-yielding Function; cluster rngs F -> non-empty ; coherence rngs F is non-empty proofend; end; theorem Th1: :: JORDAN1H:1 for p, q being Point of (TOP-REAL 2) st p <> q holds p in Cl ((LSeg (p,q)) \ {p,q}) proofend; theorem Th2: :: JORDAN1H:2 for p, q being Point of (TOP-REAL 2) st p <> q holds Cl ((LSeg (p,q)) \ {p,q}) = LSeg (p,q) proofend; theorem :: JORDAN1H:3 for S being Subset of (TOP-REAL 2) for p, q being Point of (TOP-REAL 2) st p <> q & (LSeg (p,q)) \ {p,q} c= S holds LSeg (p,q) c= Cl S proofend; begin definition func RealOrd -> Relation of REAL equals :: JORDAN1H:def 1 { [r,s] where r, s is Real : r <= s } ; coherence { [r,s] where r, s is Real : r <= s } is Relation of REAL proofend; end; :: deftheorem defines RealOrd JORDAN1H:def_1_:_ RealOrd = { [r,s] where r, s is Real : r <= s } ; theorem Th4: :: JORDAN1H:4 for r, s being Real st [r,s] in RealOrd holds r <= s proofend; Lm1: RealOrd is_reflexive_in REAL proofend; Lm2: RealOrd is_antisymmetric_in REAL proofend; Lm3: RealOrd is_transitive_in REAL proofend; Lm4: RealOrd is_connected_in REAL proofend; theorem Th5: :: JORDAN1H:5 field RealOrd = REAL proofend; registration cluster RealOrd -> total reflexive antisymmetric transitive being_linear-order ; coherence ( RealOrd is total & RealOrd is reflexive & RealOrd is antisymmetric & RealOrd is transitive & RealOrd is being_linear-order ) proofend; end; theorem Th6: :: JORDAN1H:6 RealOrd linearly_orders REAL proofend; theorem Th7: :: JORDAN1H:7 for A being finite Subset of REAL holds SgmX (RealOrd,A) is increasing proofend; theorem Th8: :: JORDAN1H:8 for f being FinSequence of REAL for A being finite Subset of REAL st A = rng f holds SgmX (RealOrd,A) = Incr f proofend; registration let A be finite Subset of REAL; cluster SgmX (RealOrd,A) -> increasing ; coherence SgmX (RealOrd,A) is increasing by Th7; end; theorem Th9: :: JORDAN1H:9 for X being non empty set for A being finite Subset of X for R being being_linear-order Order of X holds len (SgmX (R,A)) = card A proofend; begin theorem Th10: :: JORDAN1H:10 for f being FinSequence of (TOP-REAL 2) holds X_axis f = proj1 * f proofend; theorem Th11: :: JORDAN1H:11 for f being FinSequence of (TOP-REAL 2) holds Y_axis f = proj2 * f proofend; definition let D be non empty set ; let M be FinSequence of D * ; :: original:Values redefine func Values M -> Subset of D; coherence Values M is Subset of D proofend; end; registration let D be non empty with_non-empty_elements set ; let M be non empty non-empty FinSequence of D * ; cluster Values M -> non empty ; coherence not Values M is empty proofend; end; theorem Th12: :: JORDAN1H:12 for D being non empty set for M being Matrix of D for i being Element of NAT st i in Seg (width M) holds rng (Col (M,i)) c= Values M proofend; theorem Th13: :: JORDAN1H:13 for D being non empty set for M being Matrix of D for i being Element of NAT st i in dom M holds rng (Line (M,i)) c= Values M proofend; theorem Th14: :: JORDAN1H:14 for G being V15() X_increasing-in-column Matrix of (TOP-REAL 2) holds len G <= card (proj1 .: (Values G)) proofend; theorem Th15: :: JORDAN1H:15 for G being X_equal-in-line Matrix of (TOP-REAL 2) holds card (proj1 .: (Values G)) <= len G proofend; theorem Th16: :: JORDAN1H:16 for G being V15() X_equal-in-line X_increasing-in-column Matrix of (TOP-REAL 2) holds len G = card (proj1 .: (Values G)) proofend; theorem Th17: :: JORDAN1H:17 for G being V15() Y_increasing-in-line Matrix of (TOP-REAL 2) holds width G <= card (proj2 .: (Values G)) proofend; theorem Th18: :: JORDAN1H:18 for G being V15() Y_equal-in-column Matrix of (TOP-REAL 2) holds card (proj2 .: (Values G)) <= width G proofend; theorem Th19: :: JORDAN1H:19 for G being V15() Y_equal-in-column Y_increasing-in-line Matrix of (TOP-REAL 2) holds width G = card (proj2 .: (Values G)) proofend; begin theorem :: JORDAN1H:20 for G being Go-board for f being FinSequence of (TOP-REAL 2) st f is_sequence_on G holds for k being Element of NAT st 1 <= k & k + 1 <= len f holds LSeg (f,k) c= left_cell (f,k,G) proofend; theorem :: JORDAN1H:21 for k being Element of NAT for f being standard special_circular_sequence st 1 <= k & k + 1 <= len f holds left_cell (f,k,(GoB f)) = left_cell (f,k) proofend; theorem Th22: :: JORDAN1H:22 for G being Go-board for f being FinSequence of (TOP-REAL 2) st f is_sequence_on G holds for k being Element of NAT st 1 <= k & k + 1 <= len f holds LSeg (f,k) c= right_cell (f,k,G) proofend; theorem Th23: :: JORDAN1H:23 for k being Element of NAT for f being standard special_circular_sequence st 1 <= k & k + 1 <= len f holds right_cell (f,k,(GoB f)) = right_cell (f,k) proofend; theorem :: JORDAN1H:24 for P being Subset of (TOP-REAL 2) for f being non constant standard special_circular_sequence holds ( not P is_a_component_of (L~ f) ` or P = RightComp f or P = LeftComp f ) proofend; theorem :: JORDAN1H:25 for G being Go-board for f being non constant standard special_circular_sequence st f is_sequence_on G holds for k being Element of NAT st 1 <= k & k + 1 <= len f holds ( Int (right_cell (f,k,G)) c= RightComp f & Int (left_cell (f,k,G)) c= LeftComp f ) proofend; theorem Th26: :: JORDAN1H:26 for i1, j1, i2, j2 being Element of NAT for G being Go-board st [i1,j1] in Indices G & [i2,j2] in Indices G & G * (i1,j1) = G * (i2,j2) holds ( i1 = i2 & j1 = j2 ) proofend; theorem Th27: :: JORDAN1H:27 for i1, i2 being Element of NAT for f being FinSequence of (TOP-REAL 2) for M being Go-board st f is_sequence_on M holds mid (f,i1,i2) is_sequence_on M proofend; registration cluster non empty-yielding tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column -> non empty non-empty for FinSequence of the carrier of (TOP-REAL 2) * ; coherence for b1 being Go-board holds ( not b1 is empty & b1 is non-empty ) proofend; end; theorem Th28: :: JORDAN1H:28 for i being Element of NAT for G being Go-board st 1 <= i & i <= len G holds (SgmX (RealOrd,(proj1 .: (Values G)))) . i = (G * (i,1)) `1 proofend; theorem Th29: :: JORDAN1H:29 for j being Element of NAT for G being Go-board st 1 <= j & j <= width G holds (SgmX (RealOrd,(proj2 .: (Values G)))) . j = (G * (1,j)) `2 proofend; theorem Th30: :: JORDAN1H:30 for f being non empty FinSequence of (TOP-REAL 2) for G being Go-board st f is_sequence_on G & ex i being Element of NAT st ( [1,i] in Indices G & G * (1,i) in rng f ) & ex i being Element of NAT st ( [(len G),i] in Indices G & G * ((len G),i) in rng f ) holds proj1 .: (rng f) = proj1 .: (Values G) proofend; theorem Th31: :: JORDAN1H:31 for f being non empty FinSequence of (TOP-REAL 2) for G being Go-board st f is_sequence_on G & ex i being Element of NAT st ( [i,1] in Indices G & G * (i,1) in rng f ) & ex i being Element of NAT st ( [i,(width G)] in Indices G & G * (i,(width G)) in rng f ) holds proj2 .: (rng f) = proj2 .: (Values G) proofend; registration let G be Go-board; cluster Values G -> non empty ; coherence not Values G is empty proofend; end; theorem Th32: :: JORDAN1H:32 for G being Go-board holds G = GoB ((SgmX (RealOrd,(proj1 .: (Values G)))),(SgmX (RealOrd,(proj2 .: (Values G))))) proofend; theorem Th33: :: JORDAN1H:33 for f being non empty FinSequence of (TOP-REAL 2) for G being Go-board st proj1 .: (rng f) = proj1 .: (Values G) & proj2 .: (rng f) = proj2 .: (Values G) holds G = GoB f proofend; theorem Th34: :: JORDAN1H:34 for f being non empty FinSequence of (TOP-REAL 2) for G being Go-board st f is_sequence_on G & ex i being Element of NAT st ( [1,i] in Indices G & G * (1,i) in rng f ) & ex i being Element of NAT st ( [i,1] in Indices G & G * (i,1) in rng f ) & ex i being Element of NAT st ( [(len G),i] in Indices G & G * ((len G),i) in rng f ) & ex i being Element of NAT st ( [i,(width G)] in Indices G & G * (i,(width G)) in rng f ) holds G = GoB f proofend; begin theorem Th35: :: JORDAN1H:35 for i, n, m being Element of NAT st 1 <= i holds [\(((i - 2) / (2 |^ (n -' m))) + 2)/] is Element of NAT proofend; theorem Th36: :: JORDAN1H:36 for m, n, i being Element of NAT for C being compact non horizontal non vertical Subset of (TOP-REAL 2) st m <= n & 1 <= i & i + 1 <= len (Gauge (C,n)) holds ( 1 <= [\(((i - 2) / (2 |^ (n -' m))) + 2)/] & [\(((i - 2) / (2 |^ (n -' m))) + 2)/] + 1 <= len (Gauge (C,m)) ) proofend; theorem Th37: :: JORDAN1H:37 for m, n, i, j being Element of NAT for C being compact non horizontal non vertical Subset of (TOP-REAL 2) st m <= n & 1 <= i & i + 1 <= len (Gauge (C,n)) & 1 <= j & j + 1 <= width (Gauge (C,n)) holds ex i1, j1 being Element of NAT st ( i1 = [\(((i - 2) / (2 |^ (n -' m))) + 2)/] & j1 = [\(((j - 2) / (2 |^ (n -' m))) + 2)/] & cell ((Gauge (C,n)),i,j) c= cell ((Gauge (C,m)),i1,j1) ) proofend; theorem Th38: :: JORDAN1H:38 for m, n, i, j being Element of NAT for C being compact non horizontal non vertical Subset of (TOP-REAL 2) st m <= n & 1 <= i & i + 1 <= len (Gauge (C,n)) & 1 <= j & j + 1 <= width (Gauge (C,n)) holds ex i1, j1 being Element of NAT st ( 1 <= i1 & i1 + 1 <= len (Gauge (C,m)) & 1 <= j1 & j1 + 1 <= width (Gauge (C,m)) & cell ((Gauge (C,n)),i,j) c= cell ((Gauge (C,m)),i1,j1) ) proofend; theorem :: JORDAN1H:39 for P being Subset of (TOP-REAL 2) st P is bounded holds not UBD P is bounded proofend; theorem Th40: :: JORDAN1H:40 for p being Point of (TOP-REAL 2) for f being non constant standard special_circular_sequence st Rotate (f,p) is clockwise_oriented holds f is clockwise_oriented proofend; theorem :: JORDAN1H:41 for f being non constant standard special_circular_sequence st LeftComp f = UBD (L~ f) holds f is clockwise_oriented proofend; begin theorem Th42: :: JORDAN1H:42 for f being non constant standard special_circular_sequence holds (Cl (LeftComp f)) ` = RightComp f proofend; theorem :: JORDAN1H:43 for f being non constant standard special_circular_sequence holds (Cl (RightComp f)) ` = LeftComp f proofend; theorem Th44: :: JORDAN1H:44 for n being Element of NAT for C being compact non horizontal non vertical Subset of (TOP-REAL 2) st C is connected holds GoB (Cage (C,n)) = Gauge (C,n) proofend; theorem :: JORDAN1H:45 for n being Element of NAT for C being compact non horizontal non vertical Subset of (TOP-REAL 2) st C is connected holds N-min C in right_cell ((Cage (C,n)),1) proofend; theorem Th46: :: JORDAN1H:46 for i, j being Element of NAT for C being compact non horizontal non vertical Subset of (TOP-REAL 2) st C is connected & i <= j holds L~ (Cage (C,j)) c= Cl (RightComp (Cage (C,i))) proofend; theorem Th47: :: JORDAN1H:47 for i, j being Element of NAT for C being compact non horizontal non vertical Subset of (TOP-REAL 2) st C is connected & i <= j holds LeftComp (Cage (C,i)) c= LeftComp (Cage (C,j)) proofend; theorem :: JORDAN1H:48 for i, j being Element of NAT for C being compact non horizontal non vertical Subset of (TOP-REAL 2) st C is connected & i <= j holds RightComp (Cage (C,j)) c= RightComp (Cage (C,i)) proofend; begin definition let C be compact non horizontal non vertical Subset of (TOP-REAL 2); let n be Element of NAT ; func X-SpanStart (C,n) -> Element of NAT equals :: JORDAN1H:def 2 (2 |^ (n -' 1)) + 2; correctness coherence (2 |^ (n -' 1)) + 2 is Element of NAT ; ; end; :: deftheorem defines X-SpanStart JORDAN1H:def_2_:_ for C being compact non horizontal non vertical Subset of (TOP-REAL 2) for n being Element of NAT holds X-SpanStart (C,n) = (2 |^ (n -' 1)) + 2; theorem Th49: :: JORDAN1H:49 for n being Element of NAT for C being compact non horizontal non vertical Subset of (TOP-REAL 2) holds ( 2 < X-SpanStart (C,n) & X-SpanStart (C,n) < len (Gauge (C,n)) ) proofend; theorem Th50: :: JORDAN1H:50 for n being Element of NAT for C being compact non horizontal non vertical Subset of (TOP-REAL 2) holds ( 1 <= (X-SpanStart (C,n)) -' 1 & (X-SpanStart (C,n)) -' 1 < len (Gauge (C,n)) ) proofend; definition let C be compact non horizontal non vertical Subset of (TOP-REAL 2); let n be Element of NAT ; predn is_sufficiently_large_for C means :Def3: :: JORDAN1H:def 3 ex j being Element of NAT st ( j < width (Gauge (C,n)) & cell ((Gauge (C,n)),((X-SpanStart (C,n)) -' 1),j) c= BDD C ); end; :: deftheorem Def3 defines is_sufficiently_large_for JORDAN1H:def_3_:_ for C being compact non horizontal non vertical Subset of (TOP-REAL 2) for n being Element of NAT holds ( n is_sufficiently_large_for C iff ex j being Element of NAT st ( j < width (Gauge (C,n)) & cell ((Gauge (C,n)),((X-SpanStart (C,n)) -' 1),j) c= BDD C ) ); theorem :: JORDAN1H:51 for n being Element of NAT for C being compact non horizontal non vertical Subset of (TOP-REAL 2) st n is_sufficiently_large_for C holds n >= 1 proofend; theorem :: JORDAN1H:52 for C being non empty compact non horizontal non vertical Subset of (TOP-REAL 2) for n being Element of NAT for f being FinSequence of (TOP-REAL 2) st f is_sequence_on Gauge (C,n) & len f > 1 holds for i1, j1 being Element of NAT st left_cell (f,((len f) -' 1),(Gauge (C,n))) meets C & [i1,j1] in Indices (Gauge (C,n)) & f /. ((len f) -' 1) = (Gauge (C,n)) * (i1,j1) & [i1,(j1 + 1)] in Indices (Gauge (C,n)) & f /. (len f) = (Gauge (C,n)) * (i1,(j1 + 1)) holds [(i1 -' 1),(j1 + 1)] in Indices (Gauge (C,n)) proofend; theorem :: JORDAN1H:53 for C being non empty compact non horizontal non vertical Subset of (TOP-REAL 2) for n being Element of NAT for f being FinSequence of (TOP-REAL 2) st f is_sequence_on Gauge (C,n) & len f > 1 holds for i1, j1 being Element of NAT st left_cell (f,((len f) -' 1),(Gauge (C,n))) meets C & [i1,j1] in Indices (Gauge (C,n)) & f /. ((len f) -' 1) = (Gauge (C,n)) * (i1,j1) & [(i1 + 1),j1] in Indices (Gauge (C,n)) & f /. (len f) = (Gauge (C,n)) * ((i1 + 1),j1) holds [(i1 + 1),(j1 + 1)] in Indices (Gauge (C,n)) proofend; theorem :: JORDAN1H:54 for C being non empty compact non horizontal non vertical Subset of (TOP-REAL 2) for n being Element of NAT for f being FinSequence of (TOP-REAL 2) st f is_sequence_on Gauge (C,n) & len f > 1 holds for j1, i2 being Element of NAT st left_cell (f,((len f) -' 1),(Gauge (C,n))) meets C & [(i2 + 1),j1] in Indices (Gauge (C,n)) & f /. ((len f) -' 1) = (Gauge (C,n)) * ((i2 + 1),j1) & [i2,j1] in Indices (Gauge (C,n)) & f /. (len f) = (Gauge (C,n)) * (i2,j1) holds [i2,(j1 -' 1)] in Indices (Gauge (C,n)) proofend; theorem :: JORDAN1H:55 for C being non empty compact non horizontal non vertical Subset of (TOP-REAL 2) for n being Element of NAT for f being FinSequence of (TOP-REAL 2) st f is_sequence_on Gauge (C,n) & len f > 1 holds for i1, j2 being Element of NAT st left_cell (f,((len f) -' 1),(Gauge (C,n))) meets C & [i1,(j2 + 1)] in Indices (Gauge (C,n)) & f /. ((len f) -' 1) = (Gauge (C,n)) * (i1,(j2 + 1)) & [i1,j2] in Indices (Gauge (C,n)) & f /. (len f) = (Gauge (C,n)) * (i1,j2) holds [(i1 + 1),j2] in Indices (Gauge (C,n)) proofend; theorem :: JORDAN1H:56 for C being non empty compact non horizontal non vertical Subset of (TOP-REAL 2) for n being Element of NAT for f being FinSequence of (TOP-REAL 2) st f is_sequence_on Gauge (C,n) & len f > 1 holds for i1, j1 being Element of NAT st front_left_cell (f,((len f) -' 1),(Gauge (C,n))) meets C & [i1,j1] in Indices (Gauge (C,n)) & f /. ((len f) -' 1) = (Gauge (C,n)) * (i1,j1) & [i1,(j1 + 1)] in Indices (Gauge (C,n)) & f /. (len f) = (Gauge (C,n)) * (i1,(j1 + 1)) holds [i1,(j1 + 2)] in Indices (Gauge (C,n)) proofend; theorem :: JORDAN1H:57 for C being non empty compact non horizontal non vertical Subset of (TOP-REAL 2) for n being Element of NAT for f being FinSequence of (TOP-REAL 2) st f is_sequence_on Gauge (C,n) & len f > 1 holds for i1, j1 being Element of NAT st front_left_cell (f,((len f) -' 1),(Gauge (C,n))) meets C & [i1,j1] in Indices (Gauge (C,n)) & f /. ((len f) -' 1) = (Gauge (C,n)) * (i1,j1) & [(i1 + 1),j1] in Indices (Gauge (C,n)) & f /. (len f) = (Gauge (C,n)) * ((i1 + 1),j1) holds [(i1 + 2),j1] in Indices (Gauge (C,n)) proofend; theorem :: JORDAN1H:58 for C being non empty compact non horizontal non vertical Subset of (TOP-REAL 2) for n being Element of NAT for f being FinSequence of (TOP-REAL 2) st f is_sequence_on Gauge (C,n) & len f > 1 holds for j1, i2 being Element of NAT st front_left_cell (f,((len f) -' 1),(Gauge (C,n))) meets C & [(i2 + 1),j1] in Indices (Gauge (C,n)) & f /. ((len f) -' 1) = (Gauge (C,n)) * ((i2 + 1),j1) & [i2,j1] in Indices (Gauge (C,n)) & f /. (len f) = (Gauge (C,n)) * (i2,j1) holds [(i2 -' 1),j1] in Indices (Gauge (C,n)) proofend; theorem :: JORDAN1H:59 for C being non empty compact non horizontal non vertical Subset of (TOP-REAL 2) for n being Element of NAT for f being FinSequence of (TOP-REAL 2) st f is_sequence_on Gauge (C,n) & len f > 1 holds for i1, j2 being Element of NAT st front_left_cell (f,((len f) -' 1),(Gauge (C,n))) meets C & [i1,(j2 + 1)] in Indices (Gauge (C,n)) & f /. ((len f) -' 1) = (Gauge (C,n)) * (i1,(j2 + 1)) & [i1,j2] in Indices (Gauge (C,n)) & f /. (len f) = (Gauge (C,n)) * (i1,j2) holds [i1,(j2 -' 1)] in Indices (Gauge (C,n)) proofend; theorem :: JORDAN1H:60 for C being non empty compact non horizontal non vertical Subset of (TOP-REAL 2) for n being Element of NAT for f being FinSequence of (TOP-REAL 2) st f is_sequence_on Gauge (C,n) & len f > 1 holds for i1, j1 being Element of NAT st front_right_cell (f,((len f) -' 1),(Gauge (C,n))) meets C & [i1,j1] in Indices (Gauge (C,n)) & f /. ((len f) -' 1) = (Gauge (C,n)) * (i1,j1) & [i1,(j1 + 1)] in Indices (Gauge (C,n)) & f /. (len f) = (Gauge (C,n)) * (i1,(j1 + 1)) holds [(i1 + 1),(j1 + 1)] in Indices (Gauge (C,n)) proofend; theorem :: JORDAN1H:61 for C being non empty compact non horizontal non vertical Subset of (TOP-REAL 2) for n being Element of NAT for f being FinSequence of (TOP-REAL 2) st f is_sequence_on Gauge (C,n) & len f > 1 holds for i1, j1 being Element of NAT st front_right_cell (f,((len f) -' 1),(Gauge (C,n))) meets C & [i1,j1] in Indices (Gauge (C,n)) & f /. ((len f) -' 1) = (Gauge (C,n)) * (i1,j1) & [(i1 + 1),j1] in Indices (Gauge (C,n)) & f /. (len f) = (Gauge (C,n)) * ((i1 + 1),j1) holds [(i1 + 1),(j1 -' 1)] in Indices (Gauge (C,n)) proofend; theorem :: JORDAN1H:62 for C being non empty compact non horizontal non vertical Subset of (TOP-REAL 2) for n being Element of NAT for f being FinSequence of (TOP-REAL 2) st f is_sequence_on Gauge (C,n) & len f > 1 holds for j1, i2 being Element of NAT st front_right_cell (f,((len f) -' 1),(Gauge (C,n))) meets C & [(i2 + 1),j1] in Indices (Gauge (C,n)) & f /. ((len f) -' 1) = (Gauge (C,n)) * ((i2 + 1),j1) & [i2,j1] in Indices (Gauge (C,n)) & f /. (len f) = (Gauge (C,n)) * (i2,j1) holds [i2,(j1 + 1)] in Indices (Gauge (C,n)) proofend; theorem :: JORDAN1H:63 for C being non empty compact non horizontal non vertical Subset of (TOP-REAL 2) for n being Element of NAT for f being FinSequence of (TOP-REAL 2) st f is_sequence_on Gauge (C,n) & len f > 1 holds for i1, j2 being Element of NAT st front_right_cell (f,((len f) -' 1),(Gauge (C,n))) meets C & [i1,(j2 + 1)] in Indices (Gauge (C,n)) & f /. ((len f) -' 1) = (Gauge (C,n)) * (i1,(j2 + 1)) & [i1,j2] in Indices (Gauge (C,n)) & f /. (len f) = (Gauge (C,n)) * (i1,j2) holds [(i1 -' 1),j2] in Indices (Gauge (C,n)) proofend;