:: Real Function Continuity
:: by Konrad Raczkowski and Pawe{\l} Sadowski
::
:: Received June 18, 1990
:: Copyright (c) 1990 Association of Mizar Users
:: deftheorem Def1 defines is_continuous_in FCONT_1:def 1 :
theorem Tx1: :: FCONT_1:1
theorem :: FCONT_1:2
theorem Th3: :: FCONT_1:3
theorem Th4: :: FCONT_1:4
theorem Th5: :: FCONT_1:5
theorem :: FCONT_1:6
theorem Th7: :: FCONT_1:7
theorem Th8: :: FCONT_1:8
theorem :: FCONT_1:9
theorem Th10: :: FCONT_1:10
theorem :: FCONT_1:11
theorem Th12: :: FCONT_1:12
:: deftheorem Def2 defines continuous FCONT_1:def 2 :
theorem :: FCONT_1:13
canceled;
theorem Th14: :: FCONT_1:14
theorem Th15: :: FCONT_1:15
theorem :: FCONT_1:16
theorem Th17: :: FCONT_1:17
theorem :: FCONT_1:18
theorem Th19: :: FCONT_1:19
theorem :: FCONT_1:20
theorem Th21: :: FCONT_1:21
theorem :: FCONT_1:22
theorem Th23: :: FCONT_1:23
theorem :: FCONT_1:24
theorem :: FCONT_1:25
theorem :: FCONT_1:26
theorem :: FCONT_1:27
theorem :: FCONT_1:28
theorem Th29: :: FCONT_1:29
theorem :: FCONT_1:30
theorem Th31: :: FCONT_1:31
theorem :: FCONT_1:32
:: deftheorem XDef3 defines Lipschitzian FCONT_1:def 3 :
theorem Def3: :: FCONT_1:33
theorem :: FCONT_1:34
theorem :: FCONT_1:35
theorem :: FCONT_1:36
theorem :: FCONT_1:37
theorem :: FCONT_1:38
theorem :: FCONT_1:39
theorem :: FCONT_1:40
theorem :: FCONT_1:41
theorem :: FCONT_1:42
theorem :: FCONT_1:43
theorem :: FCONT_1:44
theorem :: FCONT_1:45
theorem :: FCONT_1:46
theorem :: FCONT_1:47
theorem :: FCONT_1:48
theorem Th49: :: FCONT_1:49
theorem :: FCONT_1:50
theorem Th51: :: FCONT_1:51
theorem :: FCONT_1:52
theorem Th53: :: FCONT_1:53
theorem :: FCONT_1:54