:: Properties of Real Functions
:: by Jaros{\l}aw Kotowicz
::
:: Received June 18, 1990
:: Copyright (c) 1990 Association of Mizar Users
theorem :: RFUNCT_2:1
canceled;
theorem :: RFUNCT_2:2
canceled;
theorem :: RFUNCT_2:3
canceled;
theorem :: RFUNCT_2:4
canceled;
theorem :: RFUNCT_2:5
canceled;
theorem Th6: :: RFUNCT_2:6
theorem :: RFUNCT_2:7
canceled;
theorem :: RFUNCT_2:8
canceled;
theorem :: RFUNCT_2:9
canceled;
theorem :: RFUNCT_2:10
canceled;
theorem :: RFUNCT_2:11
canceled;
theorem :: RFUNCT_2:12
canceled;
theorem Th13: :: RFUNCT_2:13
theorem Th14: :: RFUNCT_2:14
theorem :: RFUNCT_2:15
theorem Th16: :: RFUNCT_2:16
theorem :: RFUNCT_2:17
theorem :: RFUNCT_2:18
theorem :: RFUNCT_2:19
canceled;
theorem :: RFUNCT_2:20
canceled;
theorem :: RFUNCT_2:21
canceled;
theorem :: RFUNCT_2:22
canceled;
theorem Th23: :: RFUNCT_2:23
theorem Th24: :: RFUNCT_2:24
theorem :: RFUNCT_2:25
theorem :: RFUNCT_2:26
theorem :: RFUNCT_2:27
theorem :: RFUNCT_2:28
canceled;
theorem :: RFUNCT_2:29
canceled;
theorem :: RFUNCT_2:30
canceled;
theorem :: RFUNCT_2:31
canceled;
theorem :: RFUNCT_2:32
theorem :: RFUNCT_2:33
theorem :: RFUNCT_2:34
canceled;
theorem :: RFUNCT_2:35
canceled;
theorem :: RFUNCT_2:36
theorem :: RFUNCT_2:37
theorem :: RFUNCT_2:38
canceled;
theorem :: RFUNCT_2:39
canceled;
theorem :: RFUNCT_2:40
theorem Th41: :: RFUNCT_2:41
theorem :: RFUNCT_2:42
:: deftheorem RFUNCT_2:def 1 :
canceled;
:: deftheorem NDef2 defines increasing RFUNCT_2:def 2 :
:: deftheorem NDef3 defines decreasing RFUNCT_2:def 3 :
:: deftheorem NDef4 defines non-decreasing RFUNCT_2:def 4 :
:: deftheorem NDef5 defines non-increasing RFUNCT_2:def 5 :
theorem Def2: :: RFUNCT_2:43
theorem Def3: :: RFUNCT_2:44
theorem Def4: :: RFUNCT_2:45
theorem Def5: :: RFUNCT_2:46
:: deftheorem Def6 defines monotone RFUNCT_2:def 6 :
theorem :: RFUNCT_2:47
canceled;
theorem Th48: :: RFUNCT_2:48
theorem Th49: :: RFUNCT_2:49
theorem :: RFUNCT_2:50
canceled;
theorem :: RFUNCT_2:51
canceled;
theorem :: RFUNCT_2:52
canceled;
theorem :: RFUNCT_2:53
canceled;
theorem :: RFUNCT_2:54
theorem :: RFUNCT_2:55
canceled;
theorem :: RFUNCT_2:56
canceled;
theorem :: RFUNCT_2:57
canceled;
theorem :: RFUNCT_2:58
canceled;
theorem :: RFUNCT_2:59
theorem :: RFUNCT_2:60
theorem :: RFUNCT_2:61
theorem :: RFUNCT_2:62
theorem :: RFUNCT_2:63
theorem Th64: :: RFUNCT_2:64
theorem :: RFUNCT_2:65
theorem Th66: :: RFUNCT_2:66
theorem :: RFUNCT_2:67
theorem Th68: :: RFUNCT_2:68
theorem :: RFUNCT_2:69
theorem :: RFUNCT_2:70
theorem :: RFUNCT_2:71
theorem :: RFUNCT_2:72
theorem :: RFUNCT_2:73
theorem :: RFUNCT_2:74
theorem :: RFUNCT_2:75
theorem :: RFUNCT_2:76
theorem :: RFUNCT_2:77
theorem :: RFUNCT_2:78
theorem :: RFUNCT_2:79
theorem :: RFUNCT_2:80
theorem :: RFUNCT_2:81
theorem :: RFUNCT_2:82
theorem :: RFUNCT_2:83
theorem :: RFUNCT_2:84