:: Scott-Continuous Functions, Part II :: by Adam Grabowski :: :: Received June 22, 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 WAYBEL_0, WAYBEL11, WAYBEL_9, SUBSET_1, WAYBEL17, EQREL_1, ORDINAL2, FUNCT_1, STRUCT_0, TARSKI, YELLOW_1, XBOOLE_0, ORDERS_2, RELAT_2, SEQM_3, XXREAL_0, RELAT_1, FUNCOP_1, LATTICES, LATTICE3, NEWTON, REWRITE1, YELLOW_0, FUNCT_2, ZFMISC_1, BORSUK_1, FUNCT_5, MCART_1, PRE_TOPC, CAT_1, MONOID_0, WAYBEL_3, PBOOLE, CARD_3, FUNCT_4, WAYBEL24; notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_1, FUNCT_1, RELSET_1, FUNCT_2, BINOP_1, DOMAIN_1, FUNCT_5, MONOID_0, CARD_3, PBOOLE, FUNCOP_1, STRUCT_0, PRE_TOPC, ORDERS_2, LATTICE3, FUNCT_7, YELLOW_0, ORDERS_3, WAYBEL_0, YELLOW_1, YELLOW_2, WAYBEL_3, WAYBEL_9, WAYBEL11, WAYBEL17, YELLOW_3; constructors FUNCT_7, BORSUK_1, MONOID_0, ORDERS_3, WAYBEL_1, WAYBEL_3, WAYBEL17, YELLOW_3, FUNCT_5; registrations XBOOLE_0, SUBSET_1, RELSET_1, FUNCT_2, STRUCT_0, LATTICE3, YELLOW_0, MONOID_0, WAYBEL_0, YELLOW_1, YELLOW_3, WAYBEL_3, WAYBEL10, WAYBEL11, WAYBEL17, PRE_TOPC; requirements SUBSET, BOOLE; begin :: Preliminaries theorem :: WAYBEL24:1 for S, T being up-complete Scott TopLattice for M being Subset of SCMaps (S,T) holds "\/" (M, SCMaps (S,T)) is continuous Function of S, T; registration let S be non empty RelStr, T be non empty reflexive RelStr; cluster constant -> monotone for Function of S, T; end; registration let S be non empty RelStr, T be reflexive non empty RelStr, a be Element of T; cluster S --> a -> monotone; end; theorem :: WAYBEL24:2 for S being non empty RelStr, T being lower-bounded antisymmetric reflexive non empty RelStr holds Bottom MonMaps(S, T) = S --> Bottom T; theorem :: WAYBEL24:3 for S being non empty RelStr, T being upper-bounded antisymmetric reflexive non empty RelStr holds Top MonMaps(S, T) = S --> Top T; scheme :: WAYBEL24:sch 1 FuncFraenkelSL{ B, C() -> non empty RelStr, A(set) -> Element of C(), f() -> Function, P[set]}: f().:{A(x) where x is Element of B(): P[x]} = {f().A(x) where x is Element of B(): P[x]} provided the carrier of C() c= dom f(); scheme :: WAYBEL24:sch 2 Fraenkel6A{ B() -> LATTICE, 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]; theorem :: WAYBEL24:4 for S, T being complete LATTICE, f being monotone Function of S, T holds for x being Element of S holds f.x = sup (f.:downarrow x); theorem :: WAYBEL24:5 for S, T being complete lower-bounded LATTICE, f being monotone Function of S, T holds for x being Element of S holds f.x = "\/"({ f.w where w is Element of S : w <= x },T); theorem :: WAYBEL24:6 for S being RelStr, T being non empty RelStr, F being Subset of ( T |^ the carrier of S) holds sup F is Function of S, T; begin :: On the Scott continuity of maps definition let X1, X2, Y be non empty RelStr; let f be Function of [:X1, X2:], Y; let x be Element of X1; func Proj (f, x) -> Function of X2, Y equals :: WAYBEL24:def 1 (curry f).x; end; reserve X1, X2, Y for non empty RelStr, f for Function of [:X1, X2:], Y, x for Element of X1, y for Element of X2; theorem :: WAYBEL24:7 for y being Element of X2 holds (Proj (f, x)). y = f.(x, y); definition let X1, X2, Y be non empty RelStr; let f be Function of [:X1, X2:], Y; let y be Element of X2; func Proj (f, y) -> Function of X1, Y equals :: WAYBEL24:def 2 (curry' f).y; end; theorem :: WAYBEL24:8 for x being Element of X1 holds (Proj (f, y)). x = f.(x, y); theorem :: WAYBEL24:9 for R, S, T being non empty RelStr, f being Function of [:R,S:], T, a being Element of R, b being Element of S holds Proj (f, a). b = Proj (f, b ). a; registration let S be non empty RelStr, T be non empty reflexive RelStr; cluster antitone for Function of S, T; end; theorem :: WAYBEL24:10 for R, S, T being non empty reflexive RelStr, f being Function of [:R,S:], T, a being Element of R, b being Element of S st f is monotone holds Proj (f, a) is monotone & Proj (f, b) is monotone; theorem :: WAYBEL24:11 for R, S, T being non empty reflexive RelStr, f being Function of [:R,S:], T, a being Element of R, b being Element of S st f is antitone holds Proj (f, a) is antitone & Proj (f, b) is antitone; registration let R, S, T be non empty reflexive RelStr; let f be monotone Function of [:R, S:], T; let a be Element of R; cluster Proj (f, a) -> monotone; end; registration let R, S, T be non empty reflexive RelStr; let f be monotone Function of [:R, S:], T; let b be Element of S; cluster Proj (f, b) -> monotone; end; registration let R, S, T be non empty reflexive RelStr; let f be antitone Function of [:R, S:], T; let a be Element of R; cluster Proj (f, a) -> antitone; end; registration let R, S, T be non empty reflexive RelStr; let f be antitone Function of [:R, S:], T; let b be Element of S; cluster Proj (f, b) -> antitone; end; theorem :: WAYBEL24:12 for R, S, T being LATTICE, f being Function of [:R,S:], T st ( for a being Element of R, b being Element of S holds Proj (f, a) is monotone & Proj (f, b) is monotone) holds f is monotone; theorem :: WAYBEL24:13 for R, S, T being LATTICE, f being Function of [:R,S:], T st ( for a being Element of R, b being Element of S holds Proj (f, a) is antitone & Proj ( f, b) is antitone) holds f is antitone; theorem :: WAYBEL24:14 for R, S, T being LATTICE, f being Function of [:R,S:], T, b being Element of S, X being Subset of R holds Proj (f, b).:X = f.:[:X, {b}:]; theorem :: WAYBEL24:15 for R, S, T being LATTICE, f being Function of [:R,S:], T, b being Element of R, X being Subset of S holds Proj (f, b).:X = f.:[:{b}, X:]; theorem :: WAYBEL24:16 :: Lemma 2.9 p. 116 (1) => (2) for R, S, T being LATTICE, f being Function of [:R,S:], T, a being Element of R, b being Element of S st f is directed-sups-preserving holds Proj (f, a) is directed-sups-preserving & Proj (f, b) is directed-sups-preserving; theorem :: WAYBEL24:17 for R, S, T being LATTICE, f being monotone Function of [:R, S:] , T, a being Element of R, b being Element of S, X being directed Subset of [:R , S:] st ex_sup_of f.:X, T & a in proj1 X & b in proj2 X holds f. [a, b] <= sup (f.:X); theorem :: WAYBEL24:18 :: Lemma 2.9 p. 116 (2) => (1) for R, S, T being complete LATTICE, f being Function of [:R, S:], T st ( for a being Element of R, b being Element of S holds Proj (f, a) is directed-sups-preserving & Proj (f, b) is directed-sups-preserving ) holds f is directed-sups-preserving; theorem :: WAYBEL24:19 for S being set, T being non empty RelStr, f be set holds f is Element of T |^ S iff f is Function of S, the carrier of T; begin :: The poset of continuous maps definition let S be TopStruct, T be non empty TopRelStr; func ContMaps (S, T) -> strict RelStr means :: WAYBEL24:def 3 it is full SubRelStr of T |^ the carrier of S & for x being set holds x in the carrier of it iff ex f being Function of S, T st x = f & f is continuous; end; registration let S be non empty TopSpace, T be non empty TopSpace-like TopRelStr; cluster ContMaps (S, T) -> non empty; end; registration let S be non empty TopSpace, T be non empty TopSpace-like TopRelStr; cluster ContMaps (S, T) -> constituted-Functions; end; theorem :: WAYBEL24:20 for S being non empty TopSpace, T being non empty reflexive TopSpace-like TopRelStr, x, y being Element of ContMaps (S, T) holds x <= y iff for i being Element of S holds [x.i, y.i] in the InternalRel of T; theorem :: WAYBEL24:21 for S being non empty TopSpace, T being non empty reflexive TopSpace-like TopRelStr, x being set holds x is continuous Function of S, T iff x is Element of ContMaps (S, T); registration let S be non empty TopSpace, T be non empty reflexive TopSpace-like TopRelStr; cluster ContMaps (S, T) -> reflexive; end; registration let S be non empty TopSpace, T be non empty transitive TopSpace-like TopRelStr; cluster ContMaps (S, T) -> transitive; end; registration let S be non empty TopSpace, T be non empty antisymmetric TopSpace-like TopRelStr; cluster ContMaps (S, T) -> antisymmetric; end; registration let S be set, T be non empty RelStr; cluster T |^ S -> constituted-Functions; end; theorem :: WAYBEL24:22 for S being non empty 1-sorted, T being complete LATTICE for f, g, h being Function of S, T, i being Element of S st h = "\/" ({f, g}, T |^ the carrier of S) holds h.i = sup {f.i, g.i}; theorem :: WAYBEL24:23 for I being non empty set for J being RelStr-yielding non-Empty reflexive-yielding ManySortedSet of I st for i being Element of I holds J.i is complete LATTICE for X being Subset of product J, i being Element of I holds ( inf X).i = inf pi(X,i); theorem :: WAYBEL24:24 for S being non empty 1-sorted, T being complete LATTICE for f, g, h being Function of S, T, i being Element of S st h = "/\" ({f, g}, T |^ the carrier of S) holds h.i = inf {f.i, g.i}; theorem :: WAYBEL24:25 for S being non empty RelStr, T being complete LATTICE for F being non empty Subset of (T |^ the carrier of S), i being Element of S holds ( sup F).i = "\/" ({ f.i where f is Element of (T |^ the carrier of S) : f in F } , T ); theorem :: WAYBEL24:26 for S, T being complete TopLattice for F being non empty Subset of ContMaps (S, T), i being Element of S holds "\/" (F, (T |^ the carrier of S) ).i = "\/" ({ f.i where f is Element of (T |^ the carrier of S) : f in F }, T ) ; reserve S for non empty RelStr, T for complete LATTICE; theorem :: WAYBEL24:27 for F being non empty Subset of (T |^ the carrier of S), D being non empty Subset of S holds (sup F).:D = { "\/" ({ f.i where f is Element of (T |^ the carrier of S) : f in F }, T ) where i is Element of S : i in D }; theorem :: WAYBEL24:28 for S, T being complete Scott TopLattice, F being non empty Subset of ContMaps (S, T), D being non empty Subset of S holds ("\/" (F, (T |^ the carrier of S))).:D = { "\/" ({ f.i where f is Element of (T |^ the carrier of S) : f in F }, T ) where i is Element of S : i in D }; scheme :: WAYBEL24:sch 3 FraenkelF9RS{ B() -> non empty TopRelStr, 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 :: WAYBEL24:sch 4 FraenkelF9RSS{ B() -> non empty RelStr, 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 :: WAYBEL24:sch 5 FuncFraenkelS{ B, C() -> non empty TopRelStr, A(set) -> Element of C(), f() -> Function, P[set]}: f().:{A(x) where x is Element of B(): P[x]} = {f().A(x) where x is Element of B(): P[x]} provided the carrier of C() c= dom f(); theorem :: WAYBEL24:29 for S, T being complete Scott TopLattice, F being non empty Subset of ContMaps (S, T) holds "\/" (F, (T |^ the carrier of S)) is monotone Function of S, T; theorem :: WAYBEL24:30 for S, T being complete Scott TopLattice, F being non empty Subset of ContMaps (S, T), D being directed non empty Subset of S holds "\/"({ "\/"({g.i where i is Element of S : i in D }, T ) where g is Element of (T |^ the carrier of S) : g in F }, T ) = "\/"({ "\/" ({g9.i9 where g9 is Element of (T |^ the carrier of S) : g9 in F }, T ) where i9 is Element of S : i9 in D }, T); theorem :: WAYBEL24:31 for S, T being complete Scott TopLattice, F being non empty Subset of ContMaps (S, T), D being directed non empty Subset of S holds "\/" (( "\/"(F, (T |^ the carrier of S))).:D, T) = "\/" (F, (T |^ the carrier of S)). sup D; theorem :: WAYBEL24:32 for S, T being complete Scott TopLattice, F being non empty Subset of ContMaps (S, T) holds "\/"(F, (T |^ the carrier of S)) in the carrier of ContMaps (S, T); theorem :: WAYBEL24:33 for S being non empty RelStr, T being lower-bounded antisymmetric non empty RelStr holds Bottom (T |^ the carrier of S) = S --> Bottom T; theorem :: WAYBEL24:34 for S being non empty RelStr, T being upper-bounded antisymmetric non empty RelStr holds Top (T |^ the carrier of S) = S --> Top T; registration let S be non empty reflexive RelStr, T be complete LATTICE, a be Element of T; cluster S --> a -> directed-sups-preserving; end; theorem :: WAYBEL24:35 :: Lemma 2.4, p. 115 for S, T being complete Scott TopLattice holds ContMaps (S, T) is sups-inheriting SubRelStr of (T |^ the carrier of S); registration let S, T be complete Scott TopLattice; cluster ContMaps (S, T) -> complete; end; theorem :: WAYBEL24:36 for S, T being non empty Scott complete TopLattice holds Bottom ContMaps (S, T) = S --> Bottom T; theorem :: WAYBEL24:37 for S, T being non empty Scott complete TopLattice holds Top ContMaps (S, T) = S --> Top T; theorem :: WAYBEL24:38 for S, T being Scott complete TopLattice holds SCMaps (S, T) = ContMaps (S, T);