begin
Lm1:
for p being Point of st p <> 0. (TOP-REAL 2) holds
|.p.| > 0
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem Th6:
theorem Th7:
theorem Th8:
theorem Th9:
theorem Th10:
theorem Th11:
theorem Th12:
theorem Th13:
theorem Th14:
theorem Th15:
:: deftheorem Def1 defines NormF JGRAPH_4:def 1 :
theorem
theorem
canceled;
theorem
canceled;
theorem Th19:
theorem Th20:
theorem Th21:
theorem Th22:
begin
:: deftheorem Def2 defines FanW JGRAPH_4:def 2 :
:: deftheorem Def3 defines -FanMorphW JGRAPH_4:def 3 :
theorem Th23:
theorem Th24:
theorem Th25:
Lm2:
for K being non empty Subset of holds
( proj1 | K is continuous Function of ((TOP-REAL 2) | K),R^1 & ( for q being Point of holds (proj1 | K) . q = proj1 . q ) )
Lm3:
for K being non empty Subset of holds
( proj2 | K is continuous Function of ((TOP-REAL 2) | K),R^1 & ( for q being Point of 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 holds
( (2 NormF ) | K is continuous Function of ((TOP-REAL 2) | K),R^1 & ( for q being Point of holds ((2 NormF ) | K) . q = (2 NormF ) . q ) )
Lm6:
for K1 being non empty Subset of
for g1 being Function of ((TOP-REAL 2) | K1),R^1 st g1 = (2 NormF ) | K1 & ( for q being Point of st q in the carrier of ((TOP-REAL 2) | K1) holds
q <> 0. (TOP-REAL 2) ) holds
for q being Point of holds g1 . q <> 0
theorem Th26:
theorem Th27:
theorem Th28:
theorem Th29:
theorem Th30:
theorem Th31:
Lm7:
for sn being Real
for K1 being Subset of st K1 = { p7 where p7 is Point of : p7 `2 >= sn * |.p7.| } holds
K1 is closed
Lm8:
for sn being Real
for K1 being Subset of st K1 = { p7 where p7 is Point of : p7 `1 >= sn * |.p7.| } holds
K1 is closed
theorem Th32:
Lm9:
for sn being Real
for K1 being Subset of st K1 = { p7 where p7 is Point of : p7 `2 <= sn * |.p7.| } holds
K1 is closed
Lm10:
for sn being Real
for K1 being Subset of st K1 = { p7 where p7 is Point of : p7 `1 <= sn * |.p7.| } holds
K1 is closed
theorem Th33:
theorem Th34:
theorem Th35:
theorem Th36:
theorem Th37:
theorem Th38:
theorem Th39:
theorem Th40:
theorem Th41:
theorem Th42:
theorem Th43:
Lm11:
TopStruct(# the carrier of (TOP-REAL 2),the topology of (TOP-REAL 2) #) = TopSpaceMetr (Euclid 2)
by EUCLID:def 8;
theorem Th44:
theorem Th45:
theorem Th46:
Lm12:
for q4, q, p2 being Point of
for O, u, uq being Point of st u in cl_Ball O,(|.p2.| + 1) & q = uq & q4 = u & O = 0. (TOP-REAL 2) & |.q4.| = |.q.| holds
q in cl_Ball O,(|.p2.| + 1)
theorem Th47:
theorem
theorem Th49:
theorem Th50:
theorem Th51:
theorem Th52:
theorem
theorem
theorem
begin
:: deftheorem Def4 defines FanN JGRAPH_4:def 4 :
:: deftheorem Def5 defines -FanMorphN JGRAPH_4:def 5 :
theorem Th56:
theorem Th57:
theorem Th58:
theorem Th59:
theorem Th60:
theorem Th61:
theorem Th62:
theorem Th63:
theorem Th64:
theorem Th65:
theorem Th66:
theorem Th67:
theorem Th68:
theorem Th69:
theorem Th70:
theorem Th71:
theorem Th72:
theorem Th73:
theorem Th74:
theorem Th75:
theorem Th76:
theorem Th77:
theorem Th78:
theorem Th79:
theorem Th80:
theorem
theorem Th82:
theorem Th83:
theorem Th84:
theorem Th85:
theorem
theorem
theorem
begin
:: deftheorem Def6 defines FanE JGRAPH_4:def 6 :
:: deftheorem Def7 defines -FanMorphE JGRAPH_4:def 7 :
theorem Th89:
theorem Th90:
theorem Th91:
theorem Th92:
theorem Th93:
theorem Th94:
theorem Th95:
theorem Th96:
theorem Th97:
theorem Th98:
theorem Th99:
theorem Th100:
theorem Th101:
theorem Th102:
theorem Th103:
theorem Th104:
theorem Th105:
theorem Th106:
theorem Th107:
theorem Th108:
theorem Th109:
theorem Th110:
theorem Th111:
theorem
theorem Th113:
theorem Th114:
theorem Th115:
theorem Th116:
theorem
theorem
theorem
begin
:: deftheorem Def8 defines FanS JGRAPH_4:def 8 :
:: deftheorem Def9 defines -FanMorphS JGRAPH_4:def 9 :
theorem Th120:
theorem Th121:
theorem Th122:
theorem Th123:
theorem Th124:
theorem Th125:
theorem Th126:
theorem Th127:
theorem Th128:
theorem Th129:
theorem Th130:
theorem Th131:
theorem Th132:
theorem Th133:
theorem Th134:
theorem Th135:
theorem Th136:
theorem Th137:
theorem Th138:
theorem Th139:
theorem Th140:
theorem Th141:
theorem Th142:
theorem
theorem Th144:
theorem Th145:
theorem Th146:
theorem Th147:
theorem
theorem
theorem