:: 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:];