Journal of Formalized Mathematics
Volume 12, 2000
University of Bialystok
Copyright (c) 2000
Association of Mizar Users
The abstract of the Mizar article:
-
- 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