:: Scott-Continuous Functions, Part II
:: by Adam Grabowski
::
:: Received June 22, 1999
:: Copyright (c) 1999-2018 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, RELAT_1;
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);