:: Function Spaces in the Category of Directed Suprema Preserving Maps :: by Grzegorz Bancerek and Adam Naumowicz :: :: Received November 26, 1999 :: Copyright (c) 1999-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, RELAT_1, FUNCOP_1, FUNCT_5, FUNCT_6, XBOOLE_0, TARSKI, FUNCT_2, PBOOLE, ZFMISC_1, SUBSET_1, CARD_3, MCART_1, MONOID_0, STRUCT_0, REWRITE1, WAYBEL_0, NEWTON, ORDERS_2, YELLOW_0, BINOP_1, GROUP_6, SEQM_3, XXREAL_0, CAT_1, FUNCT_3, CARD_1, YELLOW_1, RLVECT_2, PRE_TOPC, WAYBEL26, WAYBEL24, WAYBEL25, ORDINAL2, RCOMP_1, WELLORD2, WELLORD1, RELAT_2, WAYBEL11, WAYBEL_9, WAYBEL17, YELLOW_9, EQREL_1, WAYBEL18, PROB_1, WAYBEL_1, WAYBEL_8, RLVECT_3, LATTICES, BORSUK_1, WAYBEL27; notations TARSKI, XBOOLE_0, ZFMISC_1, XTUPLE_0, SUBSET_1, TOLER_1, MCART_1, RELAT_1, FUNCT_1, PBOOLE, RELSET_1, PARTFUN1, BINOP_1, FUNCT_3, FUNCT_4, FUNCT_5, ORDINAL1, NUMBERS, CARD_3, FUNCOP_1, FUNCT_6, ORDERS_1, MONOID_0, PRALG_1, QUANTAL1, FUNCT_2, DOMAIN_1, STRUCT_0, PRE_TOPC, TOPS_2, ORDERS_2, 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 DOMAIN_1, TOLER_1, FUNCT_6, TOPS_2, CANTOR_1, MONOID_0, QUANTAL1, ORDERS_3, WAYBEL_6, WAYBEL_8, WAYBEL17, YELLOW_9, WAYBEL18, WAYBEL24, YELLOW16, WAYBEL26, RELSET_1, WAYBEL20, FUNCT_5, XTUPLE_0; registrations XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1, FUNCT_2, FUNCOP_1, STRUCT_0, TOPS_1, LATTICE3, YELLOW_0, MONOID_0, WAYBEL_0, YELLOW_1, YELLOW_2, WAYBEL_1, YELLOW_3, WAYBEL_2, WAYBEL_3, WAYBEL_8, WAYBEL10, WAYBEL14, WAYBEL17, YELLOW_9, WAYBEL18, WAYBEL19, WAYBEL24, WAYBEL25, YELLOW16, RELSET_1, XTUPLE_0, FUNCT_5; requirements BOOLE, SUBSET, NUMERALS; 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; registration cluster empty -> uncurrying currying commuting for Function; end; registration cluster uncurrying currying commuting for Function; end; registration let F be uncurrying Function, X be set; cluster F|X -> uncurrying; end; registration 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))); registration let X,Y,Z be set; cluster uncurrying for ManySortedSet of Funcs(X, Funcs(Y, Z)); cluster currying for 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}:]; registration let T be constituted-Functions 1-sorted; cluster the carrier of T -> functional; end; registration cluster constituted-Functions complete strict for LATTICE; cluster constituted-Functions non empty for 1-sorted; end; registration let T be constituted-Functions non empty RelStr; cluster -> constituted-Functions for non empty SubRelStr of T; end; theorem :: WAYBEL27:10 for S,T being complete LATTICE for f being idempotent Function of T,T for h being Function 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 Function of S, T for f1 being Function 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 Function of S, T for f1 being Function 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 Function of BoolePoset X, (BoolePoset {0})|^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{0})|^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 Function 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 Function 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 Function of S2, S1 st F is currying holds F is monotone; begin :: Again poset of continuous maps definition 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 Function of S, T; end; registration 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; registration 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,S9 being non empty RelStr for T,T9 being non empty reflexive antisymmetric RelStr st the RelStr of S = the RelStr of S9 & the RelStr of T = the RelStr of T9 holds UPS(S,T) = UPS(S9,T9); registration 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 Function of S1, S2 such that f is directed-sups-preserving; let g be Function of T1, T2 such that g is directed-sups-preserving; func UPS(f,g) -> Function of UPS(S2, T1), UPS(S1, T2) means :: WAYBEL27:def 5 for h being directed-sups-preserving Function 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 Function of S2, S3 for f2 being directed-sups-preserving Function of S1, S2 for g1 being directed-sups-preserving Function of T1, T2 for g2 being directed-sups-preserving Function 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 Function of S1, S2 for g being directed-sups-preserving Function 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{0}); :: 2.7. LEMMA, p. 116 theorem :: WAYBEL27:33 for S being complete LATTICE ex F being Function of UPS(S, BoolePoset{0}), InclPoset sigma S st F is isomorphic & for f being directed-sups-preserving Function of S, BoolePoset{0} holds F.f = f"{1}; theorem :: WAYBEL27:34 for S being complete LATTICE holds UPS(S, BoolePoset{0}), InclPoset sigma S are_isomorphic; theorem :: WAYBEL27:35 for S1, S2, T1, T2 being complete LATTICE for f being Function of S1, S2, g being Function 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 Function 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 Function of S, T|^X for i being Element of X holds ( commute f).i is directed-sups-preserving Function of S, T; theorem :: WAYBEL27:39 for X being non empty set, S,T being non empty Poset for f being directed-sups-preserving Function 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 Function of S, T|^X; theorem :: WAYBEL27:41 for X being non empty set, S,T being non empty Poset ex F being Function 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 Function of R, UPS(S, T) holds uncurry f is directed-sups-preserving Function of [:R,S:], T; theorem :: WAYBEL27:46 for R,S,T being complete LATTICE for f being directed-sups-preserving Function of [:R,S:], T holds curry f is directed-sups-preserving Function of R, UPS(S, T); :: 2.10. THEOREM, p. 117 theorem :: WAYBEL27:47 for R,S,T being complete LATTICE ex f being Function of UPS(R, UPS(S, T)), UPS([:R,S:], T) st f is uncurrying isomorphic;