:: The Continuous Functions on Normed Linear Spaces
:: by Takaya Nishiyama, Keiji Ohkubo and Yasunari Shidama
::
:: Received April 6, 2004
:: Copyright (c) 2004 Association of Mizar Users
theorem :: NFCONT_1:1
theorem Th2: :: NFCONT_1:2
:: deftheorem NFCONT_1:def 1 :
canceled;
:: deftheorem Def2 defines ||. NFCONT_1:def 2 :
:: deftheorem Def3 defines Neighbourhood NFCONT_1:def 3 :
theorem Th3: :: NFCONT_1:3
theorem Th4: :: NFCONT_1:4
:: deftheorem Def4 defines compact NFCONT_1:def 4 :
:: deftheorem defines closed NFCONT_1:def 5 :
:: deftheorem defines open NFCONT_1:def 6 :
:: deftheorem NFCONT_1:def 7 :
canceled;
:: deftheorem NFCONT_1:def 8 :
canceled;
:: deftheorem Def9 defines is_continuous_in NFCONT_1:def 9 :
:: deftheorem Def10 defines is_continuous_in NFCONT_1:def 10 :
theorem Th5: :: NFCONT_1:5
theorem Th6: :: NFCONT_1:6
theorem :: NFCONT_1:7
canceled;
theorem :: NFCONT_1:8
canceled;
theorem :: NFCONT_1:9
canceled;
theorem :: NFCONT_1:10
canceled;
theorem :: NFCONT_1:11
canceled;
theorem :: NFCONT_1:12
canceled;
theorem :: NFCONT_1:13
canceled;
theorem Th14: :: NFCONT_1:14
theorem Th15: :: NFCONT_1:15
theorem Th16: :: NFCONT_1:16
theorem Th17: :: NFCONT_1:17
theorem :: NFCONT_1:18
theorem Th19: :: NFCONT_1:19
theorem Th20: :: NFCONT_1:20
theorem Th21: :: NFCONT_1:21
theorem :: NFCONT_1:22
theorem Th23: :: NFCONT_1:23
theorem :: NFCONT_1:24
:: deftheorem Def11 defines is_continuous_on NFCONT_1:def 11 :
:: deftheorem Def12 defines is_continuous_on NFCONT_1:def 12 :
theorem Th25: :: NFCONT_1:25
theorem Th26: :: NFCONT_1:26
theorem :: NFCONT_1:27
theorem :: NFCONT_1:28
theorem Th29: :: NFCONT_1:29
theorem Th30: :: NFCONT_1:30
theorem :: NFCONT_1:31
theorem Th32: :: NFCONT_1:32
theorem :: NFCONT_1:33
theorem Th34: :: NFCONT_1:34
theorem Th35: :: NFCONT_1:35
theorem :: NFCONT_1:36
theorem Th37: :: NFCONT_1:37
theorem Th38: :: NFCONT_1:38
theorem :: NFCONT_1:39
theorem Th40: :: NFCONT_1:40
theorem Th41: :: NFCONT_1:41
theorem Th42: :: NFCONT_1:42
theorem :: NFCONT_1:43
theorem :: NFCONT_1:44
:: deftheorem Def13 defines is_Lipschitzian_on NFCONT_1:def 13 :
:: deftheorem Def14 defines is_Lipschitzian_on NFCONT_1:def 14 :
theorem Th45: :: NFCONT_1:45
theorem :: NFCONT_1:46
theorem :: NFCONT_1:47
theorem Th48: :: NFCONT_1:48
theorem :: NFCONT_1:49
theorem Th50: :: NFCONT_1:50
theorem :: NFCONT_1:51
theorem Th52: :: NFCONT_1:52
theorem Th53: :: NFCONT_1:53
theorem :: NFCONT_1:54
theorem :: NFCONT_1:55
theorem Th56: :: NFCONT_1:56
theorem :: NFCONT_1:57
theorem :: NFCONT_1:58
theorem :: NFCONT_1:59
theorem Th60: :: NFCONT_1:60
theorem :: NFCONT_1:61