:: More on External Approximation of a Continuum
:: by Andrzej Trybulec
::
:: Received October 7, 2001
:: Copyright (c) 2001 Association of Mizar Users
theorem :: JORDAN1H:1
canceled;
theorem :: JORDAN1H:2
canceled;
theorem :: JORDAN1H:3
canceled;
theorem :: JORDAN1H:4
canceled;
theorem :: JORDAN1H:5
canceled;
theorem Th6: :: JORDAN1H:6
theorem Th7: :: JORDAN1H:7
theorem :: JORDAN1H:8
:: deftheorem defines RealOrd JORDAN1H:def 1 :
theorem Th9: :: JORDAN1H:9
Lm1:
RealOrd is_reflexive_in REAL
Lm2:
RealOrd is_antisymmetric_in REAL
Lm3:
RealOrd is_transitive_in REAL
Lm4:
RealOrd is_connected_in REAL
theorem Th10: :: JORDAN1H:10
theorem Th11: :: JORDAN1H:11
theorem Th12: :: JORDAN1H:12
theorem Th13: :: JORDAN1H:13
theorem :: JORDAN1H:14
canceled;
theorem Th15: :: JORDAN1H:15
theorem Th16: :: JORDAN1H:16
theorem Th17: :: JORDAN1H:17
theorem Th18: :: JORDAN1H:18
theorem Th19: :: JORDAN1H:19
theorem Th20: :: JORDAN1H:20
theorem Th21: :: JORDAN1H:21
theorem Th22: :: JORDAN1H:22
theorem Th23: :: JORDAN1H:23
theorem Th24: :: JORDAN1H:24
theorem Th25: :: JORDAN1H:25
theorem :: JORDAN1H:26
theorem :: JORDAN1H:27
theorem Th28: :: JORDAN1H:28
theorem Th29: :: JORDAN1H:29
theorem :: JORDAN1H:30
theorem :: JORDAN1H:31
theorem Th32: :: JORDAN1H:32
theorem Th33: :: JORDAN1H:33
theorem Th34: :: JORDAN1H:34
theorem Th35: :: JORDAN1H:35
theorem Th36: :: JORDAN1H:36
theorem Th37: :: JORDAN1H:37
theorem Th38: :: JORDAN1H:38
theorem Th39: :: JORDAN1H:39
theorem Th40: :: JORDAN1H:40
theorem Th41: :: JORDAN1H:41
theorem Th42: :: JORDAN1H:42
theorem Th43: :: JORDAN1H:43
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 )
theorem Th44: :: JORDAN1H:44
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 )
theorem :: JORDAN1H:45
canceled;
theorem :: JORDAN1H:46
canceled;
theorem :: JORDAN1H:47
theorem Th48: :: JORDAN1H:48
theorem :: JORDAN1H:49
theorem Th50: :: JORDAN1H:50
theorem :: JORDAN1H:51
theorem Th52: :: JORDAN1H:52
theorem :: JORDAN1H:53
theorem Th54: :: JORDAN1H:54
theorem Th55: :: JORDAN1H:55
theorem :: JORDAN1H:56
:: deftheorem defines X-SpanStart JORDAN1H:def 2 :
theorem :: JORDAN1H:57
canceled;
theorem Th58: :: JORDAN1H:58
theorem Th59: :: JORDAN1H:59
:: deftheorem Def3 defines is_sufficiently_large_for JORDAN1H:def 3 :
theorem :: JORDAN1H:60
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
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)
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
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)
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
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)
theorem :: JORDAN1H:64
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)
theorem :: JORDAN1H:65
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)
theorem :: JORDAN1H:66
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)
theorem :: JORDAN1H:67
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)
theorem :: JORDAN1H:68
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)
theorem :: JORDAN1H:69
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)
theorem :: JORDAN1H:70
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)
theorem :: JORDAN1H:71
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)
theorem :: JORDAN1H:72
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)