:: Fan Homeomorphisms in the Plane
:: by Yatsuka Nakamura
::
:: Received January 8, 2002
:: Copyright (c) 2002 Association of Mizar Users
Lm1:
for p being Point of (TOP-REAL 2) st p <> 0.REAL 2 holds
|.p.| > 0
theorem :: JGRAPH_4:1
canceled;
theorem :: JGRAPH_4:2
canceled;
theorem :: JGRAPH_4:3
canceled;
theorem :: JGRAPH_4:4
canceled;
theorem :: JGRAPH_4:5
canceled;
theorem Th6: :: JGRAPH_4:6
theorem Th7: :: JGRAPH_4:7
theorem Th8: :: JGRAPH_4:8
theorem Th9: :: JGRAPH_4:9
theorem Th10: :: JGRAPH_4:10
theorem Th11: :: JGRAPH_4:11
theorem Th12: :: JGRAPH_4:12
theorem Th13: :: JGRAPH_4:13
theorem Th14: :: JGRAPH_4:14
theorem Th15: :: JGRAPH_4:15
:: deftheorem Def1 defines NormF JGRAPH_4:def 1 :
theorem :: JGRAPH_4:16
theorem :: JGRAPH_4:17
canceled;
theorem :: JGRAPH_4:18
canceled;
theorem Th19: :: JGRAPH_4:19
theorem Th20: :: JGRAPH_4:20
theorem Th21: :: JGRAPH_4:21
theorem Th22: :: JGRAPH_4:22
:: deftheorem Def2 defines FanW JGRAPH_4:def 2 :
:: deftheorem Def3 defines -FanMorphW JGRAPH_4:def 3 :
theorem Th23: :: JGRAPH_4:23
theorem Th24: :: JGRAPH_4:24
theorem Th25: :: JGRAPH_4:25
Lm2:
for K being non empty Subset of (TOP-REAL 2) holds
( proj1 | K is continuous Function of ((TOP-REAL 2) | K),R^1 & ( for q being Point of ((TOP-REAL 2) | K) holds (proj1 | K) . q = proj1 . q ) )
Lm3:
for K being non empty Subset of (TOP-REAL 2) holds
( proj2 | K is continuous Function of ((TOP-REAL 2) | K),R^1 & ( for q being Point of ((TOP-REAL 2) | K) holds (proj2 | K) . q = proj2 . q ) )
Lm4:
dom (2 NormF ) = the carrier of (TOP-REAL 2)
by FUNCT_2:def 1;
Lm5:
for K being non empty Subset of (TOP-REAL 2) holds
( (2 NormF ) | K is continuous Function of ((TOP-REAL 2) | K),R^1 & ( for q being Point of ((TOP-REAL 2) | K) holds ((2 NormF ) | K) . q = (2 NormF ) . q ) )
Lm6:
for K1 being non empty Subset of (TOP-REAL 2)
for g1 being Function of ((TOP-REAL 2) | K1),R^1 st g1 = (2 NormF ) | K1 & ( for q being Point of (TOP-REAL 2) st q in the carrier of ((TOP-REAL 2) | K1) holds
q <> 0.REAL 2 ) holds
for q being Point of ((TOP-REAL 2) | K1) holds g1 . q <> 0
theorem Th26: :: JGRAPH_4:26
theorem Th27: :: JGRAPH_4:27
theorem Th28: :: JGRAPH_4:28
theorem Th29: :: JGRAPH_4:29
theorem Th30: :: JGRAPH_4:30
theorem Th31: :: JGRAPH_4:31
Lm7:
for sn being Real
for K1 being Subset of (TOP-REAL 2) st K1 = { p7 where p7 is Point of (TOP-REAL 2) : p7 `2 >= sn * |.p7.| } holds
K1 is closed
Lm8:
for sn being Real
for K1 being Subset of (TOP-REAL 2) st K1 = { p7 where p7 is Point of (TOP-REAL 2) : p7 `1 >= sn * |.p7.| } holds
K1 is closed
theorem Th32: :: JGRAPH_4:32
Lm9:
for sn being Real
for K1 being Subset of (TOP-REAL 2) st K1 = { p7 where p7 is Point of (TOP-REAL 2) : p7 `2 <= sn * |.p7.| } holds
K1 is closed
Lm10:
for sn being Real
for K1 being Subset of (TOP-REAL 2) st K1 = { p7 where p7 is Point of (TOP-REAL 2) : p7 `1 <= sn * |.p7.| } holds
K1 is closed
theorem Th33: :: JGRAPH_4:33
theorem Th34: :: JGRAPH_4:34
theorem Th35: :: JGRAPH_4:35
theorem Th36: :: JGRAPH_4:36
theorem Th37: :: JGRAPH_4:37
theorem Th38: :: JGRAPH_4:38
theorem Th39: :: JGRAPH_4:39
theorem Th40: :: JGRAPH_4:40
theorem Th41: :: JGRAPH_4:41
theorem Th42: :: JGRAPH_4:42
theorem Th43: :: JGRAPH_4:43
theorem Th44: :: JGRAPH_4:44
theorem Th45: :: JGRAPH_4:45
theorem Th46: :: JGRAPH_4:46
Lm11:
now
let K0 be
Subset of
(TOP-REAL 2);
:: thesis: for q4, q, p2 being Point of (TOP-REAL 2)
for O, u, uq being Point of (Euclid 2) st u in cl_Ball O,(|.p2.| + 1) & q = uq & q4 = u & O = 0.REAL 2 & |.q4.| = |.q.| holds
q in cl_Ball O,(|.p2.| + 1)let q4,
q,
p2 be
Point of
(TOP-REAL 2);
:: thesis: for O, u, uq being Point of (Euclid 2) st u in cl_Ball O,(|.p2.| + 1) & q = uq & q4 = u & O = 0.REAL 2 & |.q4.| = |.q.| holds
q in cl_Ball O,(|.p2.| + 1)let O,
u,
uq be
Point of
(Euclid 2);
:: thesis: ( u in cl_Ball O,(|.p2.| + 1) & q = uq & q4 = u & O = 0.REAL 2 & |.q4.| = |.q.| implies q in cl_Ball O,(|.p2.| + 1) )assume A1:
u in cl_Ball O,
(|.p2.| + 1)
;
:: thesis: ( q = uq & q4 = u & O = 0.REAL 2 & |.q4.| = |.q.| implies q in cl_Ball O,(|.p2.| + 1) )assume A2:
(
q = uq &
q4 = u &
O = 0.REAL 2 )
;
:: thesis: ( |.q4.| = |.q.| implies q in cl_Ball O,(|.p2.| + 1) )assume A3:
|.q4.| = |.q.|
;
:: thesis: q in cl_Ball O,(|.p2.| + 1)
hence
q in cl_Ball O,
(|.p2.| + 1)
;
:: thesis: verum
end;
theorem Th47: :: JGRAPH_4:47
theorem :: JGRAPH_4:48
theorem Th49: :: JGRAPH_4:49
theorem Th50: :: JGRAPH_4:50
theorem Th51: :: JGRAPH_4:51
theorem Th52: :: JGRAPH_4:52
theorem :: JGRAPH_4:53
theorem :: JGRAPH_4:54
theorem :: JGRAPH_4:55
:: deftheorem Def4 defines FanN JGRAPH_4:def 4 :
:: deftheorem Def5 defines -FanMorphN JGRAPH_4:def 5 :
theorem Th56: :: JGRAPH_4:56
theorem Th57: :: JGRAPH_4:57
theorem Th58: :: JGRAPH_4:58
theorem Th59: :: JGRAPH_4:59
theorem Th60: :: JGRAPH_4:60
theorem Th61: :: JGRAPH_4:61
theorem Th62: :: JGRAPH_4:62
theorem Th63: :: JGRAPH_4:63
theorem Th64: :: JGRAPH_4:64
theorem Th65: :: JGRAPH_4:65
theorem Th66: :: JGRAPH_4:66
theorem Th67: :: JGRAPH_4:67
theorem Th68: :: JGRAPH_4:68
theorem Th69: :: JGRAPH_4:69
theorem Th70: :: JGRAPH_4:70
theorem Th71: :: JGRAPH_4:71
theorem Th72: :: JGRAPH_4:72
theorem Th73: :: JGRAPH_4:73
theorem Th74: :: JGRAPH_4:74
theorem Th75: :: JGRAPH_4:75
theorem Th76: :: JGRAPH_4:76
theorem Th77: :: JGRAPH_4:77
theorem Th78: :: JGRAPH_4:78
theorem Th79: :: JGRAPH_4:79
theorem Th80: :: JGRAPH_4:80
theorem :: JGRAPH_4:81
theorem Th82: :: JGRAPH_4:82
theorem Th83: :: JGRAPH_4:83
theorem Th84: :: JGRAPH_4:84
theorem Th85: :: JGRAPH_4:85
theorem :: JGRAPH_4:86
theorem :: JGRAPH_4:87
theorem :: JGRAPH_4:88
:: deftheorem Def6 defines FanE JGRAPH_4:def 6 :
:: deftheorem Def7 defines -FanMorphE JGRAPH_4:def 7 :
theorem Th89: :: JGRAPH_4:89
theorem Th90: :: JGRAPH_4:90
theorem Th91: :: JGRAPH_4:91
theorem Th92: :: JGRAPH_4:92
theorem Th93: :: JGRAPH_4:93
theorem Th94: :: JGRAPH_4:94
theorem Th95: :: JGRAPH_4:95
theorem Th96: :: JGRAPH_4:96
theorem Th97: :: JGRAPH_4:97
theorem Th98: :: JGRAPH_4:98
theorem Th99: :: JGRAPH_4:99
theorem Th100: :: JGRAPH_4:100
theorem Th101: :: JGRAPH_4:101
theorem Th102: :: JGRAPH_4:102
theorem Th103: :: JGRAPH_4:103
theorem Th104: :: JGRAPH_4:104
theorem Th105: :: JGRAPH_4:105
theorem Th106: :: JGRAPH_4:106
theorem Th107: :: JGRAPH_4:107
theorem Th108: :: JGRAPH_4:108
theorem Th109: :: JGRAPH_4:109
theorem Th110: :: JGRAPH_4:110
theorem Th111: :: JGRAPH_4:111
theorem :: JGRAPH_4:112
theorem Th113: :: JGRAPH_4:113
theorem Th114: :: JGRAPH_4:114
theorem Th115: :: JGRAPH_4:115
theorem Th116: :: JGRAPH_4:116
theorem :: JGRAPH_4:117
theorem :: JGRAPH_4:118
theorem :: JGRAPH_4:119
:: deftheorem Def8 defines FanS JGRAPH_4:def 8 :
:: deftheorem Def9 defines -FanMorphS JGRAPH_4:def 9 :
theorem Th120: :: JGRAPH_4:120
theorem Th121: :: JGRAPH_4:121
theorem Th122: :: JGRAPH_4:122
theorem Th123: :: JGRAPH_4:123
theorem Th124: :: JGRAPH_4:124
theorem Th125: :: JGRAPH_4:125
theorem Th126: :: JGRAPH_4:126
theorem Th127: :: JGRAPH_4:127
theorem Th128: :: JGRAPH_4:128
theorem Th129: :: JGRAPH_4:129
theorem Th130: :: JGRAPH_4:130
theorem Th131: :: JGRAPH_4:131
theorem Th132: :: JGRAPH_4:132
theorem Th133: :: JGRAPH_4:133
theorem Th134: :: JGRAPH_4:134
theorem Th135: :: JGRAPH_4:135
theorem Th136: :: JGRAPH_4:136
theorem Th137: :: JGRAPH_4:137
theorem Th138: :: JGRAPH_4:138
theorem Th139: :: JGRAPH_4:139
theorem Th140: :: JGRAPH_4:140
theorem Th141: :: JGRAPH_4:141
theorem Th142: :: JGRAPH_4:142
theorem :: JGRAPH_4:143
theorem Th144: :: JGRAPH_4:144
theorem Th145: :: JGRAPH_4:145
theorem Th146: :: JGRAPH_4:146
theorem Th147: :: JGRAPH_4:147
theorem :: JGRAPH_4:148
theorem :: JGRAPH_4:149
theorem :: JGRAPH_4:150