:: Miscellaneous Facts about Functions
:: by Grzegorz Bancerek and Andrzej Trybulec
::
:: Received January 12, 1996
:: Copyright (c) 1996 Association of Mizar Users
theorem :: FUNCT_7:1
theorem :: FUNCT_7:2
theorem Th3: :: FUNCT_7:3
theorem Th4: :: FUNCT_7:4
theorem :: FUNCT_7:5
theorem Th6: :: FUNCT_7:6
theorem Th7: :: FUNCT_7:7
theorem :: FUNCT_7:8
theorem :: FUNCT_7:9
canceled;
theorem Th10: :: FUNCT_7:10
theorem Th11: :: FUNCT_7:11
theorem :: FUNCT_7:12
theorem Th13: :: FUNCT_7:13
theorem :: FUNCT_7:14
theorem :: FUNCT_7:15
theorem :: FUNCT_7:16
theorem :: FUNCT_7:17
canceled;
theorem :: FUNCT_7:18
theorem :: FUNCT_7:19
theorem Th20: :: FUNCT_7:20
theorem :: FUNCT_7:21
for
A,
B being
set st
A * c= B * holds
A c= B
theorem :: FUNCT_7:22
theorem :: FUNCT_7:23
theorem Th24: :: FUNCT_7:24
theorem Th25: :: FUNCT_7:25
:: deftheorem Def1 defines In FUNCT_7:def 1 :
for
x,
y being
set st
x in y holds
In x,
y = x;
theorem :: FUNCT_7:26
:: deftheorem Def2 defines equal_outside FUNCT_7:def 2 :
theorem Th27: :: FUNCT_7:27
theorem Th28: :: FUNCT_7:28
theorem Th29: :: FUNCT_7:29
theorem Th30: :: FUNCT_7:30
theorem Th31: :: FUNCT_7:31
:: deftheorem Def3 defines +* FUNCT_7:def 3 :
theorem Th32: :: FUNCT_7:32
theorem Th33: :: FUNCT_7:33
theorem Th34: :: FUNCT_7:34
theorem :: FUNCT_7:35
theorem :: FUNCT_7:36
theorem Th37: :: FUNCT_7:37
theorem :: FUNCT_7:38
theorem :: FUNCT_7:39
theorem :: FUNCT_7:40
:: deftheorem Def4 defines compose FUNCT_7:def 4 :
:: deftheorem Def5 defines apply FUNCT_7:def 5 :
theorem Th41: :: FUNCT_7:41
theorem Th42: :: FUNCT_7:42
theorem Th43: :: FUNCT_7:43
theorem Th44: :: FUNCT_7:44
theorem :: FUNCT_7:45
theorem :: FUNCT_7:46
theorem Th47: :: FUNCT_7:47
theorem :: FUNCT_7:48
theorem Th49: :: FUNCT_7:49
theorem :: FUNCT_7:50
theorem Th51: :: FUNCT_7:51
theorem :: FUNCT_7:52
theorem Th53: :: FUNCT_7:53
theorem :: FUNCT_7:54
theorem Th55: :: FUNCT_7:55
theorem Th56: :: FUNCT_7:56
theorem :: FUNCT_7:57
theorem :: FUNCT_7:58
:: deftheorem Def6 defines firstdom FUNCT_7:def 6 :
:: deftheorem Def7 defines lastrng FUNCT_7:def 7 :
theorem Th59: :: FUNCT_7:59
theorem Th60: :: FUNCT_7:60
theorem Th61: :: FUNCT_7:61
:: deftheorem Def8 defines FuncSeq-like FUNCT_7:def 8 :
theorem Th62: :: FUNCT_7:62
theorem Th63: :: FUNCT_7:63
theorem Th64: :: FUNCT_7:64
theorem :: FUNCT_7:65
theorem :: FUNCT_7:66
theorem :: FUNCT_7:67
:: deftheorem Def9 defines FuncSequence FUNCT_7:def 9 :
:: deftheorem Def10 defines FuncSequence FUNCT_7:def 10 :
theorem Th68: :: FUNCT_7:68
theorem :: FUNCT_7:69
Lm1:
for X being set
for f being Function of X,X holds rng f c= dom f
Lm2:
for f being Function
for n being Element of NAT
for p1, p2 being Function of NAT , PFuncs ((dom f) \/ (rng f)),((dom f) \/ (rng f)) st p1 . 0 = id ((dom f) \/ (rng f)) & ( for k being Nat ex g being Function st
( g = p1 . k & p1 . (k + 1) = g * f ) ) & p2 . 0 = id ((dom f) \/ (rng f)) & ( for k being Nat ex g being Function st
( g = p2 . k & p2 . (k + 1) = g * f ) ) holds
p1 = p2
definition
let f be
Function;
let n be
Nat;
func iter f,
n -> Function means :
Def11:
:: FUNCT_7:def 11
ex
p being
Function of
NAT ,
PFuncs ((dom f) \/ (rng f)),
((dom f) \/ (rng f)) st
(
it = p . n &
p . 0 = id ((dom f) \/ (rng f)) & ( for
k being
Nat ex
g being
Function st
(
g = p . k &
p . (k + 1) = g * f ) ) );
existence
ex b1 being Function ex p being Function of NAT , PFuncs ((dom f) \/ (rng f)),((dom f) \/ (rng f)) st
( b1 = p . n & p . 0 = id ((dom f) \/ (rng f)) & ( for k being Nat ex g being Function st
( g = p . k & p . (k + 1) = g * f ) ) )
uniqueness
for b1, b2 being Function st ex p being Function of NAT , PFuncs ((dom f) \/ (rng f)),((dom f) \/ (rng f)) st
( b1 = p . n & p . 0 = id ((dom f) \/ (rng f)) & ( for k being Nat ex g being Function st
( g = p . k & p . (k + 1) = g * f ) ) ) & ex p being Function of NAT , PFuncs ((dom f) \/ (rng f)),((dom f) \/ (rng f)) st
( b2 = p . n & p . 0 = id ((dom f) \/ (rng f)) & ( for k being Nat ex g being Function st
( g = p . k & p . (k + 1) = g * f ) ) ) holds
b1 = b2
by Lm2;
end;
:: deftheorem Def11 defines iter FUNCT_7:def 11 :
Lm3:
for f being Function holds
( (id ((dom f) \/ (rng f))) * f = f & f * (id ((dom f) \/ (rng f))) = f )
theorem Th70: :: FUNCT_7:70
Lm4:
for f being Function st rng f c= dom f holds
iter f,0 = id (dom f)
theorem Th71: :: FUNCT_7:71
theorem Th72: :: FUNCT_7:72
theorem Th73: :: FUNCT_7:73
theorem Th74: :: FUNCT_7:74
theorem :: FUNCT_7:75
theorem Th76: :: FUNCT_7:76
theorem Th77: :: FUNCT_7:77
theorem :: FUNCT_7:78
theorem Th79: :: FUNCT_7:79
Lm5:
for f being Function
for m, k being Element of NAT st iter (iter f,m),k = iter f,(m * k) holds
iter (iter f,m),(k + 1) = iter f,(m * (k + 1))
theorem :: FUNCT_7:80
theorem Th81: :: FUNCT_7:81
theorem :: FUNCT_7:82
theorem :: FUNCT_7:83
theorem :: FUNCT_7:84
theorem :: FUNCT_7:85
theorem :: FUNCT_7:86
theorem :: FUNCT_7:87
theorem :: FUNCT_7:88
theorem :: FUNCT_7:89
theorem :: FUNCT_7:90
theorem :: FUNCT_7:91
theorem :: FUNCT_7:92
theorem :: FUNCT_7:93
theorem Th94: :: FUNCT_7:94
theorem :: FUNCT_7:95
theorem Th96: :: FUNCT_7:96
theorem :: FUNCT_7:97
theorem :: FUNCT_7:98
theorem Th99: :: FUNCT_7:99
theorem :: FUNCT_7:100
:: deftheorem Def12 defines Swap FUNCT_7:def 12 :
theorem Th101: :: FUNCT_7:101
theorem Th102: :: FUNCT_7:102
theorem Th103: :: FUNCT_7:103
theorem Th104: :: FUNCT_7:104
theorem :: FUNCT_7:105
theorem :: FUNCT_7:106
theorem :: FUNCT_7:107
theorem :: FUNCT_7:108
theorem Th109: :: FUNCT_7:109
theorem :: FUNCT_7:110
theorem :: FUNCT_7:111
theorem Th112: :: FUNCT_7:112
theorem :: FUNCT_7:113
theorem :: FUNCT_7:114
theorem :: FUNCT_7:115
theorem :: FUNCT_7:116
theorem Th117: :: FUNCT_7:117
theorem Th118: :: FUNCT_7:118
theorem :: FUNCT_7:119
:: deftheorem defines followed_by FUNCT_7:def 13 :
theorem Thy: :: FUNCT_7:120
theorem Th54: :: FUNCT_7:121
theorem Th55: :: FUNCT_7:122
:: deftheorem defines followed_by FUNCT_7:def 14 :
theorem Thx: :: FUNCT_7:123
theorem Th57: :: FUNCT_7:124
theorem Th58: :: FUNCT_7:125
theorem Th59: :: FUNCT_7:126
theorem Th60: :: FUNCT_7:127
theorem Th62: :: FUNCT_7:128
theorem :: FUNCT_7:129
theorem :: FUNCT_7:130
theorem :: FUNCT_7:131