:: Bounded Domains and Unbounded Domains
:: by Yatsuka Nakamura , Andrzej Trybulec and Czeslaw Bylinski
::
:: Received January 7, 1999
:: Copyright (c) 1999 Association of Mizar Users
theorem Th1: :: JORDAN2C:1
theorem Th2: :: JORDAN2C:2
theorem Th3: :: JORDAN2C:3
for
n,
m being
Element of
NAT st
n <= m &
m <= n + 3 & not
m = n & not
m = n + 1 & not
m = n + 2 holds
m = n + 3
theorem Th4: :: JORDAN2C:4
for
n,
m being
Element of
NAT st
n <= m &
m <= n + 4 & not
m = n & not
m = n + 1 & not
m = n + 2 & not
m = n + 3 holds
m = n + 4
theorem :: JORDAN2C:5
canceled;
theorem :: JORDAN2C:6
canceled;
theorem Th7: :: JORDAN2C:7
theorem Th8: :: JORDAN2C:8
theorem Th9: :: JORDAN2C:9
theorem :: JORDAN2C:10
theorem Th11: :: JORDAN2C:11
theorem Th12: :: JORDAN2C:12
theorem Th13: :: JORDAN2C:13
theorem :: JORDAN2C:14
canceled;
theorem Th15: :: JORDAN2C:15
:: deftheorem JORDAN2C:def 1 :
canceled;
:: deftheorem Def2 defines Bounded JORDAN2C:def 2 :
theorem Th16: :: JORDAN2C:16
:: deftheorem Def3 defines is_inside_component_of JORDAN2C:def 3 :
theorem Th17: :: JORDAN2C:17
:: deftheorem Def4 defines is_outside_component_of JORDAN2C:def 4 :
theorem Th18: :: JORDAN2C:18
theorem :: JORDAN2C:19
theorem :: JORDAN2C:20
:: deftheorem defines BDD JORDAN2C:def 5 :
:: deftheorem defines UBD JORDAN2C:def 6 :
theorem Th21: :: JORDAN2C:21
theorem :: JORDAN2C:22
theorem Th23: :: JORDAN2C:23
theorem Th24: :: JORDAN2C:24
theorem Th25: :: JORDAN2C:25
theorem Th26: :: JORDAN2C:26
theorem Th27: :: JORDAN2C:27
theorem Th28: :: JORDAN2C:28
theorem Th29: :: JORDAN2C:29
theorem Th30: :: JORDAN2C:30
theorem Th31: :: JORDAN2C:31
theorem :: JORDAN2C:32
canceled;
theorem Th33: :: JORDAN2C:33
:: deftheorem defines 1* JORDAN2C:def 7 :
:: deftheorem defines 1.REAL JORDAN2C:def 8 :
theorem :: JORDAN2C:34
theorem Th35: :: JORDAN2C:35
Lm1:
1.REAL 1 = <*1*>
by FINSEQ_2:73;
theorem :: JORDAN2C:36
canceled;
theorem :: JORDAN2C:37
theorem Th38: :: JORDAN2C:38
theorem Th39: :: JORDAN2C:39
theorem Th40: :: JORDAN2C:40
theorem Th41: :: JORDAN2C:41
theorem Th42: :: JORDAN2C:42
theorem Th43: :: JORDAN2C:43
theorem Th44: :: JORDAN2C:44
theorem Th45: :: JORDAN2C:45
theorem Th46: :: JORDAN2C:46
for
n being
Element of
NAT for
P being
Subset of
(TOP-REAL n) for
w1,
w2,
w3,
w4,
w5,
w6,
w7 being
Point of
(TOP-REAL n) st
w1 in P &
w2 in P &
w3 in P &
w4 in P &
w5 in P &
w6 in P &
w7 in P &
LSeg w1,
w2 c= P &
LSeg w2,
w3 c= P &
LSeg w3,
w4 c= P &
LSeg w4,
w5 c= P &
LSeg w5,
w6 c= P &
LSeg w6,
w7 c= P holds
ex
h being
Function of
I[01] ,
((TOP-REAL n) | P) st
(
h is
continuous &
w1 = h . 0 &
w7 = h . 1 )
theorem Th47: :: JORDAN2C:47
theorem Th48: :: JORDAN2C:48
theorem Th49: :: JORDAN2C:49
theorem Th50: :: JORDAN2C:50
theorem :: JORDAN2C:51
canceled;
theorem Th52: :: JORDAN2C:52
theorem Th53: :: JORDAN2C:53
theorem Th54: :: JORDAN2C:54
theorem Th55: :: JORDAN2C:55
theorem Th56: :: JORDAN2C:56
for
n being
Element of
NAT for
a being
Real for
Q being
Subset of
(TOP-REAL n) for
w1,
w7 being
Point of
(TOP-REAL n) st
n >= 2 &
Q = { q where q is Point of (TOP-REAL n) : |.q.| > a } &
w1 in Q &
w7 in Q & ex
r being
Real st
(
w1 = r * w7 or
w7 = r * w1 ) holds
ex
w2,
w3,
w4,
w5,
w6 being
Point of
(TOP-REAL n) st
(
w2 in Q &
w3 in Q &
w4 in Q &
w5 in Q &
w6 in Q &
LSeg w1,
w2 c= Q &
LSeg w2,
w3 c= Q &
LSeg w3,
w4 c= Q &
LSeg w4,
w5 c= Q &
LSeg w5,
w6 c= Q &
LSeg w6,
w7 c= Q )
theorem Th57: :: JORDAN2C:57
for
n being
Element of
NAT for
a being
Real for
Q being
Subset of
(TOP-REAL n) for
w1,
w7 being
Point of
(TOP-REAL n) st
n >= 2 &
Q = (REAL n) \ { q where q is Point of (TOP-REAL n) : |.q.| < a } &
w1 in Q &
w7 in Q & ex
r being
Real st
(
w1 = r * w7 or
w7 = r * w1 ) holds
ex
w2,
w3,
w4,
w5,
w6 being
Point of
(TOP-REAL n) st
(
w2 in Q &
w3 in Q &
w4 in Q &
w5 in Q &
w6 in Q &
LSeg w1,
w2 c= Q &
LSeg w2,
w3 c= Q &
LSeg w3,
w4 c= Q &
LSeg w4,
w5 c= Q &
LSeg w5,
w6 c= Q &
LSeg w6,
w7 c= Q )
theorem Th58: :: JORDAN2C:58
theorem Th59: :: JORDAN2C:59
theorem Th60: :: JORDAN2C:60
theorem Th61: :: JORDAN2C:61
theorem Th62: :: JORDAN2C:62
theorem Th63: :: JORDAN2C:63
theorem Th64: :: JORDAN2C:64
theorem :: JORDAN2C:65
theorem :: JORDAN2C:66
theorem Th67: :: JORDAN2C:67
theorem Th68: :: JORDAN2C:68
theorem Th69: :: JORDAN2C:69
theorem Th70: :: JORDAN2C:70
theorem Th71: :: JORDAN2C:71
theorem Th72: :: JORDAN2C:72
theorem Th73: :: JORDAN2C:73
theorem Th74: :: JORDAN2C:74
theorem Th75: :: JORDAN2C:75
theorem Th76: :: JORDAN2C:76
theorem Th77: :: JORDAN2C:77
theorem Th78: :: JORDAN2C:78
theorem :: JORDAN2C:79
theorem Th80: :: JORDAN2C:80
theorem Th81: :: JORDAN2C:81
theorem Th82: :: JORDAN2C:82
theorem Th83: :: JORDAN2C:83
theorem Th84: :: JORDAN2C:84
theorem Th85: :: JORDAN2C:85
theorem Th86: :: JORDAN2C:86
theorem Th87: :: JORDAN2C:87
theorem Th88: :: JORDAN2C:88
theorem Th89: :: JORDAN2C:89
theorem Th90: :: JORDAN2C:90
theorem Th91: :: JORDAN2C:91
theorem Th92: :: JORDAN2C:92
:: deftheorem JORDAN2C:def 9 :
canceled;
:: deftheorem Def10 defines pi JORDAN2C:def 10 :
theorem Th93: :: JORDAN2C:93
theorem Th94: :: JORDAN2C:94
theorem Th95: :: JORDAN2C:95
theorem :: JORDAN2C:96
theorem Th97: :: JORDAN2C:97
theorem Th98: :: JORDAN2C:98
theorem Th99: :: JORDAN2C:99
theorem Th100: :: JORDAN2C:100
theorem Th101: :: JORDAN2C:101
theorem Th102: :: JORDAN2C:102
theorem Th103: :: JORDAN2C:103
theorem Th104: :: JORDAN2C:104
theorem Th105: :: JORDAN2C:105
theorem Th106: :: JORDAN2C:106
theorem Th107: :: JORDAN2C:107
theorem Th108: :: JORDAN2C:108
theorem Th109: :: JORDAN2C:109
theorem Th110: :: JORDAN2C:110
theorem Th111: :: JORDAN2C:111
theorem :: JORDAN2C:112
theorem Th113: :: JORDAN2C:113
theorem Th114: :: JORDAN2C:114
theorem Th115: :: JORDAN2C:115
theorem Th116: :: JORDAN2C:116
theorem :: JORDAN2C:117
theorem :: JORDAN2C:118
theorem :: JORDAN2C:119
theorem :: JORDAN2C:120
theorem :: JORDAN2C:121
theorem :: JORDAN2C:122
theorem :: JORDAN2C:123
theorem Th124: :: JORDAN2C:124
theorem :: JORDAN2C:125
theorem :: JORDAN2C:126
theorem :: JORDAN2C:127
Lm2:
for p being Point of (TOP-REAL 2) holds p is Point of (Euclid 2)
theorem Th128: :: JORDAN2C:128
theorem Th129: :: JORDAN2C:129
theorem Th130: :: JORDAN2C:130
theorem Th131: :: JORDAN2C:131
theorem Th132: :: JORDAN2C:132
theorem Th133: :: JORDAN2C:133
theorem :: JORDAN2C:134
theorem :: JORDAN2C:135
theorem :: JORDAN2C:136
theorem :: JORDAN2C:137