Volume 10, 1998

University of Bialystok

Copyright (c) 1998 Association of Mizar Users

### The abstract of the Mizar article:

### Scott-Continuous Functions

**by****Adam Grabowski**- Received February 13, 1998
- MML identifier: WAYBEL17

- [ Mizar article, MML identifier index ]

environ vocabulary FUNCT_1, RELAT_1, WAYBEL_9, WAYBEL_0, RELAT_2, ORDERS_1, PRE_TOPC, SEQM_3, BOOLE, WAYBEL11, QUANTAL1, YELLOW_0, LATTICE3, ORDINAL2, FUNCOP_1, WAYBEL_3, BHSP_3, GROUP_1, CARD_3, CAT_1, YELLOW_1, FUNCT_2, SUBSET_1, LATTICES, WELLORD1, YELLOW_2, CANTOR_1, SETFAM_1, TOPS_1, TARSKI, WAYBEL_8, COMPTS_1, WAYBEL17, RLVECT_3; notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, NUMBERS, XREAL_0, NAT_1, RELSET_1, RELAT_1, STRUCT_0, FUNCT_1, PARTFUN1, FUNCT_2, PRE_TOPC, TOPS_1, TOLER_1, ORDERS_1, LATTICE3, YELLOW_0, ORDERS_3, WAYBEL_0, YELLOW_1, YELLOW_2, NATTRA_1, WAYBEL_3, PRE_CIRC, WAYBEL_8, WAYBEL_9, WAYBEL11, WAYBEL_2, CANTOR_1, YELLOW_8; constructors NAT_1, TOPS_1, ORDERS_3, WAYBEL_3, WAYBEL_5, TOLER_1, NATTRA_1, WAYBEL_8, WAYBEL_1, WAYBEL11, ABIAN, YELLOW_8, CANTOR_1, INT_1, LATTICE3, MEMBERED; clusters SUBSET_1, STRUCT_0, WAYBEL_0, WAYBEL_2, WAYBEL_3, RELSET_1, YELLOW_1, WAYBEL_9, LATTICE3, BORSUK_2, INT_1, WAYBEL10, WAYBEL11, ABIAN, MEMBERED, ZFMISC_1, FUNCT_1, FUNCT_2, PARTFUN1, NUMBERS, ORDINAL2; requirements NUMERALS, BOOLE, SUBSET, ARITHM; begin :: Preliminaries definition let S be non empty set; let a, b be Element of S; func (a,b),... -> Function of NAT, S means :: WAYBEL17:def 1 for i being Nat holds ((ex k being Nat st i = 2*k) implies it.i = a) & ((not ex k being Nat st i = 2*k) implies it.i = b); end; theorem :: WAYBEL17:1 for S, T being non empty reflexive RelStr, f being map 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 map 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 map of S, T st f is directed-sups-preserving holds f is monotone; definition let S, T be reflexive antisymmetric non empty RelStr; cluster directed-sups-preserving -> monotone map of S, T; end; theorem :: WAYBEL17:4 for S, T being up-complete Scott TopLattice, f being map of S, T holds f is continuous implies f is monotone; definition let S, T be up-complete Scott TopLattice; cluster continuous -> monotone map of S, T; end; begin :: Poset of continuous maps definition let S be set; let T be reflexive RelStr; cluster S --> T -> reflexive-yielding; end; definition 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 map of S, T holds f in the carrier of it iff f is continuous; end; definition 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, i', j' being Nat st i = i' & j = j' holds i <= j iff i' <= j'; end; definition 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), i', j' being Nat st i' = i & j' = i' + 1 & j' = 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 map 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); definition 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; definition let S be non empty reflexive transitive RelStr; let D be directed non empty Subset of S; cluster Net-Str D -> transitive; end; definition 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 map of S, T holds (for N being net of S holds f.(lim_inf N) <= lim_inf (f*N)) implies f is monotone; theorem :: WAYBEL17:12 for S, T being continuous lower-bounded LATTICE, f being map 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 map 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 map 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 map 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 map 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 map 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 map of S, T, N being monotone (non empty NetStr over S) holds f is monotone implies f * N is monotone; definition let S, T be up-complete LATTICE; let f be monotone map 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 map 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 map of S, T, N being net of S, j being Element of N, j' being Element of (f*N) st j' = 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 >= j'},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 map 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 map of S, T holds f is continuous iff f is directed-sups-preserving; definition let S, T be complete Scott TopLattice; cluster continuous -> directed-sups-preserving map of S, T; cluster directed-sups-preserving -> continuous map of S, T; end; :: Proposition 2.1, p. 112, (1) <=> (4) theorem :: WAYBEL17:23 for S, T being continuous complete Scott TopLattice, f being map 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 map 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 map 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 map 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 map 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 map 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 map of S, T holds f is directed-sups-preserving implies f is continuous;

Back to top