Volume 12, 2000

University of Bialystok

Copyright (c) 2000 Association of Mizar Users

### The abstract of the Mizar article:

### The Characterization of the Continuity of Topologies

**by****Grzegorz Bancerek, and****Adam Naumowicz**- Received January 6, 2000
- MML identifier: WAYBEL29

- [ Mizar article, MML identifier index ]

environ vocabulary ORDERS_1, PRE_TOPC, FUNCT_1, SGRAPH1, RELAT_1, SUBSET_1, YELLOW_0, GROUP_1, WAYBEL27, FUNCT_2, PRALG_1, FUNCT_5, CAT_1, SEQM_3, BOOLE, WAYBEL_0, WAYBEL11, WAYBEL19, ORDINAL2, QUANTAL1, TARSKI, SETFAM_1, WAYBEL24, LATTICES, FUNCOP_1, WAYBEL26, LATTICE3, WAYBEL_9, FUNCTOR0, TSP_1, BHSP_3, YELLOW_9, YELLOW16, WAYBEL_3, PBOOLE, CARD_3, FINSET_1, FUNCT_4, RELAT_2, WAYBEL25, PRELAMB, YELLOW_1, T_0TOPSP, CONNSP_2, WELLORD1, LATTICE5, WAYBEL18, FUNCT_3, PROB_1, PRALG_2, RLVECT_2, WELLORD2, TOPS_1, YELLOW_6, WAYBEL29, RLVECT_3; notation TARSKI, XBOOLE_0, ENUMSET1, ZFMISC_1, SUBSET_1, SETFAM_1, RELAT_1, FUNCT_1, PARTFUN1, RELSET_1, FUNCT_3, FINSET_1, CARD_3, STRUCT_0, PRE_TOPC, TOPS_1, GRCAT_1, T_0TOPSP, TSP_1, CONNSP_2, CANTOR_1, FUNCT_4, FUNCT_5, FUNCT_7, MONOID_0, PBOOLE, PRALG_1, PRALG_2, WELLORD1, ORDERS_1, LATTICE3, TOPS_2, YELLOW_0, WAYBEL_0, YELLOW_1, FUNCT_2, 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 ENUMSET1, ORDERS_3, WAYBEL_5, WAYBEL_1, WAYBEL17, QUANTAL1, GRCAT_1, CANTOR_1, TOPS_1, TOPS_2, YELLOW_9, TOLER_1, PRALG_3, FUNCT_7, WAYBEL18, WAYBEL24, YELLOW16, WAYBEL26, WAYBEL27, T_0TOPSP, MONOID_0, BORSUK_1; clusters SUBSET_1, RELSET_1, FUNCT_1, FINSET_1, FRAENKEL, STRUCT_0, LATTICE3, TOPS_1, BORSUK_1, BORSUK_2, PRALG_1, FUNCT_2, YELLOW_0, WAYBEL_0, YELLOW_1, YELLOW_3, WAYBEL_3, WAYBEL11, YELLOW_9, WAYBEL14, YELLOW14, WAYBEL24, WAYBEL25, YELLOW16, WAYBEL26, WAYBEL27, TOPGRP_1, WAYBEL10, WAYBEL18, XBOOLE_0; requirements BOOLE, SUBSET; begin :: Preliminaries :: isomorphic -> onto is in YELLOW14 theorem :: WAYBEL29:1 for S, T being non empty RelStr for f being map of S, T st f is one-to-one onto holds f*f" = id T & f"*f = id S & f" is one-to-one onto; 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 map of S, T st f is currying one-to-one onto holds f" is uncurrying; theorem :: WAYBEL29:3 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 map of T, S st f is uncurrying one-to-one onto holds f" is currying; theorem :: WAYBEL29:4 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 map of S, T st f is currying one-to-one onto holds f is isomorphic; theorem :: WAYBEL29:5 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 map of S, T st f is uncurrying one-to-one onto holds f is isomorphic; theorem :: WAYBEL29:6 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 map of S1, T1 st f is isomorphic for g being map of S2, T2 st g = f holds g is isomorphic; :::::::::::::::::::::::: Przywlaszczone theorem :: WAYBEL29:7 :: stolen from WAYBEL_1:8 for R, S, T being RelStr for f being map of R, S st f is isomorphic for g being map of S, T st g is isomorphic for h being map of R, T st h = g*f holds h is isomorphic; ::::::::::::::::::::::::::::::::::::::::::::::::::::: canceled 2; theorem :: WAYBEL29:10 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:11 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 map of X, L; theorem :: WAYBEL29:12 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:13 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); definition cluster Scott -> injective T_0 (complete continuous TopLattice); end; definition cluster Scott continuous complete TopLattice; end; definition let X be non empty TopSpace; let L be Scott up-complete (non empty TopPoset); cluster ContMaps(X, L) -> up-complete; end; theorem :: WAYBEL29:14 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:15 :: stolen (generalized) from WAYBEL_3:33 for I being non empty set for J being Poset-yielding non-Empty reflexive-yielding 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)); definition let X be set; let L be lower-bounded (non empty reflexive antisymmetric RelStr); cluster L|^X -> lower-bounded; end; definition let X be non empty TopSpace; let L be lower-bounded (non empty TopPoset); cluster ContMaps(X, L) -> lower-bounded; end; definition let L be up-complete (non empty Poset); cluster -> up-complete TopAugmentation of L; cluster Scott -> correct TopAugmentation of L; end; definition let L be up-complete (non empty Poset); cluster strict Scott TopAugmentation of L; end; canceled; theorem :: WAYBEL29:17 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:18 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:19 for S being Scott up-complete (non empty TopPoset) holds Sigma S = the TopRelStr of S; theorem :: WAYBEL29:20 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 map of S,T; func Sigma f -> map of Sigma S, Sigma T equals :: WAYBEL29:def 2 f; end; definition let S,T be up-complete (non empty Poset); let f be directed-sups-preserving map of S,T; cluster Sigma f -> continuous; end; theorem :: WAYBEL29:21 for S, T being up-complete (non empty Poset) for f being map of S, T holds f is isomorphic iff Sigma f is isomorphic; theorem :: WAYBEL29:22 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) -> map 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 -> map of oContMaps(X, Sierpinski_Space), InclPoset the topology of X means :: WAYBEL29:def 4 for g being continuous map of X, Sierpinski_Space holds it.g = g"{1}; end; theorem :: WAYBEL29:23 for X being non empty TopSpace for V being open Subset of X holds (alpha X)".V = chi(V, the carrier of X); definition let X be non empty TopSpace; cluster alpha X -> isomorphic; end; definition let X be non empty TopSpace; cluster (alpha X)" -> isomorphic; end; definition let S be injective T_0-TopSpace; cluster Omega S -> Scott; end; definition let X be non empty TopSpace; cluster oContMaps(X, Sierpinski_Space) -> complete; end; theorem :: WAYBEL29:24 Omega Sierpinski_Space = Sigma BoolePoset 1; definition let M be non empty set; let S be injective T_0-TopSpace; cluster M-TOP_prod (M --> S) -> injective; end; theorem :: WAYBEL29:25 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:26 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) -> map of oContMaps(X, M-TOP_prod (M --> Y)), oContMaps(X, Y)|^M means :: WAYBEL29:def 5 for f being continuous map of X, M-TOP_prod (M --> Y) holds it.f = commute f; end; definition let M be non empty set; let X,Y be non empty TopSpace; cluster commute(X,M,Y) -> one-to-one onto; end; definition let M be non empty set; let X be non empty TopSpace; cluster commute(X, M, Sierpinski_Space) -> isomorphic; end; theorem :: WAYBEL29:27 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:28 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 map of ContMaps(X, T), ContMaps([:X, Y:], L), g being map 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 map of ContMaps(X, T), ContMaps([:X, Y:], L), g being map 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:29 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:30 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 map 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:31 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:32 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:33 for R1,R2,R3 being non empty RelStr for f1 being map of R1,R3 st f1 is isomorphic for f2 being map 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:34 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:35 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:36 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:37 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:];

Back to top