:: Properties of Number-Valued Functions
:: by Library Committee
::
:: Received December 18, 2007
:: Copyright (c) 2007 Association of Mizar Users
Lm1:
for f being FinSequence
for h being Function st dom h = dom f holds
h is FinSequence
Lm2:
for f, g being FinSequence
for h being Function st dom h = (dom f) /\ (dom g) holds
h is FinSequence
:: deftheorem Def1 defines + VALUED_1:def 1 :
theorem :: VALUED_1:1
:: deftheorem Def2 defines + VALUED_1:def 2 :
theorem :: VALUED_1:2
:: deftheorem defines - VALUED_1:def 3 :
theorem :: VALUED_1:3
theorem :: VALUED_1:4
:: deftheorem Def4 defines (#) VALUED_1:def 4 :
theorem :: VALUED_1:5
:: deftheorem Def5 defines (#) VALUED_1:def 5 :
theorem Th6: :: VALUED_1:6
theorem :: VALUED_1:7
:: deftheorem defines - VALUED_1:def 6 :
theorem Th8: :: VALUED_1:8
theorem :: VALUED_1:9
:: deftheorem Def7 defines " VALUED_1:def 7 :
theorem Th10: :: VALUED_1:10
:: deftheorem defines ^2 VALUED_1:def 8 :
theorem Th11: :: VALUED_1:11
:: deftheorem defines - VALUED_1:def 9 :
theorem Th12: :: VALUED_1:12
theorem :: VALUED_1:13
theorem :: VALUED_1:14
Lm3:
for C being set
for D1, D2 being non empty complex-membered set
for f1 being Function of C,D1
for f2 being Function of C,D2 holds dom (f1 - f2) = C
theorem :: VALUED_1:15
:: deftheorem defines /" VALUED_1:def 10 :
theorem Th16: :: VALUED_1:16
theorem :: VALUED_1:17
Lm4:
for C being set
for D1, D2 being non empty complex-membered set
for f1 being Function of C,D1
for f2 being Function of C,D2 holds dom (f1 /" f2) = C
:: deftheorem Def11 defines |. VALUED_1:def 11 :
theorem :: VALUED_1:18
theorem :: VALUED_1:19
:: deftheorem Def12 defines Shift VALUED_1:def 12 :
theorem :: VALUED_1:20
theorem :: VALUED_1:21
theorem :: VALUED_1:22
theorem :: VALUED_1:23
theorem :: VALUED_1:24
theorem TW2: :: VALUED_1:25
theorem TW1: :: VALUED_1:26
theorem :: VALUED_1:27
:: deftheorem defines increasing VALUED_1:def 13 :
:: deftheorem defines decreasing VALUED_1:def 14 :
:: deftheorem defines non-decreasing VALUED_1:def 15 :
:: deftheorem defines non-increasing VALUED_1:def 16 :