:: More on External Approximation of a Continuum
:: by Andrzej Trybulec
::
:: Copyright (c) 2001-2021 Association of Mizar Users

registration
let D be non empty with_non-empty_element set ;
existence
ex b1 being FinSequence of D * st
( not b1 is empty & b1 is non-empty )
proof end;
end;

registration
let F be non-empty Function-yielding Function;
coherence
proof end;
end;

theorem Th1: :: JORDAN1H:1
for p, q being Point of () st p <> q holds
p in Cl ((LSeg (p,q)) \ {p,q})
proof end;

theorem Th2: :: JORDAN1H:2
for p, q being Point of () st p <> q holds
Cl ((LSeg (p,q)) \ {p,q}) = LSeg (p,q)
proof end;

theorem :: JORDAN1H:3
for S being Subset of ()
for p, q being Point of () st p <> q & (LSeg (p,q)) \ {p,q} c= S holds
LSeg (p,q) c= Cl S
proof end;

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

Lm1:
;

Lm2:
proof end;

Lm3:
proof end;

Lm4:
proof end;

theorem Th5: :: JORDAN1H:5
proof end;

registration
coherence
proof end;
end;

theorem Th6: :: JORDAN1H:6
proof end;

theorem Th7: :: JORDAN1H:7
for A being finite Subset of REAL holds SgmX (RealOrd,A) is increasing
proof end;

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

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

theorem Th10: :: JORDAN1H:10
for f being FinSequence of () holds X_axis f = proj1 * f
proof end;

theorem Th11: :: JORDAN1H:11
for f being FinSequence of () holds Y_axis f = proj2 * f
proof end;

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

theorem Th12: :: JORDAN1H:12
for D being non empty set
for M being Matrix of D
for i being Nat st i in Seg () holds
rng (Col (M,i)) c= Values M
proof end;

theorem Th13: :: JORDAN1H:13
for D being non empty set
for M being Matrix of D
for i being Nat st i in dom M holds
rng (Line (M,i)) c= Values M
proof end;

theorem Th14: :: JORDAN1H:14
for G being V3() X_increasing-in-column Matrix of () holds len G <= card (proj1 .: ())
proof end;

theorem Th15: :: JORDAN1H:15
for G being X_equal-in-line Matrix of () holds card (proj1 .: ()) <= len G
proof end;

theorem Th16: :: JORDAN1H:16
for G being V3() X_equal-in-line X_increasing-in-column Matrix of () holds len G = card (proj1 .: ())
proof end;

theorem Th17: :: JORDAN1H:17
for G being V3() Y_increasing-in-line Matrix of () holds width G <= card (proj2 .: ())
proof end;

theorem Th18: :: JORDAN1H:18
for G being V3() Y_equal-in-column Matrix of () holds card (proj2 .: ()) <= width G
proof end;

theorem Th19: :: JORDAN1H:19
for G being V3() Y_equal-in-column Y_increasing-in-line Matrix of () holds width G = card (proj2 .: ())
proof end;

theorem :: JORDAN1H:20
for G being Go-board
for f being FinSequence of () st f is_sequence_on G holds
for k being Nat st 1 <= k & k + 1 <= len f holds
LSeg (f,k) c= left_cell (f,k,G)
proof end;

theorem :: JORDAN1H:21
for k being 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)
proof end;

theorem Th22: :: JORDAN1H:22
for G being Go-board
for f being FinSequence of () st f is_sequence_on G holds
for k being Nat st 1 <= k & k + 1 <= len f holds
LSeg (f,k) c= right_cell (f,k,G)
proof end;

theorem Th23: :: JORDAN1H:23
for k being 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)
proof end;

theorem :: JORDAN1H:24
for P being Subset of ()
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 )
proof end;

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

theorem Th26: :: JORDAN1H:26
for i1, j1, i2, j2 being 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 )
proof end;

theorem Th27: :: JORDAN1H:27
for i1, i2 being Nat
for f being FinSequence of ()
for M being Go-board st f is_sequence_on M holds
mid (f,i1,i2) is_sequence_on M
proof end;

registration
coherence
for b1 being Go-board holds
( not b1 is empty & b1 is non-empty )
proof end;
end;

theorem Th28: :: JORDAN1H:28
for i being Nat
for G being Go-board st 1 <= i & i <= len G holds
(SgmX (RealOrd,(proj1 .: ()))) . i = (G * (i,1)) 1
proof end;

theorem Th29: :: JORDAN1H:29
for j being Nat
for G being Go-board st 1 <= j & j <= width G holds
(SgmX (RealOrd,(proj2 .: ()))) . j = (G * (1,j)) 2
proof end;

theorem Th30: :: JORDAN1H:30
for f being non empty FinSequence of ()
for G being Go-board st f is_sequence_on G & ex i being Nat st
( [1,i] in Indices G & G * (1,i) in rng f ) & ex i being Nat st
( [(len G),i] in Indices G & G * ((len G),i) in rng f ) holds
proj1 .: (rng f) = proj1 .: ()
proof end;

theorem Th31: :: JORDAN1H:31
for f being non empty FinSequence of ()
for G being Go-board st f is_sequence_on G & ex i being Nat st
( [i,1] in Indices G & G * (i,1) in rng f ) & ex i being Nat st
( [i,()] in Indices G & G * (i,()) in rng f ) holds
proj2 .: (rng f) = proj2 .: ()
proof end;

registration
let G be Go-board;
cluster Values G -> non empty ;
coherence
not Values G is empty
proof end;
end;

theorem Th32: :: JORDAN1H:32
for G being Go-board holds G = GoB ((SgmX (RealOrd,(proj1 .: ()))),(SgmX (RealOrd,(proj2 .: ()))))
proof end;

theorem Th33: :: JORDAN1H:33
for f being non empty FinSequence of ()
for G being Go-board st proj1 .: (rng f) = proj1 .: () & proj2 .: (rng f) = proj2 .: () holds
G = GoB f
proof end;

theorem Th34: :: JORDAN1H:34
for f being non empty FinSequence of ()
for G being Go-board st f is_sequence_on G & ex i being Nat st
( [1,i] in Indices G & G * (1,i) in rng f ) & ex i being Nat st
( [i,1] in Indices G & G * (i,1) in rng f ) & ex i being Nat st
( [(len G),i] in Indices G & G * ((len G),i) in rng f ) & ex i being Nat st
( [i,()] in Indices G & G * (i,()) in rng f ) holds
G = GoB f
proof end;

theorem Th35: :: JORDAN1H:35
for m, i, n being Nat st 1 <= i holds
[\(((i - 2) / (2 |^ (n -' m))) + 2)/] is Element of NAT
proof end;

theorem Th36: :: JORDAN1H:36
for m, i, n being Nat
for C being compact non horizontal non vertical Subset of () 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)) )
proof end;

theorem Th37: :: JORDAN1H:37
for m, j, i, n being Nat
for C being compact non horizontal non vertical Subset of () st m <= n & 1 <= i & i + 1 <= len (Gauge (C,n)) & 1 <= j & j + 1 <= width (Gauge (C,n)) holds
ex i1, j1 being 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) )
proof end;

theorem Th38: :: JORDAN1H:38
for m, j, i, n being Nat
for C being compact non horizontal non vertical Subset of () st m <= n & 1 <= i & i + 1 <= len (Gauge (C,n)) & 1 <= j & j + 1 <= width (Gauge (C,n)) holds
ex i1, j1 being 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) )
proof end;

theorem :: JORDAN1H:39
for P being Subset of () st P is bounded holds
not UBD P is bounded
proof end;

theorem Th40: :: JORDAN1H:40
for p being Point of ()
for f being non constant standard special_circular_sequence st Rotate (f,p) is clockwise_oriented holds
f is clockwise_oriented
proof end;

theorem :: JORDAN1H:41
for f being non constant standard special_circular_sequence st LeftComp f = UBD (L~ f) holds
f is clockwise_oriented
proof end;

theorem Th42: :: JORDAN1H:42
for f being non constant standard special_circular_sequence holds (Cl ())  = RightComp f
proof end;

theorem :: JORDAN1H:43
for f being non constant standard special_circular_sequence holds (Cl ()) ` = LeftComp f
proof end;

theorem Th44: :: JORDAN1H:44
for n being Nat
for C being compact non horizontal non vertical Subset of () st C is connected holds
GoB (Cage (C,n)) = Gauge (C,n)
proof end;

theorem :: JORDAN1H:45
for n being Nat
for C being compact non horizontal non vertical Subset of () st C is connected holds
N-min C in right_cell ((Cage (C,n)),1)
proof end;

theorem Th46: :: JORDAN1H:46
for j, i being Nat
for C being compact non horizontal non vertical Subset of () st C is connected & i <= j holds
L~ (Cage (C,j)) c= Cl (RightComp (Cage (C,i)))
proof end;

theorem Th47: :: JORDAN1H:47
for j, i being Nat
for C being compact non horizontal non vertical Subset of () st C is connected & i <= j holds
LeftComp (Cage (C,i)) c= LeftComp (Cage (C,j))
proof end;

theorem :: JORDAN1H:48
for j, i being Nat
for C being compact non horizontal non vertical Subset of () st C is connected & i <= j holds
RightComp (Cage (C,j)) c= RightComp (Cage (C,i))
proof end;

definition
let C be compact non horizontal non vertical Subset of ();
let n be Nat;
func X-SpanStart (C,n) -> Nat equals :: JORDAN1H:def 2
(2 |^ (n -' 1)) + 2;
correctness
coherence
(2 |^ (n -' 1)) + 2 is Nat
;
;
end;

:: deftheorem defines X-SpanStart JORDAN1H:def 2 :
for C being compact non horizontal non vertical Subset of ()
for n being Nat holds X-SpanStart (C,n) = (2 |^ (n -' 1)) + 2;

theorem Th49: :: JORDAN1H:49
for n being Nat
for C being compact non horizontal non vertical Subset of () holds
( 2 < X-SpanStart (C,n) & X-SpanStart (C,n) < len (Gauge (C,n)) )
proof end;

theorem Th50: :: JORDAN1H:50
for n being Nat
for C being compact non horizontal non vertical Subset of () holds
( 1 <= (X-SpanStart (C,n)) -' 1 & (X-SpanStart (C,n)) -' 1 < len (Gauge (C,n)) )
proof end;

definition
let C be compact non horizontal non vertical Subset of ();
let n be Nat;
pred n is_sufficiently_large_for C means :: JORDAN1H:def 3
ex j being Nat st
( j < width (Gauge (C,n)) & cell ((Gauge (C,n)),((X-SpanStart (C,n)) -' 1),j) c= BDD C );
end;

:: deftheorem defines is_sufficiently_large_for JORDAN1H:def 3 :
for C being compact non horizontal non vertical Subset of ()
for n being Nat holds
( n is_sufficiently_large_for C iff ex j being 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 Nat
for C being compact non horizontal non vertical Subset of () st n is_sufficiently_large_for C holds
n >= 1
proof end;

theorem :: JORDAN1H:52
for C being non empty compact non horizontal non vertical Subset of ()
for n being Nat
for f being FinSequence of () st f is_sequence_on Gauge (C,n) & len f > 1 holds
for i1, j1 being 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))
proof end;

theorem :: JORDAN1H:53
for C being non empty compact non horizontal non vertical Subset of ()
for n being Nat
for f being FinSequence of () st f is_sequence_on Gauge (C,n) & len f > 1 holds
for i1, j1 being 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))
proof end;

theorem :: JORDAN1H:54
for C being non empty compact non horizontal non vertical Subset of ()
for n being Nat
for f being FinSequence of () st f is_sequence_on Gauge (C,n) & len f > 1 holds
for j1, i2 being 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))
proof end;

theorem :: JORDAN1H:55
for C being non empty compact non horizontal non vertical Subset of ()
for n being Nat
for f being FinSequence of () st f is_sequence_on Gauge (C,n) & len f > 1 holds
for i1, j2 being 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))
proof end;

theorem :: JORDAN1H:56
for C being non empty compact non horizontal non vertical Subset of ()
for n being Nat
for f being FinSequence of () st f is_sequence_on Gauge (C,n) & len f > 1 holds
for i1, j1 being 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))
proof end;

theorem :: JORDAN1H:57
for C being non empty compact non horizontal non vertical Subset of ()
for n being Nat
for f being FinSequence of () st f is_sequence_on Gauge (C,n) & len f > 1 holds
for i1, j1 being 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))
proof end;

theorem :: JORDAN1H:58
for C being non empty compact non horizontal non vertical Subset of ()
for n being Nat
for f being FinSequence of () st f is_sequence_on Gauge (C,n) & len f > 1 holds
for j1, i2 being 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))
proof end;

theorem :: JORDAN1H:59
for C being non empty compact non horizontal non vertical Subset of ()
for n being Nat
for f being FinSequence of () st f is_sequence_on Gauge (C,n) & len f > 1 holds
for i1, j2 being 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))
proof end;

theorem :: JORDAN1H:60
for C being non empty compact non horizontal non vertical Subset of ()
for n being Nat
for f being FinSequence of () st f is_sequence_on Gauge (C,n) & len f > 1 holds
for i1, j1 being 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))
proof end;

theorem :: JORDAN1H:61
for C being non empty compact non horizontal non vertical Subset of ()
for n being Nat
for f being FinSequence of () st f is_sequence_on Gauge (C,n) & len f > 1 holds
for i1, j1 being 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))
proof end;

theorem :: JORDAN1H:62
for C being non empty compact non horizontal non vertical Subset of ()
for n being Nat
for f being FinSequence of () st f is_sequence_on Gauge (C,n) & len f > 1 holds
for j1, i2 being 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))
proof end;

theorem :: JORDAN1H:63
for C being non empty compact non horizontal non vertical Subset of ()
for n being Nat
for f being FinSequence of () st f is_sequence_on Gauge (C,n) & len f > 1 holds
for i1, j2 being 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))
proof end;