:: Number-Valued Functions
:: by Library Committee
::
:: Received November 22, 2007
:: Copyright (c) 2007 Association of Mizar Users
:: deftheorem Def1 defines complex-valued VALUED_0:def 1 :
:: deftheorem Def2 defines ext-real-valued VALUED_0:def 2 :
:: deftheorem Def3 defines real-valued VALUED_0:def 3 :
:: deftheorem Def4 defines rational-valued VALUED_0:def 4 :
:: deftheorem Def5 defines integer-valued VALUED_0:def 5 :
:: deftheorem Def6 defines natural-valued VALUED_0:def 6 :
theorem Th1: :: VALUED_0:1
theorem Th2: :: VALUED_0:2
theorem Th3: :: VALUED_0:3
theorem Th4: :: VALUED_0:4
theorem Th5: :: VALUED_0:5
theorem Th6: :: VALUED_0:6
:: deftheorem Def7 defines complex-valued VALUED_0:def 7 :
:: deftheorem Def8 defines ext-real-valued VALUED_0:def 8 :
:: deftheorem Def9 defines real-valued VALUED_0:def 9 :
:: deftheorem Def10 defines rational-valued VALUED_0:def 10 :
:: deftheorem Def11 defines integer-valued VALUED_0:def 11 :
:: deftheorem Def12 defines natural-valued VALUED_0:def 12 :
theorem Th7: :: VALUED_0:7
theorem Th8: :: VALUED_0:8
theorem Th9: :: VALUED_0:9
theorem Th10: :: VALUED_0:10
theorem Th11: :: VALUED_0:11
theorem Th12: :: VALUED_0:12
theorem :: VALUED_0:13
theorem :: VALUED_0:14
theorem :: VALUED_0:15
theorem :: VALUED_0:16
theorem :: VALUED_0:17
theorem :: VALUED_0:18
:: deftheorem Def13 defines increasing VALUED_0:def 13 :
:: deftheorem Def14 defines decreasing VALUED_0:def 14 :
:: deftheorem Def15 defines non-decreasing VALUED_0:def 15 :
:: deftheorem Def16 defines non-increasing VALUED_0:def 16 :
:: deftheorem Def17 defines subsequence VALUED_0:def 17 :
theorem :: VALUED_0:19
theorem :: VALUED_0:20
theorem Th21: :: VALUED_0:21
theorem :: VALUED_0:22
:: deftheorem defines constant VALUED_0:def 18 :
theorem Th23: :: VALUED_0:23
theorem Th24: :: VALUED_0:24
theorem :: VALUED_0:25
theorem :: VALUED_0:26
theorem Th27: :: VALUED_0:27
theorem Th28: :: VALUED_0:28
theorem :: VALUED_0:29
theorem Th38: :: VALUED_0:30
theorem :: VALUED_0:31
:: deftheorem defines zeroed VALUED_0:def 19 :