:: 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;