:: Basic Functions and Operations on Functions
:: by Czes{\l}aw Byli\'nski
::
:: Received May 9, 1989
:: Copyright (c) 1990 Association of Mizar Users
theorem Th1: :: FUNCT_3:1
theorem Th2: :: FUNCT_3:2
theorem Th3: :: FUNCT_3:3
theorem Th4: :: FUNCT_3:4
theorem Th5: :: FUNCT_3:5
scheme :: FUNCT_3:sch 1
FuncEx3{
F1()
-> set ,
F2()
-> set ,
P1[
set ,
set ,
set ] } :
ex
f being
Function st
(
dom f = [:F1(),F2():] & ( for
x,
y being
set st
x in F1() &
y in F2() holds
P1[
x,
y,
f . x,
y] ) )
provided
A1:
for
x,
y,
z1,
z2 being
set st
x in F1() &
y in F2() &
P1[
x,
y,
z1] &
P1[
x,
y,
z2] holds
z1 = z2
and A2:
for
x,
y being
set st
x in F1() &
y in F2() holds
ex
z being
set st
P1[
x,
y,
z]
theorem Th6: :: FUNCT_3:6
:: deftheorem Def1 defines .: FUNCT_3:def 1 :
theorem :: FUNCT_3:7
canceled;
theorem Th8: :: FUNCT_3:8
theorem :: FUNCT_3:9
theorem Th10: :: FUNCT_3:10
theorem :: FUNCT_3:11
canceled;
theorem :: FUNCT_3:12
theorem Th13: :: FUNCT_3:13
theorem :: FUNCT_3:14
theorem Th15: :: FUNCT_3:15
theorem Th16: :: FUNCT_3:16
theorem :: FUNCT_3:17
theorem Th18: :: FUNCT_3:18
theorem :: FUNCT_3:19
theorem :: FUNCT_3:20
theorem Th21: :: FUNCT_3:21
theorem Th22: :: FUNCT_3:22
:: deftheorem Def2 defines " FUNCT_3:def 2 :
theorem :: FUNCT_3:23
canceled;
theorem Th24: :: FUNCT_3:24
theorem Th25: :: FUNCT_3:25
theorem :: FUNCT_3:26
canceled;
theorem :: FUNCT_3:27
theorem :: FUNCT_3:28
theorem Th29: :: FUNCT_3:29
theorem :: FUNCT_3:30
theorem Th31: :: FUNCT_3:31
theorem :: FUNCT_3:32
theorem Th33: :: FUNCT_3:33
theorem :: FUNCT_3:34
theorem Th35: :: FUNCT_3:35
theorem Th36: :: FUNCT_3:36
theorem :: FUNCT_3:37
theorem :: FUNCT_3:38
theorem :: FUNCT_3:39
:: deftheorem Def3 defines chi FUNCT_3:def 3 :
for
A,
X being
set for
b3 being
Function holds
(
b3 = chi A,
X iff (
dom b3 = X & ( for
x being
set st
x in X holds
( (
x in A implies
b3 . x = 1 ) & ( not
x in A implies
b3 . x = {} ) ) ) ) );
theorem :: FUNCT_3:40
canceled;
theorem :: FUNCT_3:41
canceled;
theorem Th42: :: FUNCT_3:42
for
x,
A,
X being
set st
(chi A,X) . x = 1 holds
x in A
theorem :: FUNCT_3:43
theorem :: FUNCT_3:44
canceled;
theorem :: FUNCT_3:45
canceled;
theorem :: FUNCT_3:46
canceled;
theorem :: FUNCT_3:47
theorem Th48: :: FUNCT_3:48
theorem :: FUNCT_3:49
theorem :: FUNCT_3:50
canceled;
theorem :: FUNCT_3:51
canceled;
theorem :: FUNCT_3:52
canceled;
theorem :: FUNCT_3:53
theorem :: FUNCT_3:54
canceled;
theorem :: FUNCT_3:55
canceled;
theorem :: FUNCT_3:56
definition
let X,
Y be
set ;
canceled;func pr1 X,
Y -> Function means :
Def5:
:: FUNCT_3:def 5
(
dom it = [:X,Y:] & ( for
x,
y being
set st
x in X &
y in Y holds
it . x,
y = x ) );
existence
ex b1 being Function st
( dom b1 = [:X,Y:] & ( for x, y being set st x in X & y in Y holds
b1 . x,y = x ) )
uniqueness
for b1, b2 being Function st dom b1 = [:X,Y:] & ( for x, y being set st x in X & y in Y holds
b1 . x,y = x ) & dom b2 = [:X,Y:] & ( for x, y being set st x in X & y in Y holds
b2 . x,y = x ) holds
b1 = b2
func pr2 X,
Y -> Function means :
Def6:
:: FUNCT_3:def 6
(
dom it = [:X,Y:] & ( for
x,
y being
set st
x in X &
y in Y holds
it . x,
y = y ) );
existence
ex b1 being Function st
( dom b1 = [:X,Y:] & ( for x, y being set st x in X & y in Y holds
b1 . x,y = y ) )
uniqueness
for b1, b2 being Function st dom b1 = [:X,Y:] & ( for x, y being set st x in X & y in Y holds
b1 . x,y = y ) & dom b2 = [:X,Y:] & ( for x, y being set st x in X & y in Y holds
b2 . x,y = y ) holds
b1 = b2
end;
:: deftheorem FUNCT_3:def 4 :
canceled;
:: deftheorem Def5 defines pr1 FUNCT_3:def 5 :
:: deftheorem Def6 defines pr2 FUNCT_3:def 6 :
theorem :: FUNCT_3:57
canceled;
theorem :: FUNCT_3:58
canceled;
theorem Th59: :: FUNCT_3:59
theorem :: FUNCT_3:60
theorem Th61: :: FUNCT_3:61
theorem :: FUNCT_3:62
definition
let X,
Y be
set ;
:: original: pr1redefine func pr1 X,
Y -> Function of
[:X,Y:],
X;
coherence
pr1 X,Y is Function of [:X,Y:],X
:: original: pr2redefine func pr2 X,
Y -> Function of
[:X,Y:],
Y;
coherence
pr2 X,Y is Function of [:X,Y:],Y
end;
:: deftheorem Def7 defines delta FUNCT_3:def 7 :
theorem :: FUNCT_3:63
canceled;
theorem :: FUNCT_3:64
canceled;
theorem :: FUNCT_3:65
canceled;
theorem Th66: :: FUNCT_3:66
:: deftheorem Def8 defines <: FUNCT_3:def 8 :
theorem :: FUNCT_3:67
canceled;
theorem Th68: :: FUNCT_3:68
theorem Th69: :: FUNCT_3:69
theorem Th70: :: FUNCT_3:70
theorem Th71: :: FUNCT_3:71
theorem Th72: :: FUNCT_3:72
theorem Th73: :: FUNCT_3:73
theorem Th74: :: FUNCT_3:74
theorem :: FUNCT_3:75
theorem :: FUNCT_3:76
theorem :: FUNCT_3:77
theorem Th78: :: FUNCT_3:78
theorem :: FUNCT_3:79
theorem :: FUNCT_3:80
theorem Th81: :: FUNCT_3:81
theorem :: FUNCT_3:82
theorem :: FUNCT_3:83
theorem :: FUNCT_3:84
definition
let f,
g be
Function;
func [:f,g:] -> Function means :
Def9:
:: FUNCT_3:def 9
(
dom it = [:(dom f),(dom g):] & ( for
x,
y being
set st
x in dom f &
y in dom g holds
it . x,
y = [(f . x),(g . y)] ) );
existence
ex b1 being Function st
( dom b1 = [:(dom f),(dom g):] & ( for x, y being set st x in dom f & y in dom g holds
b1 . x,y = [(f . x),(g . y)] ) )
uniqueness
for b1, b2 being Function st dom b1 = [:(dom f),(dom g):] & ( for x, y being set st x in dom f & y in dom g holds
b1 . x,y = [(f . x),(g . y)] ) & dom b2 = [:(dom f),(dom g):] & ( for x, y being set st x in dom f & y in dom g holds
b2 . x,y = [(f . x),(g . y)] ) holds
b1 = b2
end;
:: deftheorem Def9 defines [: FUNCT_3:def 9 :
theorem :: FUNCT_3:85
canceled;
theorem Th86: :: FUNCT_3:86
theorem Th87: :: FUNCT_3:87
theorem Th88: :: FUNCT_3:88
theorem Th89: :: FUNCT_3:89
theorem :: FUNCT_3:90
theorem :: FUNCT_3:91
theorem :: FUNCT_3:92
theorem :: FUNCT_3:93
theorem :: FUNCT_3:94
theorem Th95: :: FUNCT_3:95
definition
let X1,
X2,
Y1,
Y2 be
set ;
let f1 be
Function of
X1,
Y1;
let f2 be
Function of
X2,
Y2;
:: original: [:redefine func [:f1,f2:] -> Function of
[:X1,X2:],
[:Y1,Y2:];
coherence
[:f1,f2:] is Function of [:X1,X2:],[:Y1,Y2:]
by Th95;
end;
theorem :: FUNCT_3:96
theorem :: FUNCT_3:97
theorem :: FUNCT_3:98
theorem :: FUNCT_3:99
theorem :: FUNCT_3:100