:: Graphs of Functions :: by Czes{\l}aw Byli\'nski :: :: Received April 14, 1989 :: Copyright (c) 1990-2021 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, TARSKI, RELAT_1, XBOOLE_0, SUBSET_1; notations TARSKI, XBOOLE_0, XTUPLE_0, SUBSET_1, ENUMSET1, RELAT_1, FUNCT_1; constructors TARSKI, SUBSET_1, FUNCT_1, ENUMSET1, XTUPLE_0; registrations FUNCT_1, RELAT_1; requirements SUBSET, BOOLE; begin reserve X,Y for set, p,x,x1,x2,y,y1,y2,z,z1,z2 for object; reserve f,g,h for Function; theorem :: GRFUNC_1:1 for G being set st G c= f holds G is Function; theorem :: GRFUNC_1:2 f c= g iff dom f c= dom g & for x being object st x in dom f holds f.x = g.x; theorem :: GRFUNC_1:3 dom f = dom g & f c= g implies f = g; theorem :: GRFUNC_1:4 [x,z] in (g*f) implies [x,f.x] in f & [f.x,z] in g; theorem :: GRFUNC_1:5 {[x,y]} is Function; theorem :: GRFUNC_1:6 f = {[x,y]} implies f.x = y; theorem :: GRFUNC_1:7 dom f = {x} implies f = {[x,f.x]}; theorem :: GRFUNC_1:8 {[x1,y1],[x2,y2]} is Function iff (x1 = x2 implies y1 = y2); theorem :: GRFUNC_1:9 f is one-to-one iff for x1,x2,y st [x1,y] in f & [x2,y] in f holds x1 = x2; theorem :: GRFUNC_1:10 g c= f & f is one-to-one implies g is one-to-one; registration let f,X; cluster f /\ X -> Function-like; end; theorem :: GRFUNC_1:11 x in dom(f /\ g) implies (f /\ g).x = f.x; theorem :: GRFUNC_1:12 f is one-to-one implies f /\ g is one-to-one; theorem :: GRFUNC_1:13 dom f misses dom g implies f \/ g is Function; theorem :: GRFUNC_1:14 f c= h & g c= h implies f \/ g is Function; theorem :: GRFUNC_1:15 x in dom g & h = f \/ g implies h.x = g.x; theorem :: GRFUNC_1:16 x in dom h & h = f \/ g implies h.x = f.x or h.x = g.x; theorem :: GRFUNC_1:17 f is one-to-one & g is one-to-one & h = f \/ g & rng f misses rng g implies h is one-to-one; ::$CT 2 theorem :: GRFUNC_1:20 f is one-to-one implies for x,y holds [y,x] in f" iff [x,y] in f; theorem :: GRFUNC_1:21 f = {} implies f" = {}; theorem :: GRFUNC_1:22 x in dom f & x in X iff [x,f.x] in f|X; theorem :: GRFUNC_1:23 g c= f implies f|dom g = g; theorem :: GRFUNC_1:24 x in dom f & f.x in Y iff [x,f.x] in Y|`f; theorem :: GRFUNC_1:25 g c= f & f is one-to-one implies rng g|`f = g; theorem :: GRFUNC_1:26 x in f"Y iff [x,f.x] in f & f.x in Y; begin :: Addenda :: from HAHNBAN theorem :: GRFUNC_1:27 for X being set, f,g being Function st X c= dom f & f c= g holds f|X = g|X; :: from AMI_3 theorem :: GRFUNC_1:28 for f being Function, x being set st x in dom f holds f|{x} = {[ x,f.x]}; :: from AMI_3, 2007.06.14, A.T. theorem :: GRFUNC_1:29 for f,g being Function, x being set st dom f = dom g & f.x = g.x holds f|{x} = g|{x}; theorem :: GRFUNC_1:30 for f,g being Function, x,y being set st dom f = dom g & f.x = g .x & f.y = g.y holds f|{x,y} = g|{x,y}; theorem :: GRFUNC_1:31 for f,g being Function, x,y,z being set st dom f = dom g & f.x = g.x & f.y = g.y & f.z = g.z holds f|{x,y,z} = g|{x,y,z}; :: from AMISTD_2, 2007.07.26, A.T. registration let f be Function, A be set; cluster f \ A -> Function-like; end; theorem :: GRFUNC_1:32 for f, g being Function st x in dom f \ dom g holds (f \ g).x = f.x; :: missing, 2007.06.19, A.T. theorem :: GRFUNC_1:33 f c= g & f c= h implies g|dom f = h|dom f; :: new, 2009.09.30, A.T. registration let f be Function, g be Subset of f; cluster g-compatible -> f-compatible for Function; end; :: 2009.10.17, A.T. theorem :: GRFUNC_1:34 g c= f implies g = f|dom g; registration let f be Function, g be f-compatible Function; cluster -> f-compatible for Subset of g; end; theorem :: GRFUNC_1:35 g c= f & x in X & X /\ dom f c= dom g implies f.x = g.x;