Volume 11, 1999

University of Bialystok

Copyright (c) 1999 Association of Mizar Users

### The abstract of the Mizar article:

### Function Spaces in the Category of Directed Suprema Preserving Maps

**by****Grzegorz Bancerek, and****Adam Naumowicz**- Received November 26, 1999
- MML identifier: WAYBEL27

- [ Mizar article, MML identifier index ]

environ vocabulary FUNCT_1, RELAT_1, PRALG_1, FUNCT_5, PRALG_2, BOOLE, FUNCT_2, PBOOLE, FRAENKEL, MCART_1, MONOID_0, ORDERS_1, GROUP_1, BHSP_3, WAYBEL_0, YELLOW_0, BINOP_1, PRE_TOPC, GROUP_6, SEQM_3, CAT_1, FUNCT_3, CARD_3, FUNCOP_1, YELLOW_1, RLVECT_2, WAYBEL26, WAYBEL25, WAYBEL24, ORDINAL2, WELLORD2, WELLORD1, RELAT_2, WAYBEL11, WAYBEL_9, WAYBEL17, QUANTAL1, YELLOW_9, LATTICES, WAYBEL18, PROB_1, SUBSET_1, WAYBEL_1, WAYBEL_8, BORSUK_1, WAYBEL27, RLVECT_3; notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, TOLER_1, FRAENKEL, MCART_1, RELAT_1, FUNCT_1, PARTFUN1, FUNCT_3, FUNCT_4, FUNCT_5, CARD_3, MONOID_0, PRALG_1, PBOOLE, PRE_CIRC, QUANTAL1, PRALG_2, STRUCT_0, PRE_TOPC, GRCAT_1, FUNCT_2, TOPS_2, ORDERS_1, CANTOR_1, LATTICE3, YELLOW_0, WAYBEL_0, YELLOW_1, YELLOW_2, WAYBEL_1, YELLOW_3, WAYBEL_3, WAYBEL_8, WAYBEL_9, WAYBEL11, YELLOW_9, WAYBEL17, WAYBEL18, WAYBEL24, WAYBEL25, YELLOW16, WAYBEL26; constructors ORDERS_3, WAYBEL_8, YELLOW_9, WAYBEL17, WAYBEL18, WAYBEL26, WAYBEL24, GRCAT_1, ENUMSET1, QUANTAL1, T_0TOPSP, TOPS_2, WAYBEL_5, CANTOR_1, WAYBEL_1, WAYBEL_6, PRALG_2, TOLER_1, YELLOW16, MONOID_0; clusters RELSET_1, RELAT_1, FUNCT_1, PRALG_1, SUBSET_1, STRUCT_0, LATTICE3, TOPS_1, WAYBEL14, MONOID_0, YELLOW_0, WAYBEL_0, YELLOW_1, YELLOW_2, YELLOW_3, WAYBEL_1, WAYBEL_2, WAYBEL_8, WAYBEL10, FUNCT_2, WAYBEL17, WAYBEL18, YELLOW16, WAYBEL24, WAYBEL25, FRAENKEL, YELLOW_9, PARTFUN1; requirements BOOLE, SUBSET; begin definition let F be Function; attr F is uncurrying means :: WAYBEL27:def 1 (for x being set st x in dom F holds x is Function-yielding Function) & for f being Function st f in dom F holds F.f = uncurry f; attr F is currying means :: WAYBEL27:def 2 (for x being set st x in dom F holds x is Function & proj1 x is Relation) & for f being Function st f in dom F holds F.f = curry f; attr F is commuting means :: WAYBEL27:def 3 (for x being set st x in dom F holds x is Function-yielding Function) & for f being Function st f in dom F holds F.f = commute f; end; definition cluster empty -> uncurrying currying commuting Function; end; definition cluster uncurrying currying commuting Function; end; definition let F be uncurrying Function, X be set; cluster F|X -> uncurrying; end; definition let F be currying Function, X be set; cluster F|X -> currying; end; theorem :: WAYBEL27:1 for X,Y,Z,D being set st D c= Funcs(X, Funcs(Y,Z)) ex F being ManySortedSet of D st F is uncurrying & rng F c= Funcs([:X,Y:], Z); theorem :: WAYBEL27:2 for X,Y,Z,D being set st D c= Funcs([:X,Y:], Z) ex F being ManySortedSet of D st F is currying & ((Y = {} implies X = {}) implies rng F c= Funcs(X, Funcs(Y, Z))); definition let X,Y,Z be set; cluster uncurrying ManySortedSet of Funcs(X, Funcs(Y, Z)); cluster currying ManySortedSet of Funcs([:X, Y:], Z); end; theorem :: WAYBEL27:3 for A,B being non empty set, C being set for f,g being commuting Function st dom f c= Funcs(A, Funcs(B, C)) & rng f c= dom g holds g*f = id dom f; theorem :: WAYBEL27:4 for B being non empty set, A,C being set for f being uncurrying Function for g being currying Function st dom f c= Funcs(A, Funcs(B, C)) & rng f c= dom g holds g*f = id dom f; theorem :: WAYBEL27:5 for A,B,C being set for f being currying Function for g being uncurrying Function st dom f c= Funcs([:A, B:], C) & rng f c= dom g holds g*f = id dom f; theorem :: WAYBEL27:6 for f being Function-yielding Function for i,A being set st i in dom commute f holds ((commute f).i).:A c= pi(f.:A, i); theorem :: WAYBEL27:7 for f being Function-yielding Function for i,A being set st for g being Function st g in f.:A holds i in dom g holds pi(f.:A, i) c= ((commute f).i).:A; theorem :: WAYBEL27:8 for X,Y being set, f being Function st rng f c= Funcs(X, Y) for i,A being set st i in X holds ((commute f).i).:A = pi(f.:A, i); theorem :: WAYBEL27:9 for f being Function for i,A being set st [:A,{i}:] c= dom f holds pi((curry f).:A, i) = f.:[:A,{i}:]; definition let X be set; let Y be non empty functional set; cluster -> Function-yielding Function of X, Y; end; definition let T be constituted-Functions 1-sorted; cluster the carrier of T -> functional; end; definition let X be set; let L be non empty RelStr; cluster L|^X -> constituted-Functions; end; definition cluster constituted-Functions complete strict LATTICE; cluster constituted-Functions non empty 1-sorted; end; definition let T be constituted-Functions non empty RelStr; cluster -> constituted-Functions (non empty SubRelStr of T); end; theorem :: WAYBEL27:10 for S,T being complete LATTICE for f being idempotent map of T,T for h being map of S, Image f holds f*h = h; theorem :: WAYBEL27:11 for S being non empty RelStr for T,T1 being non empty RelStr st T is SubRelStr of T1 for f being map of S, T for f1 being map of S, T1 holds f is monotone & f=f1 implies f1 is monotone; theorem :: WAYBEL27:12 for S being non empty RelStr for T,T1 being non empty RelStr st T is full SubRelStr of T1 for f being map of S, T for f1 being map of S, T1 holds f1 is monotone & f=f1 implies f is monotone; theorem :: WAYBEL27:13 for X being set, V being Subset of X holds chi(V,X)"{1} = V & chi(V,X)"{0} = X\V; begin definition let X be non empty set; let T be non empty RelStr; let f be Element of T|^X; let x be Element of X; redefine func f.x -> Element of T; end; theorem :: WAYBEL27:14 for X being non empty set, T being non empty RelStr for f,g being Element of T|^X holds f <= g iff for x being Element of X holds f.x <= g.x; theorem :: WAYBEL27:15 for X being set for L,S being non empty RelStr st the RelStr of L = the RelStr of S holds L|^X = S|^X; theorem :: WAYBEL27:16 for S1,S2,T1,T2 being non empty TopSpace st the TopStruct of S1 = the TopStruct of S2 & the TopStruct of T1 = the TopStruct of T2 holds oContMaps(S1, T1) = oContMaps(S2, T2); theorem :: WAYBEL27:17 for X being set ex f being map of BoolePoset X, (BoolePoset 1)|^X st f is isomorphic & for Y being Subset of X holds f.Y = chi(Y,X); theorem :: WAYBEL27:18 for X being set holds BoolePoset X, (BoolePoset 1)|^X are_isomorphic; theorem :: WAYBEL27:19 for X,Y being non empty set, T being non empty Poset for S1 being full non empty SubRelStr of (T|^X)|^Y for S2 being full non empty SubRelStr of (T|^Y)|^X for F being map of S1, S2 st F is commuting holds F is monotone; theorem :: WAYBEL27:20 for X,Y being non empty set, T being non empty Poset for S1 being full non empty SubRelStr of (T|^Y)|^X for S2 being full non empty SubRelStr of T|^[:X,Y:] for F being map of S1, S2 st F is uncurrying holds F is monotone; theorem :: WAYBEL27:21 for X,Y being non empty set, T being non empty Poset for S1 being full non empty SubRelStr of (T|^Y)|^X for S2 being full non empty SubRelStr of T|^[:X,Y:] for F being map of S2, S1 st F is currying holds F is monotone; begin :: Again poset of continuous maps definition :: To moze byc rewizja w WAYBEL17 na SCMaps let S be non empty RelStr; let T be non empty reflexive antisymmetric RelStr; func UPS(S, T) -> strict RelStr means :: WAYBEL27:def 4 it is full SubRelStr of T |^ the carrier of S & for x being set holds x in the carrier of it iff x is directed-sups-preserving map of S, T; end; definition let S be non empty RelStr; let T be non empty reflexive antisymmetric RelStr; cluster UPS(S, T) -> non empty reflexive antisymmetric constituted-Functions; end; definition let S be non empty RelStr; let T be non empty Poset; cluster UPS(S,T) -> transitive; end; theorem :: WAYBEL27:22 for S being non empty RelStr for T being non empty reflexive antisymmetric RelStr holds the carrier of UPS(S, T) c= Funcs(the carrier of S, the carrier of T); definition let S be non empty RelStr; let T be non empty reflexive antisymmetric RelStr; let f be Element of UPS(S, T); let s be Element of S; redefine func f.s -> Element of T; end; theorem :: WAYBEL27:23 for S being non empty RelStr for T being non empty reflexive antisymmetric RelStr for f,g being Element of UPS(S, T) holds f <= g iff for s being Element of S holds f.s <= g.s; theorem :: WAYBEL27:24 for S,T being complete Scott TopLattice holds UPS(S,T) = SCMaps(S,T); theorem :: WAYBEL27:25 for S,S' being non empty RelStr for T,T' being non empty reflexive antisymmetric RelStr st the RelStr of S = the RelStr of S' & the RelStr of T = the RelStr of T' holds UPS(S,T) = UPS(S',T'); definition let S, T be complete LATTICE; cluster UPS(S, T) -> complete; end; theorem :: WAYBEL27:26 for S,T being complete LATTICE holds UPS(S, T) is sups-inheriting SubRelStr of T|^the carrier of S; theorem :: WAYBEL27:27 for S,T being complete LATTICE for A being Subset of UPS(S, T) holds sup A = "\/"(A, T|^the carrier of S); definition let S1,S2,T1,T2 be non empty reflexive antisymmetric RelStr; let f be map of S1, S2 such that f is directed-sups-preserving; let g be map of T1, T2 such that g is directed-sups-preserving; func UPS(f,g) -> map of UPS(S2, T1), UPS(S1, T2) means :: WAYBEL27:def 5 for h being directed-sups-preserving map of S2, T1 holds it.h = g*h*f; end; :: 2.6. PROPOSITOION, p. 115 :: preservation of composition theorem :: WAYBEL27:28 for S1,S2,S3, T1,T2,T3 being non empty Poset for f1 being directed-sups-preserving map of S2, S3 for f2 being directed-sups-preserving map of S1, S2 for g1 being directed-sups-preserving map of T1, T2 for g2 being directed-sups-preserving map of T2, T3 holds UPS(f2, g2) * UPS(f1, g1) = UPS(f1*f2, g2*g1); :: 2.6. PROPOSITOION, p. 115 :: preservation of identities theorem :: WAYBEL27:29 for S,T being non empty reflexive antisymmetric RelStr holds UPS(id S, id T) = id UPS(S, T); :: 2.6. PROPOSITOION, p. 115 :: preservation of directed-sups theorem :: WAYBEL27:30 for S1,S2, T1,T2 being complete LATTICE for f being directed-sups-preserving map of S1, S2 for g being directed-sups-preserving map of T1, T2 holds UPS(f, g) is directed-sups-preserving; theorem :: WAYBEL27:31 Omega Sierpinski_Space is Scott; theorem :: WAYBEL27:32 for S being complete Scott TopLattice holds oContMaps(S, Sierpinski_Space) = UPS(S, BoolePoset 1); :: 2.7. LEMMA, p. 116 theorem :: WAYBEL27:33 for S being complete LATTICE ex F being map of UPS(S, BoolePoset 1), InclPoset sigma S st F is isomorphic & for f being directed-sups-preserving map of S, BoolePoset 1 holds F.f = f"{1}; theorem :: WAYBEL27:34 for S being complete LATTICE holds UPS(S, BoolePoset 1), InclPoset sigma S are_isomorphic; theorem :: WAYBEL27:35 for S1, S2, T1, T2 being complete LATTICE for f being map of S1, S2, g being map of T1, T2 st f is isomorphic & g is isomorphic holds UPS(f, g) is isomorphic; theorem :: WAYBEL27:36 for S1, S2, T1, T2 being complete LATTICE st S1, S2 are_isomorphic & T1, T2 are_isomorphic holds UPS(S2, T1), UPS(S1, T2) are_isomorphic; theorem :: WAYBEL27:37 for S,T being complete LATTICE for f being directed-sups-preserving projection map of T,T holds Image UPS(id S, f) = UPS(S, Image f); theorem :: WAYBEL27:38 for X being non empty set, S,T being non empty Poset for f being directed-sups-preserving map of S, T|^X for i being Element of X holds (commute f).i is directed-sups-preserving map of S, T; theorem :: WAYBEL27:39 for X being non empty set, S,T being non empty Poset for f being directed-sups-preserving map of S, T|^X holds commute f is Function of X, the carrier of UPS(S, T); theorem :: WAYBEL27:40 for X being non empty set, S,T being non empty Poset for f being Function of X, the carrier of UPS(S, T) holds commute f is directed-sups-preserving map of S, T|^X; theorem :: WAYBEL27:41 for X being non empty set, S,T being non empty Poset ex F being map of UPS(S, T|^X), UPS(S, T)|^X st F is commuting isomorphic; theorem :: WAYBEL27:42 for X being non empty set, S,T being non empty Poset holds UPS(S, T|^X), UPS(S, T)|^X are_isomorphic; :: 2.8. THEOREM, p. 116 :: [CONT -> CONT] is into CONT (so [CONT -> CONT] is functor) theorem :: WAYBEL27:43 for S,T being continuous complete LATTICE holds UPS(S,T) is continuous; :: 2.8. THEOREM, p. 116 :: [ALG -> ALG] is into ALG (so [ALG -> ALG] is functor) theorem :: WAYBEL27:44 for S,T being algebraic complete LATTICE holds UPS(S,T) is algebraic; theorem :: WAYBEL27:45 for R,S,T being complete LATTICE for f being directed-sups-preserving map of R, UPS(S, T) holds uncurry f is directed-sups-preserving map of [:R,S:], T; theorem :: WAYBEL27:46 for R,S,T being complete LATTICE for f being directed-sups-preserving map of [:R,S:], T holds curry f is directed-sups-preserving map of R, UPS(S, T); :: 2.10. THEOREM, p. 117 theorem :: WAYBEL27:47 for R,S,T being complete LATTICE ex f being map of UPS(R, UPS(S, T)), UPS([:R,S:], T) st f is uncurrying isomorphic;

Back to top