:: Function Spaces in the Category of Directed Suprema Preserving Maps
:: by Grzegorz Bancerek and Adam Naumowicz
::
:: Received November 26, 1999
:: Copyright (c) 1999-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 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;