:: Binary Operations Applied to Functions
:: by Andrzej Trybulec
::
:: Received September 4, 1989
:: Copyright (c) 1990 Association of Mizar Users
theorem :: FUNCOP_1:1
canceled;
theorem Th2: :: FUNCOP_1:2
definition
let f be
Function;
func f ~ -> Function means :
Def1:
:: FUNCOP_1:def 1
(
dom it = dom f & ( for
x being
set st
x in dom f holds
( ( for
y,
z being
set st
f . x = [y,z] holds
it . x = [z,y] ) & (
f . x = it . x or ex
y,
z being
set st
f . x = [y,z] ) ) ) );
existence
ex b1 being Function st
( dom b1 = dom f & ( for x being set st x in dom f holds
( ( for y, z being set st f . x = [y,z] holds
b1 . x = [z,y] ) & ( f . x = b1 . x or ex y, z being set st f . x = [y,z] ) ) ) )
uniqueness
for b1, b2 being Function st dom b1 = dom f & ( for x being set st x in dom f holds
( ( for y, z being set st f . x = [y,z] holds
b1 . x = [z,y] ) & ( f . x = b1 . x or ex y, z being set st f . x = [y,z] ) ) ) & dom b2 = dom f & ( for x being set st x in dom f holds
( ( for y, z being set st f . x = [y,z] holds
b2 . x = [z,y] ) & ( f . x = b2 . x or ex y, z being set st f . x = [y,z] ) ) ) holds
b1 = b2
involutiveness
for b1, b2 being Function st dom b1 = dom b2 & ( for x being set st x in dom b2 holds
( ( for y, z being set st b2 . x = [y,z] holds
b1 . x = [z,y] ) & ( b2 . x = b1 . x or ex y, z being set st b2 . x = [y,z] ) ) ) holds
( dom b2 = dom b1 & ( for x being set st x in dom b1 holds
( ( for y, z being set st b1 . x = [y,z] holds
b2 . x = [z,y] ) & ( b1 . x = b2 . x or ex y, z being set st b1 . x = [y,z] ) ) ) )
end;
:: deftheorem Def1 defines ~ FUNCOP_1:def 1 :
for
f,
b2 being
Function holds
(
b2 = f ~ iff (
dom b2 = dom f & ( for
x being
set st
x in dom f holds
( ( for
y,
z being
set st
f . x = [y,z] holds
b2 . x = [z,y] ) & (
f . x = b2 . x or ex
y,
z being
set st
f . x = [y,z] ) ) ) ) );
theorem :: FUNCOP_1:3
canceled;
theorem :: FUNCOP_1:4
canceled;
theorem :: FUNCOP_1:5
canceled;
theorem Th6: :: FUNCOP_1:6
theorem Th7: :: FUNCOP_1:7
theorem :: FUNCOP_1:8
canceled;
theorem :: FUNCOP_1:9
theorem Th10: :: FUNCOP_1:10
theorem Th11: :: FUNCOP_1:11
:: deftheorem defines --> FUNCOP_1:def 2 :
theorem :: FUNCOP_1:12
canceled;
theorem Th13: :: FUNCOP_1:13
for
A,
x,
z being
set st
x in A holds
(A --> z) . x = z
theorem :: FUNCOP_1:14
theorem Th15: :: FUNCOP_1:15
theorem :: FUNCOP_1:16
theorem Th17: :: FUNCOP_1:17
theorem Th18: :: FUNCOP_1:18
theorem Th19: :: FUNCOP_1:19
theorem Th20: :: FUNCOP_1:20
for
A,
x,
B being
set st
x in B holds
(A --> x) " B = A
theorem :: FUNCOP_1:21
theorem :: FUNCOP_1:22
for
A,
x,
B being
set st not
x in B holds
(A --> x) " B = {}
theorem :: FUNCOP_1:23
theorem :: FUNCOP_1:24
theorem :: FUNCOP_1:25
theorem :: FUNCOP_1:26
:: deftheorem defines .: FUNCOP_1:def 3 :
Lm1:
for f, g, F being Function
for x being set st x in dom (F * <:f,g:>) holds
(F * <:f,g:>) . x = F . (f . x),(g . x)
theorem :: FUNCOP_1:27
theorem :: FUNCOP_1:28
theorem Th29: :: FUNCOP_1:29
theorem Th30: :: FUNCOP_1:30
theorem Th31: :: FUNCOP_1:31
:: deftheorem defines [:] FUNCOP_1:def 4 :
theorem :: FUNCOP_1:32
canceled;
theorem :: FUNCOP_1:33
canceled;
theorem :: FUNCOP_1:34
theorem Th35: :: FUNCOP_1:35
theorem :: FUNCOP_1:36
theorem Th37: :: FUNCOP_1:37
theorem :: FUNCOP_1:38
canceled;
theorem :: FUNCOP_1:39
:: deftheorem defines [;] FUNCOP_1:def 5 :
theorem :: FUNCOP_1:40
canceled;
theorem :: FUNCOP_1:41
theorem Th42: :: FUNCOP_1:42
theorem :: FUNCOP_1:43
theorem Th44: :: FUNCOP_1:44
theorem :: FUNCOP_1:45
canceled;
theorem :: FUNCOP_1:46
theorem Th47: :: FUNCOP_1:47
theorem Th48: :: FUNCOP_1:48
theorem Th49: :: FUNCOP_1:49
theorem :: FUNCOP_1:50
canceled;
theorem :: FUNCOP_1:51
theorem :: FUNCOP_1:52
theorem :: FUNCOP_1:53
theorem :: FUNCOP_1:54
theorem :: FUNCOP_1:55
theorem :: FUNCOP_1:56
theorem Th57: :: FUNCOP_1:57
theorem :: FUNCOP_1:58
theorem Th59: :: FUNCOP_1:59
theorem Th60: :: FUNCOP_1:60
theorem Th61: :: FUNCOP_1:61
theorem :: FUNCOP_1:62
canceled;
theorem :: FUNCOP_1:63
theorem :: FUNCOP_1:64
theorem Th65: :: FUNCOP_1:65
theorem Th66: :: FUNCOP_1:66
theorem Th67: :: FUNCOP_1:67
theorem :: FUNCOP_1:68
canceled;
theorem :: FUNCOP_1:69
theorem :: FUNCOP_1:70
theorem :: FUNCOP_1:71
theorem Th72: :: FUNCOP_1:72
theorem :: FUNCOP_1:73
theorem :: FUNCOP_1:74
theorem :: FUNCOP_1:75
theorem :: FUNCOP_1:76
theorem :: FUNCOP_1:77
theorem :: FUNCOP_1:78
theorem :: FUNCOP_1:79
theorem :: FUNCOP_1:80
theorem :: FUNCOP_1:81
theorem :: FUNCOP_1:82
theorem :: FUNCOP_1:83
theorem :: FUNCOP_1:84
:: deftheorem Def6 defines Function-yielding FUNCOP_1:def 6 :
theorem :: FUNCOP_1:85
:: deftheorem defines .--> FUNCOP_1:def 7 :
theorem :: FUNCOP_1:86
for
a,
b,
c being
set holds
(a,b .--> c) . a,
b = c
:: deftheorem Def8 defines IFEQ FUNCOP_1:def 8 :
for
x,
y,
a,
b being
set holds
( (
x = y implies
IFEQ x,
y,
a,
b = a ) & ( not
x = y implies
IFEQ x,
y,
a,
b = b ) );
:: deftheorem defines .--> FUNCOP_1:def 9 :
theorem Th87: :: FUNCOP_1:87
theorem :: FUNCOP_1:88
Lm2:
for o, m, r being set holds o,m :-> r is Function of [:{o},{m}:],{r}
definition
let o,
m,
r be
set ;
:: original: .-->redefine func o,
m :-> r -> Function of
[:{o},{m}:],
{r} means :: FUNCOP_1:def 10
verum;
coherence
o,m .--> r is Function of [:{o},{m}:],{r}
by Lm2;
compatibility
for b1 being Function of [:{o},{m}:],{r} holds
( b1 = o,m .--> r iff verum )
end;
:: deftheorem defines :-> FUNCOP_1:def 10 :
theorem :: FUNCOP_1:89
theorem :: FUNCOP_1:90
theorem :: FUNCOP_1:91
theorem :: FUNCOP_1:92
theorem :: FUNCOP_1:93