:: Scott-Continuous Functions
:: by Adam Grabowski
::
:: Received February 13, 1998
:: Copyright (c) 1998-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 XBOOLE_0, SUBSET_1, FUNCT_1, NUMBERS, RELAT_1, TARSKI, WAYBEL_9,
STRUCT_0, WAYBEL_0, RELAT_2, ORDERS_2, SEQM_3, XXREAL_0, WAYBEL11,
YELLOW_0, LATTICE3, ORDINAL2, PRE_TOPC, RCOMP_1, FUNCOP_1, WAYBEL_3,
REWRITE1, NEWTON, CARD_3, CAT_1, YELLOW_1, FUNCT_2, ARYTM_3, LATTICES,
WELLORD1, YELLOW_2, EQREL_1, CARD_FIL, RLVECT_3, ZFMISC_1, SETFAM_1,
YELLOW_8, TOPS_1, WAYBEL_8, WAYBEL17, NAT_1;
notations TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, NAT_1,
RELAT_1, SETFAM_1, FUNCT_1, RELSET_1, PARTFUN1, FUNCT_2, DOMAIN_1,
FUNCT_3, STRUCT_0, PRE_TOPC, TOPS_1, TOPS_2, TOLER_1, ORDERS_2, LATTICE3,
YELLOW_0, ORDERS_3, WAYBEL_0, YELLOW_1, YELLOW_2, WAYBEL_3, FUNCOP_1,
WAYBEL_8, WAYBEL_9, WAYBEL11, WAYBEL_2, CANTOR_1, YELLOW_8, XXREAL_0;
constructors DOMAIN_1, NAT_1, TOLER_1, ABIAN, TOPS_1, NATTRA_1, LATTICE3,
CANTOR_1, ORDERS_3, WAYBEL_1, WAYBEL_3, WAYBEL_8, YELLOW_8, WAYBEL11,
MEMBERED, RELSET_1, TOPS_2, WAYBEL_2;
registrations XBOOLE_0, SUBSET_1, FUNCT_1, ORDINAL1, FUNCT_2, FUNCOP_1,
MEMBERED, ABIAN, STRUCT_0, TOPS_1, LATTICE3, WAYBEL_0, YELLOW_1,
WAYBEL_2, WAYBEL_3, WAYBEL_9, WAYBEL10, WAYBEL11, PRE_TOPC, RELSET_1,
XXREAL_0, NAT_1;
requirements NUMERALS, BOOLE, SUBSET, ARITHM;
begin :: Preliminaries
definition
let S be non empty set;
let a, b be Element of S;
func (a,b),... -> sequence of S means
:: WAYBEL17:def 1
for i being Element of NAT holds
((ex k being Element of NAT st i = 2*k) implies it.i = a) &
((not ex k being Element of NAT st i = 2*k) implies it.i = b);
end;
scheme :: WAYBEL17:sch 1
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();
scheme :: WAYBEL17:sch 2
FuncFraenkelSL{ B, C() -> LATTICE,
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 :: WAYBEL17:1
for S, T being non empty reflexive RelStr, f being Function of S, T,
P being lower Subset of T st f is monotone holds f"P is lower;
theorem :: WAYBEL17:2
for S, T being non empty reflexive RelStr, f being Function of S, T,
P being upper Subset of T st f is monotone holds f"P is upper;
theorem :: WAYBEL17:3
for S, T being reflexive antisymmetric non empty RelStr,
f being Function of S, T st
f is directed-sups-preserving holds f is monotone;
registration
let S, T be reflexive antisymmetric non empty RelStr;
cluster directed-sups-preserving -> monotone for Function of S, T;
end;
theorem :: WAYBEL17:4
for S, T being up-complete Scott TopLattice,
f being Function of S, T holds f is continuous implies f is monotone;
registration
let S, T be up-complete Scott TopLattice;
cluster continuous -> monotone for Function of S, T;
end;
begin :: Poset of continuous maps
registration
let S be set;
let T be reflexive RelStr;
cluster S --> T -> reflexive-yielding;
end;
registration
let S be non empty set, T be complete LATTICE;
cluster T |^ S -> complete;
end;
definition
let S, T be up-complete Scott TopLattice;
func SCMaps (S,T) -> strict full SubRelStr of MonMaps (S, T) means
:: WAYBEL17:def 2
for f being Function of S, T holds f in the carrier of it iff
f is continuous;
end;
registration
let S, T be up-complete Scott TopLattice;
cluster SCMaps (S,T) -> non empty;
end;
begin :: Some special nets
definition
let S be non empty RelStr;
let a, b be Element of S;
func Net-Str (a,b) -> strict non empty NetStr over S means
:: WAYBEL17:def 3
the carrier of it = NAT & the mapping of it = (a,b),... &
for i, j being Element of it, i9, j9 being Element of NAT st i = i9 & j = j9
holds i <= j iff i9 <= j9;
end;
registration
let S be non empty RelStr;
let a, b be Element of S;
cluster Net-Str (a,b) -> reflexive transitive directed antisymmetric;
end;
theorem :: WAYBEL17:5
for S being non empty RelStr, a, b being Element of S,
i being Element of Net-Str (a, b) holds
Net-Str (a, b).i = a or Net-Str (a, b).i = b;
theorem :: WAYBEL17:6
for S being non empty RelStr, a, b being Element of S,
i, j being Element of Net-Str (a,b),
i9, j9 being Element of NAT st i9 = i & j9 = i9 + 1 & j9 = j holds
(Net-Str (a, b).i = a implies Net-Str (a, b).j = b) &
(Net-Str (a, b).i = b implies Net-Str (a, b).j = a);
theorem :: WAYBEL17:7
for S being with_infima Poset, a, b being Element of S holds
lim_inf Net-Str (a,b) = a "/\" b;
theorem :: WAYBEL17:8
for S, T being with_infima Poset, a, b being Element of S,
f being Function of S, T holds lim_inf (f*Net-Str (a,b)) = f.a "/\" f.b;
definition
let S be non empty RelStr;
let D be non empty Subset of S;
func Net-Str D -> strict NetStr over S equals
:: WAYBEL17:def 4
NetStr (#D, (the InternalRel of S)|_2 D, (id the carrier of S)|D#);
end;
theorem :: WAYBEL17:9
for S being non empty reflexive RelStr, D being non empty Subset of S holds
Net-Str D = Net-Str (D, (id the carrier of S)|D);
registration
let S be non empty reflexive RelStr;
let D be directed non empty Subset of S;
cluster Net-Str D -> non empty directed reflexive;
end;
registration
let S be non empty reflexive transitive RelStr;
let D be directed non empty Subset of S;
cluster Net-Str D -> transitive;
end;
registration
let S be non empty reflexive RelStr;
let D be directed non empty Subset of S;
cluster Net-Str D -> monotone;
end;
theorem :: WAYBEL17:10
for S being up-complete LATTICE,
D being directed non empty Subset of S holds lim_inf Net-Str D = sup D;
begin :: Monotone maps
theorem :: WAYBEL17:11
for S, T being LATTICE, f being Function of S, T holds
(for N being net of S holds f.(lim_inf N) <= lim_inf (f*N)) implies
f is monotone;
scheme :: WAYBEL17:sch 3
NetFraenkelS{B, B1, 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 B1(): P[x]}
provided
the carrier of C() c= dom f() and
the carrier of B() = the carrier of B1();
theorem :: WAYBEL17:12
for S, T being continuous lower-bounded LATTICE,
f being Function of S, T holds ( f is directed-sups-preserving implies
for x being Element of S holds
f.x = "\/"({ f.w where w is Element of S : w << x },T) );
theorem :: WAYBEL17:13
for S being LATTICE, T being up-complete lower-bounded LATTICE,
f being 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) ) implies
f is monotone);
theorem :: WAYBEL17:14
for S being up-complete lower-bounded LATTICE,
T being continuous lower-bounded LATTICE, f being 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) ) implies
for x being Element of S, y being Element of T
holds y << f.x iff ex w being Element of S st w << x & y << f.w );
theorem :: WAYBEL17:15
for S, T being non empty RelStr, D being Subset of S,
f being Function of S, T st ex_sup_of D,S & ex_sup_of f.:D,T or
S is complete antisymmetric & T is complete antisymmetric holds
f is monotone implies sup (f.:D) <= f.(sup D);
theorem :: WAYBEL17:16
for S, T being non empty reflexive antisymmetric RelStr,
D being directed non empty Subset of S, f being Function of S, T st
ex_sup_of D,S & ex_sup_of f.:D,T or
S is up-complete & T is up-complete holds
f is monotone implies sup (f.:D) <= f.(sup D);
theorem :: WAYBEL17:17
for S, T being non empty RelStr, D being Subset of S,
f being Function of S, T st ex_inf_of D,S & ex_inf_of f.:D,T or
S is complete antisymmetric & T is complete antisymmetric holds
f is monotone implies f.(inf D) <= inf (f.:D);
theorem :: WAYBEL17:18
for S, T being up-complete LATTICE, f being Function of S, T,
N being monotone non empty NetStr over S holds
f is monotone implies f * N is monotone;
registration
let S, T be up-complete LATTICE;
let f be monotone Function of S, T;
let N be monotone non empty NetStr over S;
cluster f * N -> monotone;
end;
theorem :: WAYBEL17:19
for S, T being up-complete LATTICE, f being Function of S, T holds
(for N being net of S holds f.(lim_inf N) <= lim_inf (f*N)) implies
for D being directed non empty Subset of S holds sup (f.:D) = f.(sup D);
theorem :: WAYBEL17:20
for S, T being complete LATTICE, f being Function of S, T, N being net of S,
j being Element of N, j9 being Element of (f*N) st j9 = j
holds f is monotone implies f."/\"({N.k where k is Element of N: k >= j},S)
<= "/\"({(f*N).l where l is Element of (f*N) : l >= j9},T);
begin :: Necessary and sufficient conditions of Scott-continuity
:: Proposition 2.1, p. 112, (1) <=> (2)
theorem :: WAYBEL17:21
for S, T being complete Scott TopLattice, f being Function of S, T holds
f is continuous iff for N be net of S holds f.(lim_inf N) <= lim_inf (f*N);
:: Proposition 2.1, p. 112, (1) <=> (3)
theorem :: WAYBEL17:22
for S, T being complete Scott TopLattice, f being Function of S, T holds
f is continuous iff f is directed-sups-preserving;
registration
let S, T be complete Scott TopLattice;
cluster continuous -> directed-sups-preserving for Function of S, T;
cluster directed-sups-preserving -> continuous for Function of S, T;
end;
:: Proposition 2.1, p. 112, (1) <=> (4)
theorem :: WAYBEL17:23
for S, T being continuous complete Scott TopLattice,
f being Function of S, T holds ( f is continuous iff
for x being Element of S, y being Element of T
holds y << f.x iff ex w being Element of S st w << x & y << f.w );
:: Proposition 2.1, p. 112, (1) <=> (5)
theorem :: WAYBEL17:24
for S, T being continuous complete Scott TopLattice,
f being Function of S, T holds ( f is continuous iff
for x being Element of S holds
f.x = "\/"({ f.w where w is Element of S : w << x },T) );
theorem :: WAYBEL17:25
for S being LATTICE, T being complete LATTICE,
f being Function of S, T holds ( for x being Element of S holds
f.x = "\/"({ f.w where w is Element of S : w <= x & w is compact },T ) )
implies f is monotone;
theorem :: WAYBEL17:26
for S, T being complete Scott TopLattice, f being Function of S, T holds
(( for x being Element of S holds
f.x = "\/"({ f.w where w is Element of S : w <= x & w is compact },T ) )
implies for x being Element of S holds
f.x = "\/"({ f.w where w is Element of S : w << x },T) );
:: Proposition 2.1, p. 112, (1) <=> (6)
theorem :: WAYBEL17:27
for S, T being complete Scott TopLattice, f being Function of S, T holds
S is algebraic & T is algebraic implies ( f is continuous iff
for x being Element of S, k being Element of T st
k in the carrier of CompactSublatt T
holds (k <= f.x iff ex j being Element of S st
j in the carrier of CompactSublatt S & j <= x & k <= f.j) );
:: Proposition 2.1, p. 112, (1) <=> (7)
theorem :: WAYBEL17:28
for S, T being complete Scott TopLattice, f being Function of S, T holds
S is algebraic & T is algebraic implies ( f is continuous iff
for x being Element of S holds
f.x = "\/"({ f.w where w is Element of S : w <= x & w is compact },T ) );
theorem :: WAYBEL17:29
for S, T being up-complete Scott non empty
reflexive transitive antisymmetric TopSpace-like TopRelStr,
f be Function of S, T holds
f is directed-sups-preserving implies f is continuous;