:: Function Domains and Fr{\ae}nkel Operator :: by Andrzej Trybulec :: :: Received February 7, 1990 :: Copyright (c) 1990-2016 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 XBOOLE_0, SUBSET_1, TARSKI, FUNCT_1, RELAT_1, FUNCT_2, ZFMISC_1, PARTFUN1, FINSET_1, MCART_1, FINSUB_1, SETWISEO; notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, XTUPLE_0, MCART_1, RELAT_1, FINSET_1, FINSUB_1, FUNCT_1, RELSET_1, PARTFUN1, FUNCT_2, BINOP_1, DOMAIN_1, SETWISEO; constructors PARTFUN1, BINOP_1, DOMAIN_1, FINSET_1, SETWISEO, RELSET_1, XTUPLE_0; registrations SUBSET_1, RELAT_1, FINSET_1, FINSUB_1, RELSET_1, XTUPLE_0; requirements BOOLE, SUBSET; begin reserve B for non empty set, A,X,x for set; scheme :: FRAENKEL:sch 1 Fraenkel59{ A() -> set, F(object) -> object, P,Q[object] } : { F(v) where v is Element of A() : P[v] } c= { F(u) where u is Element of A() : Q[u] } provided for v being Element of A() holds P[v] implies Q[v]; scheme :: FRAENKEL:sch 2 Fraenkel599 { A,B() -> set, F(object,object) -> object, P,Q[object,object] }: { F(u1,v1) where u1 is Element of A(), v1 is Element of B() : P[u1,v1] } c= { F(u2,v2) where u2 is Element of A(), v2 is Element of B() : Q[u2,v2] } provided for u being (Element of A()), v being Element of B() holds P[u,v] implies Q[u,v]; scheme :: FRAENKEL:sch 3 Fraenkel69{ B() -> set, F(object) -> object, P, Q[object] } : { F(v1) where v1 is Element of B() : P[v1] } = { F(v2) where v2 is Element of B() : Q[v2] } provided for v being Element of B() holds P[v] iff Q[v]; scheme :: FRAENKEL:sch 4 Fraenkel699 { A,B() -> set, F(object,object) -> object, P,Q[object,object] }: { F(u1,v1) where u1 is Element of A(), v1 is Element of B() : P[u1,v1] } = { F(u2,v2) where u2 is Element of A(), v2 is Element of B() : Q[u2,v2] } provided for u being Element of A(), v being Element of B() holds P[u,v] iff Q[u,v]; scheme :: FRAENKEL:sch 5 FraenkelF9{ B() -> set, F,G(object) -> object, P[object] } : { F(v1) where v1 is Element of B() : P[v1] } = { G(v2) where v2 is Element of B() : P[v2] } provided for v being Element of B() holds F(v) = G(v); scheme :: FRAENKEL:sch 6 FraenkelF9R{ B() -> set, F,G(object) -> object, P[object] } : { F(v1) where v1 is Element of B() : P[v1] } = { G(v2) where v2 is Element of B() : P[v2] } provided for v being Element of B() st P[v] holds F(v) = G(v); scheme :: FRAENKEL:sch 7 FraenkelF99 { A,B() -> set, F,G(object,object) -> object, P[object,object] }: { F(u1,v1) where u1 is Element of A(), v1 is Element of B() : P[u1,v1] } = { G(u2,v2) where u2 is Element of A(), v2 is Element of B() : P[u2,v2] } provided for u being Element of A(), v being Element of B() holds F(u,v) = G(u,v); scheme :: FRAENKEL:sch 8 FraenkelF699 { A,B() -> set, F(object,object) -> object, P,Q[object,object] }: { F(u1,v1) where u1 is Element of A(), v1 is Element of B() : P[u1,v1] } = { F(v2,u2) where u2 is Element of A(), v2 is Element of B() : Q[u2,v2] } provided for u being Element of A(), v being Element of B() holds P[u,v] iff Q[u,v] and for u being Element of A(), v being Element of B() holds F(u,v) = F(v,u); theorem :: FRAENKEL:1 for A,B being set, F,G being Function of A,B for X being set st F|X = G|X for x being Element of A st x in X holds F.x = G.x; theorem :: FRAENKEL:2 for A,B being set holds Funcs(A,B) c= bool [:A,B:]; theorem :: FRAENKEL:3 for X,Y being set st Funcs(X,Y) <> {} & X c= A & Y c= B for f being Element of Funcs(X,Y) holds f is PartFunc of A,B; scheme :: FRAENKEL:sch 9 RelevantArgs { A,B,X() -> set, f,g() -> Function of A(),B(), P,Q[object] } : { f().u9 where u9 is Element of A() : P[u9] & u9 in X() } = { g().v9 where v9 is Element of A() : Q[v9] & v9 in X() } provided f()|X() = g()|X() and for u being Element of A() st u in X() holds P[u] iff Q[u]; scheme :: FRAENKEL:sch 10 FrSet0{ A() -> non empty set, P[object] }: { x where x is Element of A(): P[x] } c= A(); scheme :: FRAENKEL:sch 11 Gen199{A,B() -> set, F(object,object) -> object, P[object,object], Q[object] }: for s being Element of A(), t being Element of B() st P[s,t] holds Q[F(s,t)] provided for st1 being set st st1 in { F(s1,t1) where s1 is (Element of A()), t1 is Element of B(): P[s1,t1] } holds Q[st1]; scheme :: FRAENKEL:sch 12 Gen199A{A,B() -> set, F(object,object) -> object, P[object,object], Q[object] } : for st1 being set st st1 in { F(s1,t1) where s1 is Element of A(), t1 is Element of B(): P[s1,t1] } holds Q[st1] provided for s being Element of A(), t being Element of B() st P[s,t] holds Q[F(s,t)]; scheme :: FRAENKEL:sch 13 Gen299{A,B,C() -> set, F(object,object) -> Element of C(), P[object,object], Q[object] } : { st1 where st1 is Element of C() : st1 in { F(s1,t1) where s1 is Element of A(), t1 is Element of B() : P[s1,t1] } & Q[st1] } = { F(s2,t2) where s2 is Element of A(), t2 is Element of B() : P[s2,t2] & Q[F(s2,t2)]}; scheme :: FRAENKEL:sch 14 Gen39{A() -> set, F(object) -> object, P,Q[object] } : { F(s) where s is Element of A() : s in { s1 where s1 is Element of A(): Q[s1] } & P[s] } = { F(s2) where s2 is Element of A() : Q[s2] & P[s2] }; scheme :: FRAENKEL:sch 15 Gen399{A,B() -> set, F(object,object) -> object, P[object,object], Q[object] }: { F(s,t) where s is (Element of A()), t is Element of B() : s in { s1 where s1 is Element of A(): Q[s1] } & P[s,t] } = { F(s2,t2) where s2 is (Element of A()), t2 is Element of B() : Q[s2] & P[s2,t2] }; scheme :: FRAENKEL:sch 16 Gen499{A,B() -> set, F(object,object) -> object, P,Q[object,object] } : { F(s,t) where s is (Element of A()), t is Element of B() : P[s,t] } c= { F(s1,t1) where s1 is (Element of A()), t1 is Element of B() : Q [s1,t1] } provided for s being (Element of A()), t being Element of B() st P[s,t] ex s9 being Element of A() st Q[s9,t] & F(s,t) = F(s9,t); scheme :: FRAENKEL:sch 17 FrSet1{ D,A() -> set, P[object], F(object) -> object }: { F(y) where y is Element of D() : F(y) in A() & P[y] } c= A(); scheme :: FRAENKEL:sch 18 FrSet2{ D,A() -> set, Q[object], F(object) -> object }: { F(y) where y is Element of D() : Q[y] & not F(y) in A() } misses A(); scheme :: FRAENKEL:sch 19 FrEqua1{ A,B() -> set, F(object,object) -> object, x() -> (Element of B()), P,Q[object,object] }: { F(s,t) where s is (Element of A()), t is Element of B(): Q[s,t] } = { F(s9,x()) where s9 is Element of A(): P [s9,x()] } provided for s being Element of A() for t being Element of B() holds Q[s,t] iff t = x() & P[s,t]; scheme :: FRAENKEL:sch 20 FrEqua2{ A,B() -> set, F(object,object) -> object, x() -> (Element of B()), P[object,object] }: { F(s,t) where s is (Element of A()), t is Element of B(): t = x() & P[s,t] } = { F(s9,x()) where s9 is Element of A(): P[ s9,x()] }; :: dziedziny funkcji reserve phi for Element of Funcs(A,B); theorem :: FRAENKEL:4 for X,Y being set st Funcs(X,Y) <> {} & X c= A & Y c= B for f being Element of Funcs(X,Y) ex phi being Element of Funcs(A,B) st phi|X = f; theorem :: FRAENKEL:5 phi|X = phi|(A /\ X); :: Zbiory skonczone scheme :: FRAENKEL:sch 21 FraenkelFin { A,X() -> set, F(object) -> object }: { F(w) where w is Element of A(): w in X() } is finite provided X() is finite; scheme :: FRAENKEL:sch 22 CartFin { A, B() -> non empty set, X, Y() -> set, F(object, object) -> object }: { F(u,v) where u is Element of A(), v is Element of B() : u in X() & v in Y () } is finite provided X() is finite and Y() is finite; scheme :: FRAENKEL:sch 23 Finiteness { A()->non empty set, B()->(Element of Fin A()), P[(Element of A( )), Element of A()] } : for x being Element of A() st x in B() ex y being Element of A() st y in B() & P[y,x] & for z being Element of A() st z in B() & P[z,y] holds P[y,z] provided for x being Element of A() holds P[x,x] and for x,y,z being Element of A() st P[x,y] & P[y,z] holds P[x,z]; scheme :: FRAENKEL:sch 24 FinIm{A,B()->non empty set, x()-> (Element of Fin B()), F(object)->(Element of A()), P[object,object]}: ex c1 being Element of Fin A() st for t being Element of A() holds t in c1 iff ex t9 being Element of B() st t9 in x() & t = F(t9) & P[t,t9]; registration let A, B be finite set; cluster Funcs(A,B) -> finite; end; theorem :: FRAENKEL:6 for A,B being set st A is finite & B is finite holds Funcs(A,B) is finite; scheme :: FRAENKEL:sch 25 ImFin { A() -> set, B() -> non empty set, X,Y() -> set, F(object) -> object } : { F(phi9) where phi9 is Element of Funcs(A(),B()): phi9.:X() c= Y() } is finite provided X() is finite and Y() is finite and for phi,psi being Element of Funcs(A(),B()) holds phi|X() = psi|X() implies F(phi) = F(psi); :: Schematy zwiazane z pewnikiem wyboru scheme :: FRAENKEL:sch 26 FunctChoice { A()->non empty set, B()->non empty set, P[(Element of A()), Element of B()], x()->Element of Fin A() }: ex ff being Function of A(), B() st for t being Element of A() st t in x() holds P[t,ff.t] provided for t being Element of A() st t in x() ex ff being Element of B() st P[t,ff]; scheme :: FRAENKEL:sch 27 FuncsChoice { A()->non empty set, B()->non empty set, P[Element of A(), Element of B()], x()->Element of Fin A() }: ex ff being Element of Funcs(A(),B( )) st for t being Element of A() st t in x() holds P[t,ff.t] provided for t being Element of A() st t in x() ex ff being Element of B() st P[t,ff]; scheme :: FRAENKEL:sch 28 FraenkelFin9 { A,B() -> non empty set, X() -> set, P[object,object] }: { x where x is Element of B(): ex w being Element of A() st P[w,x] & w in X() } is finite provided X() is finite and for w being Element of A(), x,y being Element of B() st P[w,x] & P[w ,y] holds x = y;