:: Binary Operations Applied to Functions :: by Andrzej Trybulec :: :: Received September 4, 1989 :: Copyright (c) 1990-2018 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; 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}; 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;