:: Graphs of Functions :: by Czes{\l}aw Byli\'nski :: :: Received April 14, 1989 :: Copyright (c) 1990-2017 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; definitions RELAT_1, XBOOLE_0, FUNCT_1; equalities XBOOLE_0; expansions RELAT_1, FUNCT_1; theorems TARSKI, XBOOLE_0, ZFMISC_1, FUNCT_1, RELAT_1, XBOOLE_1, ENUMSET1, XTUPLE_0; 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 Th1: for G being set st G c= f holds G is Function; theorem Th2: f c= g iff dom f c= dom g & for x being object st x in dom f holds f.x = g.x proof thus f c= g implies dom f c= dom g & for x being object st x in dom f holds f.x = g.x proof assume A1: f c= g; hence dom f c= dom g by RELAT_1:11; let x be object; assume x in dom f; then [x,f.x] in f by FUNCT_1:def 2; hence thesis by A1,FUNCT_1:1; end; assume that A2: dom f c= dom g and A3: for x being object st x in dom f holds f.x = g.x; let x,y be object; assume A4: [x,y] in f; then A5: x in dom f by FUNCT_1:1; y = f.x by A4,FUNCT_1:1; then y = g.x by A3,A5; hence thesis by A2,A5,FUNCT_1:def 2; end; theorem dom f = dom g & f c= g implies f = g proof assume that A1: dom f = dom g and A2: f c= g; for x,y being object holds [x,y] in f iff [x,y] in g proof let x,y be object; thus [x,y] in f implies [x,y] in g by A2; assume A3: [x,y] in g; then x in dom f by A1,XTUPLE_0:def 12; then [x,f.x] in f by FUNCT_1:1; hence thesis by A2,A3,FUNCT_1:def 1; end; hence thesis; end; Lm1: rng f /\ rng h = {} & x in dom f & y in dom h implies f.x <> h.y proof assume A1: rng f /\ rng h = {}; assume x in dom f & y in dom h; then f.x in rng f & h.y in rng h by FUNCT_1:def 3; hence thesis by A1,XBOOLE_0:def 4; end; theorem [x,z] in (g*f) implies [x,f.x] in f & [f.x,z] in g proof assume [x,z] in (g*f); then ex y being object st [x,y] in f & [y,z] in g by RELAT_1:def 8; hence thesis by FUNCT_1:1; end; theorem {[x,y]} is Function; Lm2: [x,y] in {[x1,y1]} implies x = x1 & y = y1 proof assume [x,y] in {[x1,y1]}; then [x,y] = [x1,y1] by TARSKI:def 1; hence thesis by XTUPLE_0:1; end; theorem f = {[x,y]} implies f.x = y proof assume f = {[x,y]}; then [x,y] in f by TARSKI:def 1; hence thesis by FUNCT_1:1; end; theorem Th7: dom f = {x} implies f = {[x,f.x]} proof reconsider g = {[x,f.x]} as Function; assume A1: dom f = {x}; for y,z being object holds [y,z] in f iff [y,z] in g proof let y,z be object; thus [y,z] in f implies [y,z] in g proof assume A2: [y,z] in f; then y in {x} by A1,XTUPLE_0:def 12; then A3: y = x by TARSKI:def 1; A4: rng f = {f.x} by A1,FUNCT_1:4; z in rng f by A2,XTUPLE_0:def 13; then z = f.x by A4,TARSKI:def 1; hence thesis by A3,TARSKI:def 1; end; assume [y,z] in g; then A5: y = x & z = f.x by Lm2; x in dom f by A1,TARSKI:def 1; hence thesis by A5,FUNCT_1:def 2; end; hence thesis; end; theorem {[x1,y1],[x2,y2]} is Function iff (x1 = x2 implies y1 = y2) proof thus {[x1,y1],[x2,y2]} is Function & x1 = x2 implies y1 = y2 proof A1: [x1,y1] in {[x1,y1],[x2,y2]} & [x2,y2] in {[x1,y1],[x2,y2]} by TARSKI:def 2; assume {[x1,y1],[x2,y2]} is Function; hence thesis by A1,FUNCT_1:def 1; end; assume A2: x1 = x2 implies y1 = y2; now thus p in {[x1,y1],[x2,y2]} implies ex x,y st [x,y] = p proof assume p in {[x1,y1],[x2,y2]}; then p = [x1,y1] or p = [x2,y2] by TARSKI:def 2; hence thesis; end; let x,z1,z2; A3: [x,z1] = [x1,y1] & [x,z2] = [x1,y1] or [x,z1] = [x2,y2] & [x,z2] = [ x2,y2] implies z1 = y1 & z2 = y1 or z1 = y2 & z2 = y2 by XTUPLE_0:1; A4: now assume A5: [x,z1] = [x1,y1] & [x,z2] = [x2,y2] or [x,z1] = [x2,y2] & [x,z2 ] = [x1,y1]; then x = x1 & x = x2 by XTUPLE_0:1; hence z1 = z2 by A2,A5,XTUPLE_0:1; end; assume [x,z1] in {[x1,y1],[x2,y2]} & [x,z2] in {[x1,y1],[x2,y2]}; hence z1 = z2 by A3,A4,TARSKI:def 2; end; hence thesis by FUNCT_1:def 1; end; theorem Th9: f is one-to-one iff for x1,x2,y st [x1,y] in f & [x2,y] in f holds x1 = x2 proof thus f is one-to-one implies for x1,x2,y st [x1,y] in f & [x2,y] in f holds x1 = x2 proof assume A1: f is one-to-one; let x1,x2,y; assume A2: [x1,y] in f & [x2,y] in f; then A3: f.x1 = y & f.x2 = y by FUNCT_1:1; x1 in dom f & x2 in dom f by A2,FUNCT_1:1; hence thesis by A1,A3; end; assume A4: for x1,x2,y st [x1,y] in f & [x2,y] in f holds x1 = x2; let x1,x2; assume x1 in dom f & x2 in dom f & f.x1 = f.x2; then [x1,f.x1] in f & [x2,f.x1] in f by FUNCT_1:1; hence thesis by A4; end; theorem Th10: g c= f & f is one-to-one implies g is one-to-one proof assume g c= f & f is one-to-one; then for x1,x2,y st [x1,y] in g & [x2,y] in g holds x1 = x2 by Th9; hence thesis by Th9; end; registration let f,X; cluster f /\ X -> Function-like; coherence by Th1,XBOOLE_1:17; end; theorem x in dom(f /\ g) implies (f /\ g).x = f.x proof set y = (f /\ g).x; assume x in dom(f /\ g); then [x,y] in (f /\ g) by FUNCT_1:def 2; then [x,y] in f by XBOOLE_0:def 4; hence thesis by FUNCT_1:1; end; theorem f is one-to-one implies f /\ g is one-to-one by Th10,XBOOLE_1:17; theorem dom f misses dom g implies f \/ g is Function proof assume A1: dom f /\ dom g = {}; now thus p in f \/ g implies ex x,y being object st [x,y] = p by RELAT_1:def 1; let x,y1,y2; assume [x,y1] in f \/ g; then A2: [x,y1] in f or [x,y1] in g by XBOOLE_0:def 3; assume [x,y2] in f \/ g; then A3: [x,y2] in f or [x,y2] in g by XBOOLE_0:def 3; not (x in dom f & x in dom g) by A1,XBOOLE_0:def 4; hence y1 = y2 by A2,A3,FUNCT_1:def 1,XTUPLE_0:def 12; end; hence thesis by FUNCT_1:def 1; end; theorem f c= h & g c= h implies f \/ g is Function by Th1,XBOOLE_1:8; Lm3: h = f \/ g implies (x in dom h iff x in dom f or x in dom g) proof assume A1: h = f \/ g; thus x in dom h implies x in dom f or x in dom g proof assume x in dom h; then [x,h.x] in h by FUNCT_1:def 2; then [x,h.x] in f or [x,h.x] in g by A1,XBOOLE_0:def 3; hence thesis by XTUPLE_0:def 12; end; assume x in dom f or x in dom g; then [x,f.x] in f or [x,g.x] in g by FUNCT_1:def 2; then [x,f.x] in h or [x,g.x] in h by A1,XBOOLE_0:def 3; hence thesis by XTUPLE_0:def 12; end; theorem Th15: x in dom g & h = f \/ g implies h.x = g.x proof assume x in dom g; then [x,g.x] in g by FUNCT_1:def 2; then h = f \/ g implies [x,g.x] in h by XBOOLE_0:def 3; hence thesis by FUNCT_1:1; end; theorem x in dom h & h = f \/ g implies h.x = f.x or h.x = g.x proof assume x in dom h; then [x,h.x] in h by FUNCT_1:def 2; then h = f \/ g implies [x,h.x] in f or [x,h.x] in g by XBOOLE_0:def 3; hence thesis by FUNCT_1:1; end; theorem f is one-to-one & g is one-to-one & h = f \/ g & rng f misses rng g implies h is one-to-one proof assume that A1: f is one-to-one & g is one-to-one and A2: h = f \/ g and A3: rng f /\ rng g = {}; now let x1,x2; assume that A4: x1 in dom h & x2 in dom h and A5: h.x1 = h.x2; A6: now assume x1 in dom f & x2 in dom g or x1 in dom g & x2 in dom f; then h.x1 = f.x1 & h.x2 = g.x2 & f.x1 <> g.x2 or h.x1 = g.x1 & h.x2 = f. x2 & f.x2 <> g.x1 by A2,A3,Lm1,Th15; hence x1 = x2 by A5; end; A7: x1 in dom g & x2 in dom g implies h.x1 = g.x1 & h.x2 = g.x2 by A2,Th15; x1 in dom f & x2 in dom f implies h.x1 = f.x1 & h.x2 = f.x2 by A2,Th15; then x1 in dom f & x2 in dom f or x1 in dom g & x2 in dom g implies x1 = x2 by A1,A5,A7; hence x1 = x2 by A2,A4,A6,Lm3; end; hence thesis; end; ::\$CT 2 theorem f is one-to-one implies for x,y holds [y,x] in f" iff [x,y] in f proof assume A1: f is one-to-one; let x,y; dom(f") = rng(f) by A1,FUNCT_1:33; then y in dom(f") & x = (f").y iff x in dom f & y = f.x by A1,FUNCT_1:32; hence thesis by FUNCT_1:1; end; theorem f = {} implies f" = {} proof assume f = {}; then dom(f") = {} by FUNCT_1:33,RELAT_1:38; hence thesis; end; theorem x in dom f & x in X iff [x,f.x] in f|X proof x in dom f iff [x,f.x] in f by FUNCT_1:def 2,XTUPLE_0:def 12; hence thesis by RELAT_1:def 11; end; theorem Th21: g c= f implies f|dom g = g proof assume A1: g c= f; for x,y being object holds [x,y] in (f|dom g) implies [x,y] in g proof let x,y be object; assume A2: [x,y] in (f|dom g); then x in dom g by RELAT_1:def 11; then A3: [x,g.x] in g by FUNCT_1:def 2; [x,y] in f by A2,RELAT_1:def 11; hence thesis by A1,A3,FUNCT_1:def 1; end; then A4: (f|dom g) c= g; (g|dom g) c= (f|dom g) by A1,RELAT_1:76; then g c= (f|dom g); hence thesis by A4; end; theorem x in dom f & f.x in Y iff [x,f.x] in Y|`f proof x in dom f iff [x,f.x] in f by FUNCT_1:def 2,XTUPLE_0:def 12; hence thesis by RELAT_1:def 12; end; theorem g c= f & f is one-to-one implies rng g|`f = g proof assume A1: g c= f; assume A2: f is one-to-one; for x,y being object holds [x,y] in (rng g|`f) implies [x,y] in g proof let x,y be object; assume A3: [x,y] in (rng g|`f); then y in rng g by RELAT_1:def 12; then A4: ex x1 being object st [x1,y] in g by XTUPLE_0:def 13; [x,y] in f by A3,RELAT_1:def 12; hence thesis by A1,A2,A4,Th9; end; then A5: (rng g|`f) c= g; (rng g|`g) c= (rng g|`f) by A1,RELAT_1:101; then g c= (rng g|`f); hence thesis by A5; end; theorem x in f"Y iff [x,f.x] in f & f.x in Y proof thus x in f"Y implies [x,f.x] in f & f.x in Y proof assume x in f"Y; then ex y being object st [x,y] in f & y in Y by RELAT_1:def 14; hence thesis by FUNCT_1:1; end; thus thesis by RELAT_1:def 14; end; begin :: Addenda :: from HAHNBAN theorem for X being set, f,g being Function st X c= dom f & f c= g holds f|X = g|X proof let X be set, f,g be Function such that A1: X c= dom f; assume f c= g; hence f|X = g|(dom f)|X by Th21 .= g|((dom f) /\ X) by RELAT_1:71 .= g|X by A1,XBOOLE_1:28; end; :: from AMI_3 theorem Th26: for f being Function, x being set st x in dom f holds f|{x} = {[ x,f.x]} proof let f be Function, x be set such that A1: x in dom f; A2: x in {x} by TARSKI:def 1; dom(f|{x} qua Function) = dom f /\ {x} by RELAT_1:61 .= {x} by A1,ZFMISC_1:46; hence f|{x} = {[x,(f|{x}).x]} by Th7 .= {[x,f.x]} by A2,FUNCT_1:49; end; :: from AMI_3, 2007.06.14, A.T. theorem Th27: for f,g being Function, x being set st dom f = dom g & f.x = g.x holds f|{x} = g|{x} proof let f,g be Function, x be set such that A1: dom f = dom g and A2: f.x = g.x; per cases; suppose A3: x in dom f; hence f|{x} = {[x,g.x]} by A2,Th26 .= g|{x} by A1,A3,Th26; end; suppose not x in dom f; then A4: {x} misses dom f by ZFMISC_1:50; hence f|{x} = {} by RELAT_1:66 .= g|{x} by A1,A4,RELAT_1:66; end; end; theorem Th28: 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} proof let f,g be Function, x,y be set; assume dom f = dom g & f.x = g.x & f.y = g.y; then A1: f|{x} = g|{x} & f|{y} = g|{y} by Th27; {x,y} = {x} \/ {y} by ENUMSET1:1; hence thesis by A1,RELAT_1:150; end; theorem 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} proof let f,g be Function, x,y,z be set; assume dom f = dom g & f.x = g.x & f.y = g.y & f.z = g.z; then A1: f|{x,y} = g|{x,y} & f|{z} = g|{z} by Th27,Th28; {x,y,z} = {x,y} \/ {z} by ENUMSET1:3; hence thesis by A1,RELAT_1:150; end; :: from AMISTD_2, 2007.07.26, A.T. registration let f be Function, A be set; cluster f \ A -> Function-like; coherence; end; theorem for f, g being Function st x in dom f \ dom g holds (f \ g).x = f.x proof let f, g be Function such that A1: x in dom f \ dom g; f \ g c= f & dom f \ dom g c= dom (f \ g) by XTUPLE_0:25; hence thesis by A1,Th2; end; :: missing, 2007.06.19, A.T. theorem f c= g & f c= h implies g|dom f = h|dom f proof assume that A1: f c= g and A2: f c= h; thus g|dom f = f by A1,Th21 .= h|dom f by A2,Th21; end; :: new, 2009.09.30, A.T. registration let f be Function, g be Subset of f; cluster g-compatible -> f-compatible for Function; coherence proof let F be Function such that A1: F is g-compatible; let x; assume x in dom F; then A2: F.x in g.x by A1; then x in dom g by FUNCT_1:def 2; hence F.x in f.x by A2,Th2; end; end; :: 2009.10.17, A.T. theorem Th32: g c= f implies g = f|dom g proof assume A1: g c= f; then dom g c= dom f by RELAT_1:11; hence dom g = dom(f|dom g) by RELAT_1:62; let x; assume A2: x in dom g; hence g.x = f.x by A1,Th2 .= (f|dom g).x by A2,FUNCT_1:49; end; registration let f be Function, g be f-compatible Function; cluster -> f-compatible for Subset of g; coherence proof let h be Subset of g; h = g|dom h by Th32; hence thesis; end; end; theorem g c= f & x in X & X /\ dom f c= dom g implies f.x = g.x proof assume that A1: g c= f and A2: x in X and A3: X /\ dom f c= dom g; per cases; suppose x in dom g; hence f.x = g.x by A1,Th2; end; suppose A4: not x in dom g; then not x in X /\ dom f by A3; then not x in dom f by A2,XBOOLE_0:def 4; hence f.x = {} by FUNCT_1:def 2 .= g.x by A4,FUNCT_1:def 2; end; end;