Volume 2, 1990

University of Bialystok

Copyright (c) 1990 Association of Mizar Users

### The abstract of the Mizar article:

### Function Domains and Fr\aenkel Operator

**by****Andrzej Trybulec**- Received February 7, 1990
- MML identifier: FRAENKEL

- [ Mizar article, MML identifier index ]

environ vocabulary FUNCT_1, RELAT_1, FUNCT_2, BOOLE, PARTFUN1, FINSET_1, MCART_1, FINSUB_1, SETWISEO, FRAENKEL; notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, MCART_1, RELAT_1, FINSET_1, FINSUB_1, FUNCT_1, FUNCT_2, DOMAIN_1, PARTFUN1, SETWISEO; constructors FINSET_1, DOMAIN_1, SETWISEO, XBOOLE_0; clusters FINSUB_1, FUNCT_1, RELSET_1, SUBSET_1, FINSET_1, RELAT_1, ZFMISC_1, XBOOLE_0; requirements BOOLE, SUBSET; begin reserve B for non empty set, A,C,X,x for set; scheme Fraenkel5'{ A() -> non empty set, F(set) -> set, P[set], Q[set] } : { 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 Fraenkel5'' { A() -> non empty set, B() -> non empty set , F(set,set) -> set, P[set,set], Q[set,set] } : { 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 Fraenkel6'{ B() -> non empty set, F(set) -> set, P[set], Q[set] } : { 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 Fraenkel6'' { A() -> non empty set, B() -> non empty set , F(set,set) -> set, P[set,set], Q[set,set] } : { 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 FraenkelF'{ B() -> non empty set , F(set) -> set, G(set) -> set, P[set] } : { 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 FraenkelF'R{ B() -> non empty set , F(set) -> set, G(set) -> set, P[set] } : { 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 FraenkelF'' { A() -> non empty set, B() -> non empty set, F(set,set) -> set, G(set,set) -> set, P[set,set] } : { 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 FraenkelF6'' { A() -> non empty set, B() -> non empty set , F(set,set) -> set, P[set,set], Q[set,set] } : { 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); canceled 2; theorem :: FRAENKEL:3 for A,B being non empty 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; canceled; theorem :: FRAENKEL:5 for A,B being set holds Funcs(A,B) c= bool [:A,B:]; theorem :: FRAENKEL:6 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 RelevantArgs { A() -> non empty set, B() -> non empty set, X() -> set, f() -> (Function of A(),B()), g() -> (Function of A(),B()), P[set], Q[set] } : { f().u' where u' is Element of A() : P[u'] & u' in X() } = { g().v' where v' is Element of A() : Q[v'] & v' 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 Fr_Set0{ A() -> non empty set, P[set] }: { x where x is Element of A(): P[x] } c= A(); scheme Gen1''{A() -> non empty set, B() -> non empty set, F(set,set) -> set, P[set, set], Q[set] } : for s being (Element of A()), t being Element of B() st P[s,t] holds Q[F(s,t)] provided for s_t being set st s_t in { F(s1,t1) where s1 is (Element of A()), t1 is Element of B(): P[s1,t1] } holds Q[s_t]; scheme Gen1''A{A() -> non empty set, B() -> non empty set, F(set,set) -> set, P[set, set], Q[set] } : for s_t being set st s_t in { F(s1,t1) where s1 is (Element of A()), t1 is Element of B(): P[s1,t1] } holds Q[s_t] provided for s being (Element of A()), t being Element of B() st P[s,t] holds Q[F(s,t)]; scheme Gen2''{A() -> non empty set, B() -> non empty set, C() -> non empty set, F(set,set) -> (Element of C()), P[set, set], Q[set] } : { s_t where s_t is Element of C() : s_t in { F(s1,t1) where s1 is (Element of A()), t1 is Element of B() : P[s1,t1] } & Q[s_t] } = { F(s2,t2) where s2 is (Element of A()), t2 is Element of B() : P[s2,t2] & Q[F(s2,t2)]}; scheme Gen3'{A() -> non empty set, F(set) -> set, P[set], Q[set] } : { 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 Gen3''{A() -> non empty set, B() -> non empty set, F(set,set) -> set, P[set, set], Q[set] } : { 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 Gen4''{A() -> non empty set, B() -> non empty set, F(set,set) -> set, P[set, set], Q[set,set] } : { 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 s' being Element of A() st Q[s',t] & F(s,t) = F(s',t); scheme FrSet_1{ D() -> non empty set, A() -> set, P[set], F(set) -> set }: { F(y) where y is Element of D() : F(y) in A() & P[y] } c= A(); scheme FrSet_2{ D() -> non empty set, A() -> set, Q[set], F(set) -> set }: { F(y) where y is Element of D() : Q[y] & not F(y) in A() } misses A(); scheme FrEqua1{ A()-> non empty set, B() -> non empty set, F(set,set) -> set, x() -> (Element of B()), P[set,set], Q[set,set] }: { F(s,t) where s is (Element of A()), t is Element of B(): Q[s,t] } = { F(s',x()) where s' is Element of A(): P[s',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 FrEqua2{ A()-> non empty set, B() -> non empty set, F(set,set) -> set, x() -> (Element of B()), P[set,set] }: { F(s,t) where s is (Element of A()), t is Element of B(): t = x() & P[s,t] } = { F(s',x()) where s' is Element of A(): P[s',x()] }; :: dziedziny funkcji definition let IT be set; attr IT is functional means :: FRAENKEL:def 1 for x being set st x in IT holds x is Function; end; definition cluster non empty functional set; end; definition let P be functional set; cluster -> Function-like Relation-like Element of P; end; canceled; theorem :: FRAENKEL:8 for f being Function holds { f } is functional; definition let A, B be set; cluster Funcs(A,B) -> functional; end; definition let A, B be set; mode FUNCTION_DOMAIN of A,B -> functional non empty set means :: FRAENKEL:def 2 for x being Element of it holds x is Function of A,B; end; canceled; theorem :: FRAENKEL:10 for f being Function of A,C holds { f } is FUNCTION_DOMAIN of A,C; theorem :: FRAENKEL:11 Funcs(A,B) is FUNCTION_DOMAIN of A,B; definition let A be set, B be non empty set; redefine func Funcs(A,B) -> FUNCTION_DOMAIN of A,B; let F be FUNCTION_DOMAIN of A,B; mode Element of F -> Function of A,B; end; reserve phi for Element of Funcs(A,B); canceled 2; theorem :: FRAENKEL:14 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:15 for X being set, phi holds phi|X = phi|(A /\ X); :: Zbiory skonczone scheme FraenkelFin { A() ->non empty set, X() -> set, F(set) -> set }: { F(w) where w is Element of A(): w in X() } is finite provided X() is finite; scheme CartFin { A, B() -> non empty set, X, Y() -> set, F(set, set) -> set }: { 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 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 Fin_Im{A() ->non empty set, B()->non empty set , x()-> (Element of Fin B()), F(set)->(Element of A()), P[set,set]}: ex c1 being Element of Fin A() st for t being Element of A() holds t in c1 iff ex t' being Element of B() st t' in x() & t = F(t') & P[t,t']; theorem :: FRAENKEL:16 for A,B being set st A is finite & B is finite holds Funcs(A,B) is finite; scheme ImFin { A() -> non empty set, B() -> non empty set, X() -> set, Y() -> set, F(set) -> set } : { F(phi') where phi' is Element of Funcs(A(),B()): phi'.: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 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 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];

Back to top