:: Functions and Their Basic Properties
:: by Czes{\l}aw Byli\'nski
::
:: Received March 3, 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 RELAT_1, XBOOLE_0, ZFMISC_1, SUBSET_1, TARSKI, SETFAM_1, FUNCT_1;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_1, SETFAM_1;
constructors SETFAM_1, RELAT_1, XTUPLE_0;
registrations XBOOLE_0, RELAT_1, ZFMISC_1;
requirements SUBSET, BOOLE;
begin
reserve X,X1,X2,Y,Y1,Y2 for set, p,x,x1,x2,y,y1,y2,z,z1,z2 for object;
definition
let X be set;
attr X is Function-like means
:: FUNCT_1:def 1
for x,y1,y2 st [x,y1] in X & [x,y2] in X holds y1 = y2;
end;
registration
cluster empty -> Function-like for set;
end;
registration
cluster Function-like for Relation;
end;
definition
mode Function is Function-like Relation;
end;
registration
let a, b be object;
cluster {[a,b]} -> Function-like;
end;
reserve f,g,g1,g2,h for Function,
R,S for Relation;
scheme :: FUNCT_1:sch 1
GraphFunc { A()->set,P[object,object] } :
ex f st for x,y being object holds [x,y] in f iff x in A() & P[x,y]
provided
for x,y1,y2 being object st P[x,y1] & P[x,y2] holds y1 = y2;
definition
let f; let x be object;
func f.x -> set means
:: FUNCT_1:def 2
[x,it] in f if x in dom f otherwise it = {};
end;
theorem :: FUNCT_1:1
[x,y] in f iff x in dom f & y = f.x;
theorem :: FUNCT_1:2
dom f = dom g & (for x st x in dom f holds f.x = g.x) implies f = g;
definition
let f;
redefine func rng f means
:: FUNCT_1:def 3
for y being object holds y in it iff
ex x being object st x in dom f & y = f.x;
end;
theorem :: FUNCT_1:3
x in dom f implies f.x in rng f;
theorem :: FUNCT_1:4
dom f = {x} implies rng f = {f.x};
scheme :: FUNCT_1:sch 2
FuncEx { A()->set,P[object,object] } :
ex f st dom f = A() & for x st x in A() holds P[x,f.x]
provided
for x,y1,y2 st x in A() & P[x,y1] & P[x,y2] holds y1 = y2 and
for x st x in A() ex y st P[x,y];
scheme :: FUNCT_1:sch 3
Lambda { A() -> set,F(object) -> object } :
ex f being Function st dom f = A() & for x st x in A() holds f.x = F(x);
theorem :: FUNCT_1:5
X <> {} implies for y ex f st dom f = X & rng f = {y};
theorem :: FUNCT_1:6
(for f,g st dom f = X & dom g = X holds f = g) implies X = {};
theorem :: FUNCT_1:7
dom f = dom g & rng f = {y} & rng g = {y} implies f = g;
theorem :: FUNCT_1:8
Y <> {} or X = {} implies ex f st X = dom f & rng f c= Y;
theorem :: FUNCT_1:9
(for y st y in Y ex x st x in dom f & y = f.x) implies Y c= rng f;
notation
let f,g;
synonym g*f for f*g;
end;
registration
let f,g;
cluster g*f -> Function-like;
end;
theorem :: FUNCT_1:10
for h st (for x holds x in dom h iff x in dom f & f.x in dom g) & (for
x st x in dom h holds h.x = g.(f.x)) holds h = g*f;
theorem :: FUNCT_1:11
x in dom(g*f) iff x in dom f & f.x in dom g;
theorem :: FUNCT_1:12
x in dom(g*f) implies (g*f).x = g.(f.x);
theorem :: FUNCT_1:13
x in dom f implies (g*f).x = g.(f.x);
theorem :: FUNCT_1:14
z in rng(g*f) implies z in rng g;
theorem :: FUNCT_1:15
dom(g*f) = dom f implies rng f c= dom g;
theorem :: FUNCT_1:16
rng f c= Y & (for g,h st dom g = Y & dom h = Y & g*f = h*f holds g = h)
implies Y = rng f;
registration
let X;
cluster id X -> Function-like;
end;
theorem :: FUNCT_1:17
f = id X iff dom f = X & for x st x in X holds f.x = x;
theorem :: FUNCT_1:18
x in X implies (id X).x = x;
theorem :: FUNCT_1:19
dom(f*(id X)) = dom f /\ X;
theorem :: FUNCT_1:20
x in dom f /\ X implies f.x = (f*(id X)).x;
theorem :: FUNCT_1:21
x in dom((id Y)*f) iff x in dom f & f.x in Y;
theorem :: FUNCT_1:22
(id X)*(id Y) = id(X /\ Y);
theorem :: FUNCT_1:23
rng f = dom g & g*f = f implies g = id dom g;
definition
let f;
attr f is one-to-one means
:: FUNCT_1:def 4
for x1,x2 st x1 in dom f & x2 in dom f & f.x1 = f.x2 holds x1 = x2;
end;
theorem :: FUNCT_1:24
f is one-to-one & g is one-to-one implies g*f is one-to-one;
theorem :: FUNCT_1:25
g*f is one-to-one & rng f c= dom g implies f is one-to-one;
theorem :: FUNCT_1:26
g*f is one-to-one & rng f = dom g implies f is one-to-one & g is one-to-one;
theorem :: FUNCT_1:27
f is one-to-one iff for g,h st rng g c= dom f & rng h c= dom f & dom g
= dom h & f*g = f*h holds g = h;
theorem :: FUNCT_1:28
dom f = X & dom g = X & rng g c= X & f is one-to-one & f*g = f implies
g = id X;
theorem :: FUNCT_1:29
rng(g*f) = rng g & g is one-to-one implies dom g c= rng f;
registration
let X be set;
cluster id X -> one-to-one;
end;
::$CT
theorem :: FUNCT_1:31
(ex g st g*f = id dom f) implies f is one-to-one;
registration
cluster empty -> one-to-one for Function;
end;
registration
cluster one-to-one for Function;
end;
registration
let f be one-to-one Function;
cluster f~ -> Function-like;
end;
definition
let f;
assume
f is one-to-one;
func f" -> Function equals
:: FUNCT_1:def 5
f~;
end;
theorem :: FUNCT_1:32
f is one-to-one implies for g being Function holds g=f" iff dom
g = rng f & for y,x holds y in rng f & x = g.y iff x in dom f & y = f.x;
theorem :: FUNCT_1:33
f is one-to-one implies rng f = dom(f") & dom f = rng(f");
theorem :: FUNCT_1:34
f is one-to-one & x in dom f implies x = (f").(f.x) & x = (f"*f) .x;
theorem :: FUNCT_1:35
f is one-to-one & y in rng f implies y = f.((f").y) & y = (f*f") .y;
theorem :: FUNCT_1:36
f is one-to-one implies dom(f"*f) = dom f & rng(f"*f) = dom f;
theorem :: FUNCT_1:37
f is one-to-one implies dom(f*f") = rng f & rng(f*f") = rng f;
theorem :: FUNCT_1:38
f is one-to-one & dom f = rng g & rng f = dom g & (for x,y st x in dom
f & y in dom g holds f.x = y iff g.y = x) implies g = f";
theorem :: FUNCT_1:39
f is one-to-one implies f"*f = id dom f & f*f" = id rng f;
theorem :: FUNCT_1:40
f is one-to-one implies f" is one-to-one;
registration
let f be one-to-one Function;
cluster f" -> one-to-one;
let g be one-to-one Function;
cluster g*f -> one-to-one;
end;
theorem :: FUNCT_1:41
f is one-to-one & rng f = dom g & g*f = id dom f implies g = f";
theorem :: FUNCT_1:42
f is one-to-one & rng g = dom f & f*g = id rng f implies g = f";
theorem :: FUNCT_1:43
f is one-to-one implies (f")" = f;
theorem :: FUNCT_1:44
f is one-to-one & g is one-to-one implies (g*f)" = f"*g";
theorem :: FUNCT_1:45
(id X)" = id X;
registration
let f,X;
cluster f|X -> Function-like;
end;
theorem :: FUNCT_1:46
dom g = dom f /\ X & (for x st x in dom g holds g.x = f.x) implies g = f|X;
theorem :: FUNCT_1:47
x in dom(f|X) implies (f|X).x = f.x;
theorem :: FUNCT_1:48
x in dom f /\ X implies (f|X).x = f.x;
theorem :: FUNCT_1:49
x in X implies (f|X).x = f.x;
theorem :: FUNCT_1:50
x in dom f & x in X implies f.x in rng(f|X);
theorem :: FUNCT_1:51
X c= Y implies (f|X)|Y = f|X & (f|Y)|X = f|X;
theorem :: FUNCT_1:52
f is one-to-one implies f|X is one-to-one;
registration
let Y,f;
cluster Y|`f -> Function-like;
end;
theorem :: FUNCT_1:53
g = Y|`f iff (for x holds x in dom g iff x in dom f & f.x in Y) &
for x st x in dom g holds g.x = f.x;
theorem :: FUNCT_1:54
x in dom(Y|`f) iff x in dom f & f.x in Y;
theorem :: FUNCT_1:55
x in dom(Y|`f) implies (Y|`f).x = f.x;
theorem :: FUNCT_1:56
dom(Y|`f) c= dom f;
theorem :: FUNCT_1:57
X c= Y implies Y|`(X|`f) = X|`f & X|`(Y|`f) = X|`f;
theorem :: FUNCT_1:58
f is one-to-one implies Y|`f is one-to-one;
definition
let f,X;
redefine func f.:X means
:: FUNCT_1:def 6
for y being object holds y in it iff
ex x being object st x in dom f & x in X & y = f.x;
end;
theorem :: FUNCT_1:59
x in dom f implies Im(f,x) = {f.x};
theorem :: FUNCT_1:60
x1 in dom f & x2 in dom f implies f.:{x1,x2} = {f.x1,f.x2};
theorem :: FUNCT_1:61
(Y|`f).:X c= f.:X;
theorem :: FUNCT_1:62
f is one-to-one implies f.:(X1 /\ X2) = f.:X1 /\ f.:X2;
theorem :: FUNCT_1:63
(for X1,X2 holds f.:(X1 /\ X2) = f.:X1 /\ f.:X2) implies f is one-to-one;
theorem :: FUNCT_1:64
f is one-to-one implies f.:(X1 \ X2) = f.:X1 \ f.:X2;
theorem :: FUNCT_1:65
(for X1,X2 holds f.:(X1 \ X2) = f.:X1 \ f.:X2) implies f is one-to-one;
theorem :: FUNCT_1:66
X misses Y & f is one-to-one implies f.:X misses f.:Y;
theorem :: FUNCT_1:67
(Y|`f).:X = Y /\ f.:X;
definition
let f,Y;
redefine func f"Y means
:: FUNCT_1:def 7
for x holds x in it iff x in dom f & f.x in Y;
end;
theorem :: FUNCT_1:68
f"(Y1 /\ Y2) = f"Y1 /\ f"Y2;
theorem :: FUNCT_1:69
f"(Y1 \ Y2) = f"Y1 \ f"Y2;
theorem :: FUNCT_1:70
(R|X)"Y = X /\ (R"Y);
theorem :: FUNCT_1:71
for f being Function, A,B being set st A misses B holds f"A misses f"B;
theorem :: FUNCT_1:72
y in rng R iff R"{y} <> {};
theorem :: FUNCT_1:73
(for y st y in Y holds R"{y} <> {}) implies Y c= rng R;
theorem :: FUNCT_1:74
(for y st y in rng f ex x st f"{y} = {x}) iff f is one-to-one;
theorem :: FUNCT_1:75
f.:(f"Y) c= Y;
theorem :: FUNCT_1:76
X c= dom R implies X c= R"(R.:X);
theorem :: FUNCT_1:77
Y c= rng f implies f.:(f"Y) = Y;
theorem :: FUNCT_1:78
f.:(f"Y) = Y /\ f.:(dom f);
theorem :: FUNCT_1:79
f.:(X /\ f"Y) c= (f.:X) /\ Y;
theorem :: FUNCT_1:80
f.:(X /\ f"Y) = (f.:X) /\ Y;
theorem :: FUNCT_1:81
X /\ R"Y c= R"(R.:X /\ Y);
theorem :: FUNCT_1:82
f is one-to-one implies f"(f.:X) c= X;
theorem :: FUNCT_1:83
(for X holds f"(f.:X) c= X) implies f is one-to-one;
theorem :: FUNCT_1:84
f is one-to-one implies f.:X = (f")"X;
theorem :: FUNCT_1:85
f is one-to-one implies f"Y = (f").:Y;
:: SUPLEMENT
theorem :: FUNCT_1:86
Y = rng f & dom g = Y & dom h = Y & g*f = h*f implies g = h;
theorem :: FUNCT_1:87
f.:X1 c= f.:X2 & X1 c= dom f & f is one-to-one implies X1 c= X2;
theorem :: FUNCT_1:88
f"Y1 c= f"Y2 & Y1 c= rng f implies Y1 c= Y2;
theorem :: FUNCT_1:89
f is one-to-one iff for y ex x st f"{y} c= {x};
theorem :: FUNCT_1:90
rng R c= dom S implies R"X c= (R*S)"(S.:X);
theorem :: FUNCT_1:91
for f being Function st f " X = f " Y & X c= rng f & Y c= rng f holds X = Y;
begin :: Addenda
:: from BORSUK_1
reserve e,u for object,
A for Subset of X;
theorem :: FUNCT_1:92
(id X).:A = A;
:: from PBOOLE
definition
let f be Function;
redefine attr f is empty-yielding means
:: FUNCT_1:def 8
for x st x in dom f holds f.x is empty;
end;
:: from UNIALG_1
definition
let F be Function;
redefine attr F is non-empty means
:: FUNCT_1:def 9
for n being object st n in dom F holds F.n is non empty;
end;
:: new, 2004.08.04
registration
cluster non-empty for Function;
end;
:: from MSUALG_2
scheme :: FUNCT_1:sch 4
LambdaB { D()->non empty set, F(object)->object } :
ex f be Function st dom f = D() & for d be Element of D() holds f.d = F(d);
:: from PUA2MSS1, 2005.08.22, A.T.
registration
let f be non-empty Function;
cluster rng f -> with_non-empty_elements;
end;
:: from SEQM_3, 2005.12.17, A.T.
definition
let f be Function;
attr f is constant means
:: FUNCT_1:def 10
x in dom f & y in dom f implies f.x = f.y;
end;
theorem :: FUNCT_1:93
for A,B being set, f being Function st A c= dom f & f.:A c= B holds A c= f"B;
:: moved from MSAFREE3:1, AG 1.04.2006
theorem :: FUNCT_1:94
for f being Function st X c= dom f & f is one-to-one holds f"(f.:X) = X;
:: added, AK 5.02.2007
definition
let f,g;
redefine pred f = g means
:: FUNCT_1:def 11
dom f = dom g & for x st x in dom f holds f.x = g.x;
end;
:: missing, 2007.03.09, A.T.
registration
cluster non-empty non empty for Function;
end;
:: from PRVECT_1, 2007.03.09, A.T.
registration
let a be non-empty non empty Function;
let i be Element of dom a;
cluster a.i -> non empty;
end;
:: missing, 2007.04.13, A.T.
registration
let f be Function;
cluster -> Function-like for Subset of f;
end;
:: from SCMFSA6A, 2007.07.23, A.T.
theorem :: FUNCT_1:95
for f,g being Function, D being set st D c= dom f & D c= dom g holds f
| D = g | D iff for x being set st x in D holds f.x = g.x;
:: from SCMBSORT, 2007.07.26, A.T.
theorem :: FUNCT_1:96
for f,g being Function, X being set st dom f = dom g & (for x being
set st x in X holds f.x = g.x) holds f|X = g|X;
:: missing, 2007.10.28, A.T.
theorem :: FUNCT_1:97
rng(f|{X}) c= {f.X};
theorem :: FUNCT_1:98
X in dom f implies rng(f|{X}) ={f.X};
:: from RFUNCT_1, 2008.09.04, A.T.
registration
cluster empty -> constant for Function;
end;
:: from WAYBEL35, 2008.08.04, A.T.
registration
let f be constant Function;
cluster rng f -> trivial;
end;
registration
cluster non constant for Function;
end;
registration
let f be non constant Function;
cluster rng f -> non trivial;
end;
registration
cluster non constant -> non trivial for Function;
end;
registration
cluster trivial -> constant for Function;
end;
:: from RFUNCT_2, 2008.09.14, A.T.
theorem :: FUNCT_1:99
for F,G be Function, X holds (G|(F.:X))*(F|X) = (G*F)|X;
theorem :: FUNCT_1:100
for F,G be Function, X,X1 holds (G|X1)*(F|X) = (G*F)|(X /\ (F"X1));
theorem :: FUNCT_1:101
for F,G be Function,X holds X c= dom (G*F) iff X c= dom F & F.:X c= dom G;
:: from YELLOW_6, 2008.12.26, A.T.
definition
let f be Function;
assume
f is non empty constant;
func the_value_of f -> object means
:: FUNCT_1:def 12
ex x being set st x in dom f & it = f.x;
end;
:: from QC_LANG4, 2009.01.23, A.T
registration
let X,Y;
cluster X-defined Y-valued for Function;
end;
theorem :: FUNCT_1:102
for X being set, f being X-valued Function for x being set st x in dom
f holds f.x in X;
:: from FRAENKEL, 2009.05.06, A.K.
definition
let IT be set;
attr IT is functional means
:: FUNCT_1:def 13
for x being object st x in IT holds x is Function;
end;
registration
cluster empty -> functional for set;
let f be Function;
cluster { f } -> functional;
let g be Function;
cluster { f,g } -> functional;
end;
registration
cluster non empty functional for set;
end;
registration
let P be functional set;
cluster -> Function-like Relation-like for Element of P;
end;
registration
let A be functional set;
cluster -> functional for Subset of A;
end;
:: new, 2009.09.30, A.T.
definition let g,f be Function;
attr f is g-compatible means
:: FUNCT_1:def 14
x in dom f implies f.x in g.x;
end;
theorem :: FUNCT_1:103
f is g-compatible & dom f = dom g implies g is non-empty;
theorem :: FUNCT_1:104
{} is f-compatible;
registration
let I be set, f be Function;
cluster empty I-defined f-compatible for Function;
end;
registration let X be set;
let f be Function, g be f-compatible Function;
cluster g|X -> f-compatible;
end;
registration let I be set;
cluster non-empty I-defined for Function;
end;
theorem :: FUNCT_1:105
for g being f-compatible Function holds dom g c= dom f;
registration let X;
let f be X-defined Function;
cluster f-compatible -> X-defined for Function;
end;
theorem :: FUNCT_1:106
for f being X-valued Function st x in dom f holds f.x is Element of X;
:: from JGRAPH_6, 2010.03.15, A.T.
theorem :: FUNCT_1:107
for f being Function,A being set st f is one-to-one & A c= dom f
holds f".:(f.:A)=A;
registration
let A be functional set, x be object;
let F be A-valued Function;
cluster F.x -> Function-like Relation-like;
end;
:: missing, 2011.03.06, A.T.
theorem :: FUNCT_1:108
x in X & x in dom f implies f.x in f.:X;
theorem :: FUNCT_1:109
X <> {} & X c= dom f implies f.:X <> {};
registration
let f be non trivial Function;
cluster dom f -> non trivial;
end;
:: from HAHNBAN, 2011.04.26, A.T.
theorem :: FUNCT_1:110
for B being non empty functional set, f being Function
st f = union B
holds dom f = union the set of all dom g where g is Element of B
& rng f = union the set of all rng g where g is Element of B;
scheme :: FUNCT_1:sch 5
LambdaS { A() -> set,F(object) -> object } :
ex f being Function st dom f = A() &
for X st X in A() holds f.X = F(X);
theorem :: FUNCT_1:111 :: WELLORD2:28
for M being set
st for X st X in M holds X <> {}
ex f being Function
st dom f = M & for X st X in M holds f.X in X;
scheme :: FUNCT_1:sch 6
NonUniqBoundFuncEx { X() -> set, Y() -> set, P[object,object] }:
ex f being Function st dom f = X() & rng f c= Y()
& for x being object st x in X() holds P[x,f.x]
provided
for x being object st x in X() ex y being object st y in Y() & P[x,y];
registration
let f be empty-yielding Function;
let x;
cluster f.x -> empty;
end;
:: from PNPROC_1, 2012.02.20, A.T.
theorem :: FUNCT_1:112
for f,g,h being Function st
f c= h & g c= h & f misses g holds dom f misses dom g;
theorem :: FUNCT_1:113
for Y being set, f being Function holds Y|`f = f|(f"Y);
registration
let X be set;
let x be Element of X;
reduce (id X).x to x;
end;
theorem :: FUNCT_1:114
rng f c= rng g implies
for x being object st x in dom f
ex y being object st y in dom g & f.x = g. y;