:: Continuous Functions on Real and Complex Normed Linear Spaces
:: by Noboru Endou
::
:: Received August 20, 2004
:: Copyright (c) 2004 Association of Mizar Users
theorem :: NCFCONT1:1
theorem Th2: :: NCFCONT1:2
:: deftheorem NCFCONT1:def 1 :
canceled;
:: deftheorem Def2 defines ||. NCFCONT1:def 2 :
:: deftheorem Def3 defines ||. NCFCONT1:def 3 :
:: deftheorem Def4 defines ||. NCFCONT1:def 4 :
:: deftheorem Def5 defines Neighbourhood NCFCONT1:def 5 :
theorem Th3: :: NCFCONT1:3
theorem Th4: :: NCFCONT1:4
:: deftheorem Def6 defines compact NCFCONT1:def 6 :
:: deftheorem defines closed NCFCONT1:def 7 :
:: deftheorem defines open NCFCONT1:def 8 :
:: deftheorem NCFCONT1:def 9 :
canceled;
:: deftheorem NCFCONT1:def 10 :
canceled;
:: deftheorem NCFCONT1:def 11 :
canceled;
:: deftheorem NCFCONT1:def 12 :
canceled;
:: deftheorem NCFCONT1:def 13 :
canceled;
:: deftheorem NCFCONT1:def 14 :
canceled;
:: deftheorem Def15 defines is_continuous_in NCFCONT1:def 15 :
:: deftheorem Def16 defines is_continuous_in NCFCONT1:def 16 :
:: deftheorem Def17 defines is_continuous_in NCFCONT1:def 17 :
:: deftheorem Def18 defines is_continuous_in NCFCONT1:def 18 :
:: deftheorem Def19 defines is_continuous_in NCFCONT1:def 19 :
:: deftheorem Def20 defines is_continuous_in NCFCONT1:def 20 :
theorem Th5: :: NCFCONT1:5
theorem Th6: :: NCFCONT1:6
theorem Th7: :: NCFCONT1:7
theorem Th8: :: NCFCONT1:8
theorem :: NCFCONT1:9
canceled;
theorem :: NCFCONT1:10
canceled;
theorem :: NCFCONT1:11
canceled;
theorem :: NCFCONT1:12
canceled;
theorem :: NCFCONT1:13
canceled;
theorem :: NCFCONT1:14
canceled;
theorem :: NCFCONT1:15
canceled;
theorem :: NCFCONT1:16
canceled;
theorem :: NCFCONT1:17
canceled;
theorem :: NCFCONT1:18
canceled;
theorem :: NCFCONT1:19
canceled;
theorem :: NCFCONT1:20
canceled;
theorem :: NCFCONT1:21
canceled;
theorem :: NCFCONT1:22
canceled;
theorem :: NCFCONT1:23
canceled;
theorem :: NCFCONT1:24
canceled;
theorem :: NCFCONT1:25
canceled;
theorem :: NCFCONT1:26
canceled;
theorem :: NCFCONT1:27
canceled;
theorem :: NCFCONT1:28
canceled;
theorem Th29: :: NCFCONT1:29
theorem Th30: :: NCFCONT1:30
theorem Th31: :: NCFCONT1:31
theorem Th32: :: NCFCONT1:32
theorem Th33: :: NCFCONT1:33
theorem Th34: :: NCFCONT1:34
theorem Th35: :: NCFCONT1:35
theorem Th36: :: NCFCONT1:36
theorem Th37: :: NCFCONT1:37
theorem Th38: :: NCFCONT1:38
theorem Th39: :: NCFCONT1:39
theorem Th40: :: NCFCONT1:40
theorem :: NCFCONT1:41
theorem :: NCFCONT1:42
theorem :: NCFCONT1:43
theorem Th44: :: NCFCONT1:44
theorem Th45: :: NCFCONT1:45
theorem Th46: :: NCFCONT1:46
theorem Th47: :: NCFCONT1:47
theorem Th48: :: NCFCONT1:48
theorem Th49: :: NCFCONT1:49
theorem Th50: :: NCFCONT1:50
theorem Th51: :: NCFCONT1:51
theorem Th52: :: NCFCONT1:52
theorem :: NCFCONT1:53
theorem :: NCFCONT1:54
theorem :: NCFCONT1:55
theorem Th56: :: NCFCONT1:56
theorem Th57: :: NCFCONT1:57
theorem Th58: :: NCFCONT1:58
theorem :: NCFCONT1:59
theorem :: NCFCONT1:60
theorem :: NCFCONT1:61
:: deftheorem Def21 defines is_continuous_on NCFCONT1:def 21 :
:: deftheorem Def22 defines is_continuous_on NCFCONT1:def 22 :
:: deftheorem Def23 defines is_continuous_on NCFCONT1:def 23 :
:: deftheorem Def24 defines is_continuous_on NCFCONT1:def 24 :
:: deftheorem Def25 defines is_continuous_on NCFCONT1:def 25 :
:: deftheorem Def26 defines is_continuous_on NCFCONT1:def 26 :
theorem Th62: :: NCFCONT1:62
theorem Th63: :: NCFCONT1:63
theorem Th64: :: NCFCONT1:64
theorem Th65: :: NCFCONT1:65
theorem Th66: :: NCFCONT1:66
theorem Th67: :: NCFCONT1:67
theorem :: NCFCONT1:68
theorem :: NCFCONT1:69
theorem :: NCFCONT1:70
theorem :: NCFCONT1:71
theorem :: NCFCONT1:72
theorem :: NCFCONT1:73
theorem :: NCFCONT1:74
theorem Th75: :: NCFCONT1:75
theorem :: NCFCONT1:76
theorem Th77: :: NCFCONT1:77
theorem Th78: :: NCFCONT1:78
theorem Th79: :: NCFCONT1:79
theorem :: NCFCONT1:80
theorem :: NCFCONT1:81
theorem :: NCFCONT1:82
theorem Th83: :: NCFCONT1:83
theorem Th84: :: NCFCONT1:84
theorem Th85: :: NCFCONT1:85
theorem :: NCFCONT1:86
theorem :: NCFCONT1:87
theorem :: NCFCONT1:88
theorem Th89: :: NCFCONT1:89
theorem Th90: :: NCFCONT1:90
theorem Th91: :: NCFCONT1:91
theorem Th92: :: NCFCONT1:92
theorem Th93: :: NCFCONT1:93
theorem Th94: :: NCFCONT1:94
theorem :: NCFCONT1:95
theorem :: NCFCONT1:96
theorem :: NCFCONT1:97
theorem Th98: :: NCFCONT1:98
theorem Th99: :: NCFCONT1:99
theorem Th100: :: NCFCONT1:100
theorem :: NCFCONT1:101
theorem Th102: :: NCFCONT1:102
theorem :: NCFCONT1:103
theorem :: NCFCONT1:104
theorem :: NCFCONT1:105
theorem :: NCFCONT1:106
theorem Th107: :: NCFCONT1:107
theorem Th108: :: NCFCONT1:108
theorem Th109: :: NCFCONT1:109
theorem Th110: :: NCFCONT1:110
theorem Th111: :: NCFCONT1:111
theorem Th112: :: NCFCONT1:112
theorem Th113: :: NCFCONT1:113
theorem :: NCFCONT1:114
theorem :: NCFCONT1:115
theorem :: NCFCONT1:116
theorem :: NCFCONT1:117
:: deftheorem Def27 defines is_Lipschitzian_on NCFCONT1:def 27 :
:: deftheorem Def28 defines is_Lipschitzian_on NCFCONT1:def 28 :
:: deftheorem Def29 defines is_Lipschitzian_on NCFCONT1:def 29 :
:: deftheorem Def30 defines is_Lipschitzian_on NCFCONT1:def 30 :
:: deftheorem Def31 defines is_Lipschitzian_on NCFCONT1:def 31 :
:: deftheorem Def32 defines is_Lipschitzian_on NCFCONT1:def 32 :
theorem Th118: :: NCFCONT1:118
theorem Th119: :: NCFCONT1:119
theorem Th120: :: NCFCONT1:120
theorem :: NCFCONT1:121
theorem :: NCFCONT1:122
theorem :: NCFCONT1:123
theorem :: NCFCONT1:124
theorem :: NCFCONT1:125
theorem :: NCFCONT1:126
theorem Th127: :: NCFCONT1:127
theorem Th128: :: NCFCONT1:128
theorem Th129: :: NCFCONT1:129
theorem :: NCFCONT1:130
theorem :: NCFCONT1:131
theorem :: NCFCONT1:132
theorem Th133: :: NCFCONT1:133
theorem Th134: :: NCFCONT1:134
theorem Th135: :: NCFCONT1:135
theorem :: NCFCONT1:136
theorem Th137: :: NCFCONT1:137
theorem Th138: :: NCFCONT1:138
theorem Th139: :: NCFCONT1:139
theorem :: NCFCONT1:140
theorem Th141: :: NCFCONT1:141
theorem :: NCFCONT1:142
theorem :: NCFCONT1:143
theorem :: NCFCONT1:144
theorem :: NCFCONT1:145
theorem :: NCFCONT1:146
theorem :: NCFCONT1:147
theorem :: NCFCONT1:148
theorem Th149: :: NCFCONT1:149
theorem :: NCFCONT1:150
theorem :: NCFCONT1:151
theorem :: NCFCONT1:152
theorem Th153: :: NCFCONT1:153
theorem :: NCFCONT1:154