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;