:: The Modification of a Function by a Functionand the Iteration of the Composition of a Function
:: by Czes{\l}aw Byli\'nski
::
:: Received March 1, 1990
:: Copyright (c) 1990 Association of Mizar Users
Lm1:
for x, y, Z being set st [x,y] in Z holds
( x in union (union Z) & y in union (union Z) )
Lm2:
for x, x', y, y', x1, x1', y1, y1' being set st [[x,x'],[y,y']] = [[x1,x1'],[y1,y1']] holds
( x = x1 & y = y1 & x' = x1' & y' = y1' )
theorem Th1: :: FUNCT_4:1
for
Z being
set st ( for
z being
set st
z in Z holds
ex
x,
y being
set st
z = [x,y] ) holds
ex
X,
Y being
set st
Z c= [:X,Y:]
theorem :: FUNCT_4:2
theorem :: FUNCT_4:3
canceled;
theorem :: FUNCT_4:4
theorem :: FUNCT_4:5
theorem Th6: :: FUNCT_4:6
theorem :: FUNCT_4:7
theorem :: FUNCT_4:8
theorem :: FUNCT_4:9
theorem :: FUNCT_4:10
:: deftheorem Def1 defines +* FUNCT_4:def 1 :
theorem Th11: :: FUNCT_4:11
theorem Th12: :: FUNCT_4:12
theorem Th13: :: FUNCT_4:13
theorem Th14: :: FUNCT_4:14
theorem Th15: :: FUNCT_4:15
theorem Th16: :: FUNCT_4:16
theorem :: FUNCT_4:17
theorem Th18: :: FUNCT_4:18
theorem :: FUNCT_4:19
theorem Th20: :: FUNCT_4:20
theorem Th21: :: FUNCT_4:21
theorem Th22: :: FUNCT_4:22
theorem :: FUNCT_4:23
theorem :: FUNCT_4:24
theorem Th25: :: FUNCT_4:25
theorem Th26: :: FUNCT_4:26
theorem :: FUNCT_4:27
theorem Th28: :: FUNCT_4:28
theorem Th29: :: FUNCT_4:29
theorem Th30: :: FUNCT_4:30
theorem Th31: :: FUNCT_4:31
theorem Th32: :: FUNCT_4:32
theorem Th33: :: FUNCT_4:33
theorem :: FUNCT_4:34
theorem Th35: :: FUNCT_4:35
theorem :: FUNCT_4:36
theorem :: FUNCT_4:37
theorem Th38: :: FUNCT_4:38
theorem :: FUNCT_4:39
theorem :: FUNCT_4:40
theorem :: FUNCT_4:41
definition
let f be
Function;
func ~ f -> Function means :
Def2:
:: FUNCT_4:def 2
( ( for
x being
set holds
(
x in dom it iff ex
y,
z being
set st
(
x = [z,y] &
[y,z] in dom f ) ) ) & ( for
y,
z being
set st
[y,z] in dom f holds
it . z,
y = f . y,
z ) );
existence
ex b1 being Function st
( ( for x being set holds
( x in dom b1 iff ex y, z being set st
( x = [z,y] & [y,z] in dom f ) ) ) & ( for y, z being set st [y,z] in dom f holds
b1 . z,y = f . y,z ) )
uniqueness
for b1, b2 being Function st ( for x being set holds
( x in dom b1 iff ex y, z being set st
( x = [z,y] & [y,z] in dom f ) ) ) & ( for y, z being set st [y,z] in dom f holds
b1 . z,y = f . y,z ) & ( for x being set holds
( x in dom b2 iff ex y, z being set st
( x = [z,y] & [y,z] in dom f ) ) ) & ( for y, z being set st [y,z] in dom f holds
b2 . z,y = f . y,z ) holds
b1 = b2
end;
:: deftheorem Def2 defines ~ FUNCT_4:def 2 :
theorem Th42: :: FUNCT_4:42
theorem Th43: :: FUNCT_4:43
theorem :: FUNCT_4:44
theorem :: FUNCT_4:45
theorem Th46: :: FUNCT_4:46
theorem Th47: :: FUNCT_4:47
theorem Th48: :: FUNCT_4:48
theorem :: FUNCT_4:49
theorem Th50: :: FUNCT_4:50
theorem :: FUNCT_4:51
theorem Th52: :: FUNCT_4:52
theorem Th53: :: FUNCT_4:53
theorem :: FUNCT_4:54
theorem :: FUNCT_4:55
canceled;
theorem :: FUNCT_4:56
canceled;
definition
let f,
g be
Function;
func |:f,g:| -> Function means :
Def3:
:: FUNCT_4:def 3
( ( for
z being
set holds
(
z in dom it iff ex
x,
y,
x',
y' being
set st
(
z = [[x,x'],[y,y']] &
[x,y] in dom f &
[x',y'] in dom g ) ) ) & ( for
x,
y,
x',
y' being
set st
[x,y] in dom f &
[x',y'] in dom g holds
it . [x,x'],
[y,y'] = [(f . x,y),(g . x',y')] ) );
existence
ex b1 being Function st
( ( for z being set holds
( z in dom b1 iff ex x, y, x', y' being set st
( z = [[x,x'],[y,y']] & [x,y] in dom f & [x',y'] in dom g ) ) ) & ( for x, y, x', y' being set st [x,y] in dom f & [x',y'] in dom g holds
b1 . [x,x'],[y,y'] = [(f . x,y),(g . x',y')] ) )
uniqueness
for b1, b2 being Function st ( for z being set holds
( z in dom b1 iff ex x, y, x', y' being set st
( z = [[x,x'],[y,y']] & [x,y] in dom f & [x',y'] in dom g ) ) ) & ( for x, y, x', y' being set st [x,y] in dom f & [x',y'] in dom g holds
b1 . [x,x'],[y,y'] = [(f . x,y),(g . x',y')] ) & ( for z being set holds
( z in dom b2 iff ex x, y, x', y' being set st
( z = [[x,x'],[y,y']] & [x,y] in dom f & [x',y'] in dom g ) ) ) & ( for x, y, x', y' being set st [x,y] in dom f & [x',y'] in dom g holds
b2 . [x,x'],[y,y'] = [(f . x,y),(g . x',y')] ) holds
b1 = b2
end;
:: deftheorem Def3 defines |: FUNCT_4:def 3 :
for
f,
g,
b3 being
Function holds
(
b3 = |:f,g:| iff ( ( for
z being
set holds
(
z in dom b3 iff ex
x,
y,
x',
y' being
set st
(
z = [[x,x'],[y,y']] &
[x,y] in dom f &
[x',y'] in dom g ) ) ) & ( for
x,
y,
x',
y' being
set st
[x,y] in dom f &
[x',y'] in dom g holds
b3 . [x,x'],
[y,y'] = [(f . x,y),(g . x',y')] ) ) );
theorem Th57: :: FUNCT_4:57
for
x,
x',
y,
y' being
set for
f,
g being
Function holds
(
[[x,x'],[y,y']] in dom |:f,g:| iff (
[x,y] in dom f &
[x',y'] in dom g ) )
theorem :: FUNCT_4:58
for
x,
x',
y,
y' being
set for
f,
g being
Function st
[[x,x'],[y,y']] in dom |:f,g:| holds
|:f,g:| . [x,x'],
[y,y'] = [(f . x,y),(g . x',y')]
theorem Th59: :: FUNCT_4:59
theorem Th60: :: FUNCT_4:60
for
X,
Y,
X',
Y' being
set for
f,
g being
Function st
dom f c= [:X,Y:] &
dom g c= [:X',Y':] holds
dom |:f,g:| c= [:[:X,X':],[:Y,Y':]:]
theorem Th61: :: FUNCT_4:61
for
X,
Y,
X',
Y' being
set for
f,
g being
Function st
dom f = [:X,Y:] &
dom g = [:X',Y':] holds
dom |:f,g:| = [:[:X,X':],[:Y,Y':]:]
theorem :: FUNCT_4:62
for
X,
Y,
Z,
X',
Y',
Z' being
set for
f being
PartFunc of
[:X,Y:],
Z for
g being
PartFunc of
[:X',Y':],
Z' holds
|:f,g:| is
PartFunc of
[:[:X,X':],[:Y,Y':]:],
[:Z,Z':]
theorem Th63: :: FUNCT_4:63
for
X,
Y,
Z,
X',
Y',
Z' being
set for
f being
Function of
[:X,Y:],
Z for
g being
Function of
[:X',Y':],
Z' st
Z <> {} &
Z' <> {} holds
|:f,g:| is
Function of
[:[:X,X':],[:Y,Y':]:],
[:Z,Z':]
theorem :: FUNCT_4:64
for
X,
Y,
X',
Y' being
set for
D,
D' being non
empty set for
f being
Function of
[:X,Y:],
D for
g being
Function of
[:X',Y':],
D' holds
|:f,g:| is
Function of
[:[:X,X':],[:Y,Y':]:],
[:D,D':] by Th63;
:: deftheorem defines --> FUNCT_4:def 4 :
theorem Th65: :: FUNCT_4:65
theorem Th66: :: FUNCT_4:66
for
x1,
x2,
y1,
y2 being
set holds
( (
x1 <> x2 implies
(x1,x2 --> y1,y2) . x1 = y1 ) &
(x1,x2 --> y1,y2) . x2 = y2 )
theorem :: FUNCT_4:67
for
x1,
x2,
y1,
y2 being
set st
x1 <> x2 holds
rng (x1,x2 --> y1,y2) = {y1,y2}
theorem :: FUNCT_4:68
definition
let A be non
empty set ;
let x1,
x2 be
set ;
let y1,
y2 be
Element of
A;
:: original: -->redefine func x1,
x2 --> y1,
y2 -> Function of
{x1,x2},
A;
coherence
x1,x2 --> y1,y2 is Function of {x1,x2},A
end;
theorem :: FUNCT_4:69
theorem :: FUNCT_4:70
canceled;
theorem Th71: :: FUNCT_4:71
theorem :: FUNCT_4:72
for
a,
b,
x,
y,
x',
y' being
set st
a <> b &
a,
b --> x,
y = a,
b --> x',
y' holds
(
x = x' &
y = y' )
theorem :: FUNCT_4:73
theorem Th74: :: FUNCT_4:74
theorem Th75: :: FUNCT_4:75
theorem Th76: :: FUNCT_4:76
theorem :: FUNCT_4:77
theorem :: FUNCT_4:78
theorem Th79: :: FUNCT_4:79
theorem :: FUNCT_4:80
theorem :: FUNCT_4:81
theorem :: FUNCT_4:82
theorem :: FUNCT_4:83
theorem :: FUNCT_4:84
theorem :: FUNCT_4:85
theorem :: FUNCT_4:86
theorem :: FUNCT_4:87
theorem :: FUNCT_4:88
theorem :: FUNCT_4:89
theorem Th90: :: FUNCT_4:90
theorem :: FUNCT_4:91
theorem :: FUNCT_4:92
theorem :: FUNCT_4:93
theorem :: FUNCT_4:94
theorem :: FUNCT_4:95
theorem :: FUNCT_4:96
theorem :: FUNCT_4:97
theorem :: FUNCT_4:98
theorem :: FUNCT_4:99
theorem :: FUNCT_4:100
theorem :: FUNCT_4:101
theorem Th102: :: FUNCT_4:102
theorem :: FUNCT_4:103
theorem Th104: :: FUNCT_4:104
:: deftheorem defines +~ FUNCT_4:def 5 :
theorem Th105: :: FUNCT_4:105
theorem Th106: :: FUNCT_4:106
theorem :: FUNCT_4:107
theorem Th108: :: FUNCT_4:108
theorem Th109: :: FUNCT_4:109
theorem :: FUNCT_4:110
theorem :: FUNCT_4:111
theorem :: FUNCT_4:112
theorem :: FUNCT_4:113
canceled;
theorem :: FUNCT_4:114
canceled;
theorem :: FUNCT_4:115
theorem :: FUNCT_4:116
theorem :: FUNCT_4:117
theorem :: FUNCT_4:118