:: Binary Operations Applied to Functions
:: by Andrzej Trybulec
::
:: Received September 4, 1989
:: Copyright (c) 1990-2019 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies FUNCT_1, FUNCT_3, PARTFUN1, RELAT_1, ZFMISC_1, XBOOLE_0, TARSKI,
SUBSET_1, BINOP_1, MCART_1, FUNCOP_1, WELLORD1, MSUALG_4, FUNCT_2;
notations TARSKI, XBOOLE_0, ZFMISC_1, XTUPLE_0, SUBSET_1, MCART_1, RELAT_1,
FUNCT_1, RELSET_1, PARTFUN1, FUNCT_2, FUNCT_3, BINOP_1, WELLORD1;
constructors PARTFUN1, BINOP_1, FUNCT_3, RELSET_1, WELLORD1, XTUPLE_0;
registrations XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1, FUNCT_2, RELSET_1,
FUNCT_3;
requirements SUBSET, BOOLE;
begin
reserve f,g,h for Function,
A for set;
theorem :: FUNCOP_1:1
delta A = <:id A, id A:>;
reserve F for Function,
B,x,y,y1,y2,z for set;
definition
let f;
func f~ -> Function means
:: FUNCOP_1:def 1
dom it = dom f & for x being object st x in dom f holds
(for y,z being object st f.x = [y,z] holds it.x = [z,y]) &
(f.x = it.x or ex y,z being object st f.x =[y,z]);
involutiveness;
end;
theorem :: FUNCOP_1:2
<:f,g:> = <:g,f:>~;
theorem :: FUNCOP_1:3
(f|A)~ = f~|A;
theorem :: FUNCOP_1:4
(delta A)~ = delta A;
theorem :: FUNCOP_1:5
<:f,g:>|A = <:f|A,g:>;
theorem :: FUNCOP_1:6
<:f,g:>|A = <:f,g|A:>;
definition
let A be set, z be object;
func A --> z -> set equals
:: FUNCOP_1:def 2
[:A, {z}:];
end;
registration
let A be set, z be object;
cluster A --> z -> Function-like Relation-like;
end;
reserve x,z for object;
theorem :: FUNCOP_1:7
x in A implies (A --> z).x = z;
registration
let A be non empty set, x be object, a be Element of A;
reduce (A --> x).a to x;
end;
theorem :: FUNCOP_1:8
A <> {} implies rng (A --> x) = {x};
theorem :: FUNCOP_1:9
rng f = {x} implies f = (dom f) --> x;
registration
let x be object;
cluster {} --> x -> empty;
end;
registration
let x be object;
let A be empty set;
cluster A --> x -> empty;
end;
registration
let x be object;
let A be non empty set;
cluster A --> x -> non empty;
end;
theorem :: FUNCOP_1:10
dom ({} --> x) = {} & rng ({} --> x) = {};
theorem :: FUNCOP_1:11
(for z st z in dom f holds f.z = x) implies f = dom f --> x;
theorem :: FUNCOP_1:12
(A --> x)|B = A /\ B --> x;
theorem :: FUNCOP_1:13
dom (A --> x) = A & rng (A --> x) c= {x};
registration
let X be set, a be object;
reduce dom (X --> a) to X;
end;
registration let D be set;
cluster D --> {} -> empty-yielding;
end;
theorem :: FUNCOP_1:14
x in B implies (A --> x)"B = A;
theorem :: FUNCOP_1:15
(A --> x)"{x} = A;
theorem :: FUNCOP_1:16
not x in B implies (A --> x)"B = {};
theorem :: FUNCOP_1:17
x in dom h implies h*(A --> x) = A --> h.x;
theorem :: FUNCOP_1:18
A <> {} & x in dom h implies dom(h*(A --> x)) <> {};
theorem :: FUNCOP_1:19
(A --> x)*h = h"A --> x;
theorem :: FUNCOP_1:20
(A --> [x,y])~ = A --> [y,x];
definition
let F,f,g;
func F.:(f,g) -> set equals
:: FUNCOP_1:def 3
F * <:f,g:>;
end;
registration
let F,f,g;
cluster F.:(f,g) -> Function-like Relation-like;
end;
theorem :: FUNCOP_1:21
for h st dom h = dom(F.:(f,g)) & for z being set st z in dom (F.:(f,g)
) holds h.z = F.(f.z,g.z) holds h = F.:(f,g);
theorem :: FUNCOP_1:22
x in dom (F.:(f,g)) implies (F.:(f,g)).x = F.(f.x,g.x);
theorem :: FUNCOP_1:23
f|A = g|A implies (F.:(f,h))|A = (F.:(g,h))|A;
theorem :: FUNCOP_1:24
f|A = g|A implies (F.:(h,f))|A = (F.:(h,g))|A;
theorem :: FUNCOP_1:25
F.:(f,g)*h = F.:(f*h, g*h);
definition
let F,f,x;
func F[:](f,x) -> set equals
:: FUNCOP_1:def 4
F * <:f, dom f --> x:>;
end;
registration
let F,f,x;
cluster F[:](f,x) -> Function-like Relation-like;
end;
theorem :: FUNCOP_1:26
F[:](f,x) = F.:(f, dom f --> x);
theorem :: FUNCOP_1:27
x in dom (F[:](f,z)) implies (F[:](f,z)).x = F.(f.x,z);
theorem :: FUNCOP_1:28
f|A = g|A implies (F[:](f,x))|A = (F[:](g,x))|A;
theorem :: FUNCOP_1:29
F[:](f,x)*h = F[:](f*h,x);
theorem :: FUNCOP_1:30
F[:](f,x)*id A = F[:](f|A,x);
definition
let F,x,g;
func F[;](x,g) -> set equals
:: FUNCOP_1:def 5
F * <:dom g --> x, g:>;
end;
registration
let F,x,g;
cluster F[;](x,g) -> Function-like Relation-like;
end;
theorem :: FUNCOP_1:31
F[;](x,g) = F.:(dom g --> x, g);
theorem :: FUNCOP_1:32
x in dom (F[;](z,f)) implies (F[;](z,f)).x = F.(z,f.x);
theorem :: FUNCOP_1:33
f|A = g|A implies (F[;](x,f))|A = (F[;](x,g))|A;
theorem :: FUNCOP_1:34
F[;](x,f)*h = F[;](x,f*h);
theorem :: FUNCOP_1:35
F[;](x,f)*id A = F[;](x,f|A);
reserve X for non empty set,
Y for set,
F for BinOp of X,
f,g,h for Function of Y,X,
x,x1,x2 for Element of X;
theorem :: FUNCOP_1:36
F.:(f,g) is Function of Y,X;
definition
let X be non empty set, Z be set;
let F be BinOp of X, f,g be Function of Z,X;
redefine func F.:(f,g) -> Function of Z,X;
end;
reserve Y for non empty set,
F for BinOp of X,
f,g,h for Function of Y,X,
x,x1,x2 for Element of X;
theorem :: FUNCOP_1:37
for z being Element of Y holds (F.:(f,g)).z = F.(f.z,g.z);
theorem :: FUNCOP_1:38
for h being Function of Y,X holds (for z being Element of Y
holds h.z = F.(f.z,g.z)) implies h = F.:(f,g);
theorem :: FUNCOP_1:39
for g being Function of X,X holds F.:(id X, g)*f = F.:(f,g*f);
theorem :: FUNCOP_1:40
for g being Function of X,X holds F.:(g, id X)*f = F.:(g*f,f);
theorem :: FUNCOP_1:41
F.:(id X, id X)*f = F.:(f,f);
theorem :: FUNCOP_1:42
for g being Function of X,X holds F.:(id X, g).x = F.(x,g.x);
theorem :: FUNCOP_1:43
for g being Function of X,X holds F.:(g, id X).x = F.(g.x,x);
theorem :: FUNCOP_1:44
F.:(id X, id X).x = F.(x,x);
theorem :: FUNCOP_1:45
x in B implies A --> x is Function of A,B;
definition
let I be set, i be object;
redefine func I --> i -> Function of I,{i};
end;
definition
let B be non empty set, A be set, b be Element of B;
redefine func A --> b -> Function of A,B;
end;
theorem :: FUNCOP_1:46
A --> x is Function of A,X;
reserve Y for set,
F for BinOp of X,
f,g,h for Function of Y,X,
x,x1,x2 for Element of X;
theorem :: FUNCOP_1:47
F[:](f,x) is Function of Y,X;
definition
let X be non empty set, Z be set;
let F be BinOp of X, f be Function of Z,X, x be Element of X;
redefine func F[:](f,x) -> Function of Z,X;
end;
reserve Y for non empty set,
F for BinOp of X,
f,g,h for Function of Y,X,
x,x1,x2 for Element of X;
theorem :: FUNCOP_1:48
for y being Element of Y holds (F[:](f,x)).y = F.(f.y,x);
theorem :: FUNCOP_1:49
(for y being Element of Y holds g.y = F.(f.y,x)) implies g = F
[:](f,x);
theorem :: FUNCOP_1:50
F[:](id X, x)*f = F[:](f,x);
theorem :: FUNCOP_1:51
F[:](id X, x).x = F.(x,x);
reserve Y for set,
F for BinOp of X,
f,g,h for Function of Y,X,
x,x1,x2 for Element of X;
theorem :: FUNCOP_1:52
F[;](x,g) is Function of Y,X;
definition
let X be non empty set, Z be set;
let F be BinOp of X, x be Element of X;
let g be Function of Z,X;
redefine func F[;](x,g) -> Function of Z,X;
end;
reserve Y for non empty set,
F for BinOp of X,
f,g,h for Function of Y,X,
x,x1,x2 for Element of X;
theorem :: FUNCOP_1:53
for y being Element of Y holds (F[;](x,f)).y = F.(x,f.y);
theorem :: FUNCOP_1:54
(for y being Element of Y holds g.y = F.(x,f.y)) implies g = F
[;](x,f);
reserve Y for set,
F for BinOp of X,
f,g,h for Function
of Y,X,
x,x1,x2 for Element of X;
theorem :: FUNCOP_1:55
F[;](x, id X)*f = F[;](x,f);
theorem :: FUNCOP_1:56
F[;](x, id X).x = F.(x,x);
theorem :: FUNCOP_1:57
for X,Y,Z being non empty set for f being Function of X, [:Y,Z:] for x
being Element of X holds f~.x =[(f.x)`2,(f.x)`1];
definition
let X,Y,Z be non empty set;
let f be Function of X, [:Y,Z:];
redefine func rng f -> Relation of Y,Z;
end;
definition
let X,Y,Z be non empty set;
let f be Function of X, [:Y,Z:];
redefine func f~ -> Function of X, [:Z,Y:];
end;
theorem :: FUNCOP_1:58
for X,Y,Z being non empty set for f being Function of X, [:Y,Z:] holds
rng (f~) = (rng f)~;
reserve y for Element of Y;
theorem :: FUNCOP_1:59
F is associative implies F[:](F[;](x1,f),x2) = F[;](x1,F[:](f,x2));
theorem :: FUNCOP_1:60
F is associative implies F.:(F[:](f,x),g) = F.:(f,F[;](x,g));
theorem :: FUNCOP_1:61
F is associative implies F.:(F.:(f,g),h) = F.:(f,F.:(g,h));
theorem :: FUNCOP_1:62
F is associative implies F[;](F.(x1,x2),f) = F[;](x1,F[;](x2,f));
theorem :: FUNCOP_1:63
F is associative implies F[:](f, F.(x1,x2)) = F[:](F[:](f,x1),x2);
theorem :: FUNCOP_1:64
F is commutative implies F[;](x,f) = F[:](f,x);
theorem :: FUNCOP_1:65
F is commutative implies F.:(f,g) = F.:(g,f);
theorem :: FUNCOP_1:66
F is idempotent implies F.:(f,f) = f;
reserve Y for non empty set,
F for BinOp of X,
f for Function of Y,X,
x for Element of X,
y for Element of Y;
theorem :: FUNCOP_1:67
F is idempotent implies F[;](f.y,f).y = f.y;
theorem :: FUNCOP_1:68
F is idempotent implies F[:](f,f.y).y = f.y;
:: Addendum, 2002.07.08
theorem :: FUNCOP_1:69
for F,f,g being Function st [:rng f, rng g:] c= dom F holds dom(F.:(f,
g)) = dom f /\ dom g;
:: from PRALG_1, 2004.07.23
definition
let IT be Function;
attr IT is Function-yielding means
:: FUNCOP_1:def 6
for x being object st x in dom IT holds IT.x is Function;
end;
registration
cluster Function-yielding for Function;
end;
registration
let B be Function-yielding Function, j be object;
cluster B.j -> Function-like Relation-like;
end;
registration
let F be Function-yielding Function, f be Function;
cluster F * f -> Function-yielding;
end;
:: missing, 2005.11.13, A.T.
registration
let B;
let c be non empty set;
cluster B --> c -> non-empty;
end;
:: missing, 2005.12.20, A.T.
theorem :: FUNCOP_1:70
([:X,Y:] --> z).(x,y) = z;
:: from CAT_1, 2007.02.11, A.T.
reserve a,b,c for set;
definition
let a,b,c be object;
func (a,b).-->c -> Function equals
:: FUNCOP_1:def 7
{[a,b]} --> c;
end;
theorem :: FUNCOP_1:71
for a,b,c being object holds
((a,b).-->c).(a,b) = c;
:: from CQC_LANG, 2007.03.13, A.T.
definition
let x,y,a,b be object;
func IFEQ(x,y,a,b) -> object equals
:: FUNCOP_1:def 8
a if x = y otherwise b;
end;
definition
let x,y be object; let a,b be set;
redefine func IFEQ(x,y,a,b) -> set;
end;
definition
let D be set;
let x,y be object, a,b be Element of D;
redefine func IFEQ(x,y,a,b) -> Element of D;
end;
definition
let x,y be object;
func x .--> y -> set equals
:: FUNCOP_1:def 9
{x} --> y;
end;
registration
let x,y be object;
cluster x .--> y -> Function-like Relation-like;
end;
registration
let x,y be object;
cluster x .--> y -> one-to-one;
end;
theorem :: FUNCOP_1:72
for x,y be object holds (x .--> y).x = y;
:: from SCMFSA6A, 2007.07.22, A.T.
theorem :: FUNCOP_1:73
for a,b being object, f being Function holds a.-->b c= f iff a in dom f &
f.a = b;
:: from FUNCT_2, 2007.11.22, A.T., :: from CAT_4
notation
let o,m,r be object;
synonym (o,m) :-> r for (o,m) .--> r;
end;
definition
let o,m,r be object;
redefine func (o,m) :-> r -> Function of [:{o},{m}:],{r} means
:: FUNCOP_1:def 10
not contradiction;
end;
:: missing, 2008.03.20, A.T.
reserve x,y,z for object;
theorem :: FUNCOP_1:74
x in dom(x .--> y);
theorem :: FUNCOP_1:75
z in dom(x .--> y) implies z = x;
:: missing, 2008.04.15, A.T.
theorem :: FUNCOP_1:76
not x in A implies (x .--> y)|A = {};
:: from CAT_1, (new notation), 2008.06.30. A.T.
notation
let x,y be object;
synonym x :-> y for x .--> y;
end;
definition
let m,o be object;
redefine func m :-> o -> Function of {m}, {o};
end;
theorem :: FUNCOP_1:77
for x being Element of {a} for y being Element of {b} holds
((a,b):->c).(x,y) = c;
:: from MSUHOM_1, ALTCAT_1, 2008.07.06, A.T.
registration
let f be Function-yielding Function, C be set;
cluster f|C -> Function-yielding;
end;
:: from CIRCCOMB, 2008.07.06, A.T.
registration
let A be set;
let f be Function;
cluster A --> f -> Function-yielding;
end;
:: from SEQM_3, 2008.07.17, A.T.
registration
let X be set, a be object;
cluster X --> a -> constant;
end;
:: from YELLOW_6, 2008.07.17, A.T.
registration
cluster non empty constant for Function;
let X be set, Y be non empty set;
cluster constant for Function of X,Y;
end;
:: missing, 2008.07.17, A.T.
registration
let f be constant Function, X be set;
cluster f|X -> constant;
end;
:: missing, 2008.08.14, A.T.
theorem :: FUNCOP_1:78
for f being non empty constant Function ex y st for x st x in dom f
holds f.x = y;
:: from YELLOW_6, 2008.12.26, A.T.
theorem :: FUNCOP_1:79
for X being non empty set, x being set holds the_value_of (X --> x) =
x;
:: from CIRCCMB3, 2008.12.26, A.T.
theorem :: FUNCOP_1:80
for f being constant Function holds f = (dom f) --> the_value_of f;
:: missing, 2009.01.21, A.T.
registration
let X be set, Y be non empty set;
cluster total for PartFunc of X,Y;
end;
:: new, 2009.02.14, A.T.
registration
let I be set, A be object;
cluster I --> A -> I-defined;
end;
registration
let I, A be object;
cluster I .--> A -> {I}-defined;
end;
:: BORSUK_1:6, 2009.06.11, A.K.
theorem :: FUNCOP_1:81
(A --> x).:B c= {x};
registration
let I be set, f be Function;
cluster I .--> f -> Function-yielding;
end;
:: 2009.10.03, A.T.
registration let I be set;
cluster total for I-defined non-empty Function;
end;
theorem :: FUNCOP_1:82
x .--> y is_isomorphism_of {[x,x]},{[y,y]};
theorem :: FUNCOP_1:83
{[x,x]}, {[y,y]} are_isomorphic;
registration
let I be set, A be object;
cluster I --> A -> total for I-defined Function;
end;
theorem :: FUNCOP_1:84
for f being Function st x in dom f
holds x .--> f.x c= f;
registration let A be non empty set;
let x be set, i be Element of A;
cluster x .--> i -> A-valued;
end;
reserve Y for set,
f,g for Function of Y,X,
x for Element of X,
y for Element of Y;
:: missing, 2010.02.10, A.T.
theorem :: FUNCOP_1:85
F is associative implies F.:(F[;](x,f),g) = F[;](x,F.:(f,g));
registration let A be set, B be non empty set, x be Element of B;
cluster A --> x -> B-valued;
end;
registration let A be non empty set, x be Element of A, y be object;
cluster x .--> y -> A-defined;
end;
theorem :: FUNCOP_1:86
for x,y,A being set st x in A
holds (x .--> y)|A = x .--> y;
:: missing, 2011.02.06, A.K.
registration
let Y be functional set;
cluster Y-valued -> Function-yielding for Function;
end;
:: from MSUALG_4, 2011.04.16, A.T.
definition
let IT be Function;
attr IT is Relation-yielding means
:: FUNCOP_1:def 11
for x be set st x in dom IT holds IT.x is Relation;
end;
registration
cluster Function-yielding -> Relation-yielding for Function;
end;
registration
cluster empty -> Function-yielding for Function;
end;
:: from CIRCCOMB, 2011.04.19, A.T.
theorem :: FUNCOP_1:87
for X,Y being set, x,y being object
holds X --> x tolerates Y --> y iff x = y or X misses Y;
reserve x,y,z,A for set;
theorem :: FUNCOP_1:88
rng(x .--> y) = {y};
theorem :: FUNCOP_1:89
z in A implies (A --> x)*(y .--> z) = y .--> x;
registration
let f be Function-yielding Function;
let a,b be object;
cluster f.(a,b) -> Function-like Relation-like;
end;
registration
let Y be set;
let X,Z be non empty set;
cluster -> Function-yielding for Function of X, Funcs(Y,Z);
end;