:: The Characterization of Continuity of Topologies :: by Grzegorz Bancerek and Adam Naumowicz :: :: Received January 6, 2000 :: Copyright (c) 2000-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 XBOOLE_0, ORDERS_2, YELLOW_0, NEWTON, ZFMISC_1, FUNCT_1, WAYBEL27, FUNCT_2, RELAT_1, STRUCT_0, SUBSET_1, FUNCOP_1, FUNCT_5, TARSKI, CAT_1, SEQM_3, XXREAL_0, PRE_TOPC, SETFAM_1, WAYBEL11, WAYBEL_0, WAYBEL19, WAYBEL24, EQREL_1, ORDINAL2, RCOMP_1, WAYBEL26, XBOOLEAN, CARD_3, LATTICE3, WAYBEL_9, FUNCTOR0, REWRITE1, YELLOW_9, YELLOW16, WAYBEL_3, PBOOLE, LATTICES, FINSET_1, FUNCT_4, RELAT_2, WAYBEL25, PRELAMB, CARD_FIL, YELLOW_1, T_0TOPSP, CONNSP_2, WELLORD1, LATTICE5, WAYBEL18, CARD_1, FUNCT_3, PROB_1, FUNCT_6, RLVECT_2, WELLORD2, RLVECT_3, TOPS_1, YELLOW_6, WAYBEL29; notations TARSKI, XBOOLE_0, ENUMSET1, ZFMISC_1, XTUPLE_0, SUBSET_1, SETFAM_1, RELAT_1, FUNCT_1, PBOOLE, RELSET_1, PARTFUN1, FUNCT_2, BINOP_1, FUNCT_3, FINSET_1, CARD_3, ORDINAL1, NUMBERS, FUNCT_6, FUNCOP_1, ORDERS_1, STRUCT_0, PRE_TOPC, TOPS_1, T_0TOPSP, CONNSP_2, CANTOR_1, FUNCT_4, FUNCT_5, FUNCT_7, PRALG_1, WELLORD1, ORDERS_2, LATTICE3, TOPS_2, YELLOW_0, WAYBEL_0, YELLOW_1, WAYBEL_1, YELLOW_3, WAYBEL_3, WAYBEL_5, WAYBEL_9, YELLOW_6, WAYBEL11, YELLOW_9, BORSUK_1, WAYBEL18, WAYBEL19, WAYBEL24, WAYBEL25, YELLOW16, WAYBEL26, WAYBEL27; constructors TOLER_1, FUNCT_7, TOPS_1, TOPS_2, BORSUK_1, T_0TOPSP, CANTOR_1, MONOID_0, ORDERS_3, WAYBEL_5, WAYBEL11, YELLOW_9, WAYBEL18, WAYBEL24, YELLOW16, WAYBEL26, WAYBEL27, WAYBEL20, XTUPLE_0; registrations SUBSET_1, FUNCT_1, FUNCT_2, FUNCOP_1, FINSET_1, STRUCT_0, PRE_TOPC, TOPS_1, BORSUK_1, LATTICE3, YELLOW_0, BORSUK_2, WAYBEL_0, YELLOW_1, WAYBEL_1, YELLOW_3, WAYBEL_3, WAYBEL10, WAYBEL11, WAYBEL14, YELLOW_9, WAYBEL18, WAYBEL19, TOPGRP_1, WAYBEL24, YELLOW14, WAYBEL25, YELLOW16, WAYBEL26, WAYBEL27, RELSET_1, FUNCT_5; requirements BOOLE, SUBSET; begin theorem :: WAYBEL29:1 for X,Y being non empty set, Z being non empty RelStr for S being non empty SubRelStr of Z|^[:X,Y:] for T being non empty SubRelStr of (Z|^Y)|^X for f being Function of S, T st f is currying one-to-one onto holds f" is uncurrying; theorem :: WAYBEL29:2 for X,Y being non empty set, Z being non empty RelStr for S being non empty SubRelStr of Z|^[:X,Y:] for T being non empty SubRelStr of (Z|^Y)|^X for f being Function of T, S st f is uncurrying one-to-one onto holds f" is currying; theorem :: WAYBEL29:3 for X,Y being non empty set, Z being non empty Poset for S being non empty full SubRelStr of Z|^[:X,Y:] for T being non empty full SubRelStr of (Z|^ Y)|^X for f being Function of S, T st f is currying one-to-one onto holds f is isomorphic; theorem :: WAYBEL29:4 for X,Y being non empty set, Z being non empty Poset for T being non empty full SubRelStr of Z|^[:X,Y:] for S being non empty full SubRelStr of (Z|^ Y)|^X for f being Function of S, T st f is uncurrying one-to-one onto holds f is isomorphic; theorem :: WAYBEL29:5 for S1, S2, T1, T2 being RelStr st the RelStr of S1 = the RelStr of S2 & the RelStr of T1 = the RelStr of T2 for f being Function of S1, T1 st f is isomorphic for g being Function of S2, T2 st g = f holds g is isomorphic; :: Przywlaszczone theorem :: WAYBEL29:6 :: stolen from WAYBEL_1:8 for R, S, T being RelStr for f being Function of R, S st f is isomorphic for g being Function of S, T st g is isomorphic for h being Function of R, T st h = g*f holds h is isomorphic; theorem :: WAYBEL29:7 for X,Y,X1,Y1 being TopSpace st the TopStruct of X = the TopStruct of X1 & the TopStruct of Y = the TopStruct of Y1 holds [:X,Y:] = [:X1 ,Y1:]; theorem :: WAYBEL29:8 for X being non empty TopSpace for L being Scott up-complete non empty TopPoset for F being non empty directed Subset of ContMaps(X, L) holds "\/"(F, L|^the carrier of X) is continuous Function of X, L; theorem :: WAYBEL29:9 for X being non empty TopSpace for L being Scott up-complete non empty TopPoset holds ContMaps(X, L) is directed-sups-inheriting SubRelStr of L|^the carrier of X; theorem :: WAYBEL29:10 for S1,S2 being TopStruct st the TopStruct of S1 = the TopStruct of S2 for T1,T2 being non empty TopRelStr st the TopRelStr of T1 = the TopRelStr of T2 holds ContMaps(S1,T1) = ContMaps(S2,T2); registration cluster Scott -> injective T_0 for complete continuous TopLattice; end; registration cluster Scott continuous complete for TopLattice; end; registration let X be non empty TopSpace; let L be Scott up-complete non empty TopPoset; cluster ContMaps(X, L) -> up-complete; end; theorem :: WAYBEL29:11 for I being non empty set for J being Poset-yielding non-Empty ManySortedSet of I st for i being Element of I holds J.i is up-complete holds I -POS_prod J is up-complete; theorem :: WAYBEL29:12 :: stolen (generalized) from WAYBEL_3:33 for I being non empty set for J being Poset-yielding non-Empty ManySortedSet of I st for i being Element of I holds J.i is up-complete lower-bounded for x,y being Element of product J holds x << y iff (for i being Element of I holds x .i << y.i) & ex K being finite Subset of I st for i being Element of I st not i in K holds x .i = Bottom (J.i); registration let X be set; let L be lower-bounded non empty reflexive antisymmetric RelStr; cluster L|^X -> lower-bounded; end; registration let X be non empty TopSpace; let L be lower-bounded non empty TopPoset; cluster ContMaps(X, L) -> lower-bounded; end; registration let L be up-complete non empty Poset; cluster -> up-complete for TopAugmentation of L; cluster Scott -> correct for TopAugmentation of L; end; registration let L be up-complete non empty Poset; cluster strict Scott for TopAugmentation of L; end; theorem :: WAYBEL29:13 for L being up-complete non empty Poset for S1, S2 being Scott TopAugmentation of L holds the topology of S1 = the topology of S2; theorem :: WAYBEL29:14 for S1, S2 being up-complete antisymmetric non empty reflexive TopRelStr st the TopRelStr of S1 = the TopRelStr of S2 & S1 is Scott holds S2 is Scott; definition let L be up-complete non empty Poset; func Sigma L -> strict Scott TopAugmentation of L means :: WAYBEL29:def 1 not contradiction; end; theorem :: WAYBEL29:15 for S being Scott up-complete non empty TopPoset holds Sigma S = the TopRelStr of S; theorem :: WAYBEL29:16 for L1, L2 being up-complete non empty Poset st the RelStr of L1 = the RelStr of L2 holds Sigma L1 = Sigma L2; definition let S,T be up-complete non empty Poset; let f be Function of S,T; func Sigma f -> Function of Sigma S, Sigma T equals :: WAYBEL29:def 2 f; end; registration let S,T be up-complete non empty Poset; let f be directed-sups-preserving Function of S,T; cluster Sigma f -> continuous; end; theorem :: WAYBEL29:17 for S, T being up-complete non empty Poset for f being Function of S , T holds f is isomorphic iff Sigma f is isomorphic; theorem :: WAYBEL29:18 for X being non empty TopSpace for S being Scott complete TopLattice holds oContMaps(X, S) = ContMaps(X, S); definition let X,Y be non empty TopSpace; func Theta(X,Y) -> Function of InclPoset the topology of [:X, Y:], ContMaps( X, Sigma InclPoset the topology of Y) means :: WAYBEL29:def 3 for W being open Subset of [:X, Y:] holds it.W = (W, the carrier of X)*graph; end; begin :: Some Natural Isomorphisms definition let X be non empty TopSpace; func alpha X -> Function of oContMaps(X, Sierpinski_Space), InclPoset the topology of X means :: WAYBEL29:def 4 for g being continuous Function of X, Sierpinski_Space holds it.g = g"{1}; end; theorem :: WAYBEL29:19 for X being non empty TopSpace for V being open Subset of X holds ( alpha X)".V = chi(V, the carrier of X); registration let X be non empty TopSpace; cluster alpha X -> isomorphic; end; registration let X be non empty TopSpace; cluster (alpha X)" -> isomorphic; end; registration let S be injective T_0-TopSpace; cluster Omega S -> Scott; end; registration let X be non empty TopSpace; cluster oContMaps(X, Sierpinski_Space) -> complete; end; theorem :: WAYBEL29:20 Omega Sierpinski_Space = Sigma BoolePoset{0}; registration let M be non empty set; let S be injective T_0-TopSpace; cluster M-TOP_prod (M => S) -> injective; end; theorem :: WAYBEL29:21 for M being non empty set, L being complete continuous LATTICE holds Omega (M-TOP_prod (M => Sigma L)) = Sigma (M-POS_prod (M => L)); theorem :: WAYBEL29:22 for M being non empty set, T being injective T_0-TopSpace holds Omega (M-TOP_prod (M => T)) = Sigma (M-POS_prod (M => Omega T)); definition let M be non empty set; let X,Y be non empty TopSpace; func commute(X, M, Y) -> Function of oContMaps(X, M-TOP_prod (M => Y)), oContMaps(X, Y)|^M means :: WAYBEL29:def 5 for f being continuous Function of X, M -TOP_prod (M => Y) holds it.f = commute f; end; registration let M be non empty set; let X,Y be non empty TopSpace; cluster commute(X,M,Y) -> one-to-one onto; end; registration let M be non empty set; let X be non empty TopSpace; cluster commute(X, M, Sierpinski_Space) -> isomorphic; end; theorem :: WAYBEL29:23 for X,Y being non empty TopSpace for S being Scott TopAugmentation of InclPoset the topology of Y for f1, f2 being Element of ContMaps(X, S) st f1 <= f2 holds *graph f1 c= *graph f2; begin :: The Poset of Open Sets :: 4.10. THEOREM, (1) <=> (1'), pp. 131-133 theorem :: WAYBEL29:24 for Y being T_0-TopSpace holds (for X being non empty TopSpace for L being Scott continuous complete TopLattice for T being Scott TopAugmentation of ContMaps(Y, L) ex f being Function of ContMaps(X, T), ContMaps([:X, Y:], L), g being Function of ContMaps([:X, Y:], L), ContMaps(X, T) st f is uncurrying one-to-one onto & g is currying one-to-one onto) iff for X being non empty TopSpace for L being Scott continuous complete TopLattice for T being Scott TopAugmentation of ContMaps(Y, L) ex f being Function of ContMaps(X, T), ContMaps([:X, Y:], L), g being Function of ContMaps([:X, Y:], L), ContMaps(X, T ) st f is uncurrying isomorphic & g is currying isomorphic; :: 4.10. THEOREM, (6) <=> (2), pp. 131-133 theorem :: WAYBEL29:25 for Y being T_0-TopSpace holds InclPoset the topology of Y is continuous iff for X being non empty TopSpace holds Theta(X, Y) is isomorphic ; :: 4.10. THEOREM, (6) <=> (3), pp. 131-133 theorem :: WAYBEL29:26 for Y being T_0-TopSpace holds InclPoset the topology of Y is continuous iff for X being non empty TopSpace for f being continuous Function of X, Sigma InclPoset the topology of Y holds *graph f is open Subset of [:X, Y :]; :: 4.10. THEOREM, (6) <=> (4), pp. 131-133 theorem :: WAYBEL29:27 for Y being T_0-TopSpace holds InclPoset the topology of Y is continuous iff {[W,y] where W is open Subset of Y, y is Element of Y: y in W} is open Subset of [:Sigma InclPoset the topology of Y, Y:]; :: 4.10. THEOREM, (6) <=> (5), pp. 131-133 theorem :: WAYBEL29:28 for Y being T_0-TopSpace holds InclPoset the topology of Y is continuous iff for y being Element of Y, V being open a_neighborhood of y ex H being open Subset of Sigma InclPoset the topology of Y st V in H & meet H is a_neighborhood of y; begin :: The Poset of Scott Open Sets theorem :: WAYBEL29:29 for R1,R2,R3 being non empty RelStr for f1 being Function of R1,R3 st f1 is isomorphic for f2 being Function of R2,R3 st f2=f1 & f2 is isomorphic holds the RelStr of R1 = the RelStr of R2; :: 4.11. THEOREM, (1) <=> (2), p. 133. theorem :: WAYBEL29:30 for L being complete LATTICE holds InclPoset sigma L is continuous iff for S being complete LATTICE holds sigma [:S, L:] = the topology of [:Sigma S, Sigma L:]; :: 4.11. THEOREM, (2) <=> (3), p. 133. theorem :: WAYBEL29:31 for L being complete LATTICE holds (for S being complete LATTICE holds sigma [:S, L:] = the topology of [:Sigma S, Sigma L:]) iff for S being complete LATTICE holds the TopStruct of Sigma [:S, L:] = [:Sigma S, Sigma L:] ; :: 4.11. THEOREM, (2) <=> (3+), p. 133. theorem :: WAYBEL29:32 for L being complete LATTICE holds (for S being complete LATTICE holds sigma [:S, L:] = the topology of [:Sigma S, Sigma L:]) iff for S being complete LATTICE holds Sigma [:S, L:] = Omega [:Sigma S, Sigma L:]; :: 4.11. THEOREM, (1) <=> (3+), p. 133. theorem :: WAYBEL29:33 for L being complete LATTICE holds InclPoset sigma L is continuous iff for S being complete LATTICE holds Sigma [:S, L:] = Omega [:Sigma S, Sigma L:];