:: Injective Spaces, Part { II }
:: by Artur Korni{\l}owicz and Jaros{\l}aw Gryko
::
:: Received July 3, 1999
:: Copyright (c) 1999-2016 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 PRE_TOPC, WAYBEL18, CARD_1, RCOMP_1, STRUCT_0, SUBSET_1,
XBOOLE_0, TARSKI, REWRITE1, WAYBEL11, WAYBEL_9, FUNCTOR0, T_0TOPSP,
YELLOW_9, CARD_3, FUNCOP_1, YELLOW_1, RELAT_1, RLVECT_2, FUNCT_1,
ZFMISC_1, ORDERS_2, WAYBEL_0, CAT_1, TOPS_2, WELLORD1, ORDINAL2, GROUP_6,
WAYBEL_1, FUNCT_3, BORSUK_1, EQREL_1, XXREAL_0, LATTICE3, YELLOW_0,
WAYBEL_3, RELAT_2, PROB_1, BINOP_1, SEQM_3, WAYBEL24, FUNCT_2, NEWTON,
FUNCT_6, YELLOW_2, ORDINAL1, CONNSP_2, TOPS_1, SEQ_2, YELLOW_8, SETFAM_1,
WAYBEL25;
notations TARSKI, XBOOLE_0, ENUMSET1, ZFMISC_1, SUBSET_1, RELAT_1, FUNCT_1,
RELSET_1, PARTFUN1, FUNCT_2, ORDINAL1, NUMBERS, FUNCT_3, NATTRA_1,
TOLER_1, QUANTAL1, CARD_3, PRALG_1, FUNCT_6, FUNCOP_1, WAYBEL18,
DOMAIN_1, STRUCT_0, PRE_TOPC, CONNSP_2, TOPS_1, TOPS_2, COMPTS_1,
BORSUK_1, TMAP_1, T_0TOPSP, BORSUK_3, ORDERS_2, LATTICE3, YELLOW_0,
WAYBEL_0, YELLOW_2, WAYBEL_1, WAYBEL_2, YELLOW_6, WAYBEL_3, YELLOW_8,
WAYBEL_9, WAYBEL11, YELLOW_9, WAYBEL17, YELLOW_1, WAYBEL24, YELLOW14;
constructors TOLER_1, FUNCT_6, TOPS_1, TOPS_2, NATTRA_1, BORSUK_1, TMAP_1,
CANTOR_1, MONOID_0, QUANTAL1, ORDERS_3, WAYBEL_1, WAYBEL_8, YELLOW_8,
WAYBEL17, YELLOW_9, BORSUK_3, WAYBEL24, YELLOW14, COMPTS_1, WAYBEL_2;
registrations XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1, FUNCT_2, FUNCOP_1,
STRUCT_0, PRE_TOPC, TOPS_1, BORSUK_1, LATTICE3, YELLOW_0, TEX_1, TSP_1,
BORSUK_2, WAYBEL_0, YELLOW_1, WAYBEL_1, WAYBEL_2, WAYBEL_3, WAYBEL_8,
WAYBEL10, WAYBEL17, YELLOW_9, WAYBEL18, WAYBEL19, WAYBEL21, WAYBEL24,
YELLOW14, RELSET_1;
requirements SUBSET, BOOLE, NUMERALS;
begin :: Injective spaces
theorem :: WAYBEL25:1
for p being Point of Sierpinski_Space st p = 0 holds {p} is closed;
theorem :: WAYBEL25:2
for p being Point of Sierpinski_Space st p = 1 holds {p} is non closed;
registration
cluster Sierpinski_Space -> non T_1;
end;
registration
cluster complete Scott -> T_0 for TopLattice;
end;
registration
cluster injective strict for T_0-TopSpace;
end;
registration
cluster complete Scott strict for TopLattice;
end;
theorem :: WAYBEL25:3 :: see WAYBEL18:16
for I being non empty set, T being Scott TopAugmentation of
product(I --> BoolePoset{0})
holds the carrier of T = the carrier of product(I
--> Sierpinski_Space);
theorem :: WAYBEL25:4
for L1, L2 being complete LATTICE, T1 being Scott TopAugmentation
of L1, T2 being Scott TopAugmentation of L2, h being Function of L1, L2, H
being Function of T1, T2 st h = H & h is isomorphic holds H is
being_homeomorphism;
theorem :: WAYBEL25:5
for L1, L2 being complete LATTICE, T1 being Scott TopAugmentation
of L1, T2 being Scott TopAugmentation of L2 st L1, L2 are_isomorphic holds T1,
T2 are_homeomorphic;
theorem :: WAYBEL25:6
for S, T being non empty TopSpace st S is injective & S, T
are_homeomorphic holds T is injective;
theorem :: WAYBEL25:7
for L1, L2 being complete LATTICE, T1 being Scott TopAugmentation of
L1, T2 being Scott TopAugmentation of L2 st L1, L2 are_isomorphic & T1 is
injective holds T2 is injective;
definition
let X, Y be non empty TopSpace;
redefine pred X is_Retract_of Y means
:: WAYBEL25:def 1
ex c being continuous Function
of X, Y, r being continuous Function of Y, X st r * c = id X;
end;
theorem :: WAYBEL25:8
for S, T, X, Y being non empty TopSpace st the TopStruct of S = the
TopStruct of T & the TopStruct of X = the TopStruct of Y & S is_Retract_of X
holds T is_Retract_of Y;
theorem :: WAYBEL25:9
for T, S1, S2 being non empty TopStruct st S1, S2 are_homeomorphic &
S1 is_Retract_of T holds S2 is_Retract_of T;
theorem :: WAYBEL25:10
for S, T being non empty TopSpace st T is injective & S is_Retract_of
T holds S is injective;
theorem :: WAYBEL25:11 ::p.126 exercise 3.13, 1 => 2
for J being injective non empty TopSpace, Y being non empty TopSpace
st J is SubSpace of Y holds J is_Retract_of Y;
:: p.123 proposition 3.5
:: p.124 theorem 3.8 (i, part a)
:: p.126 exercise 3.14
theorem :: WAYBEL25:12
for L being complete continuous LATTICE, T being Scott
TopAugmentation of L holds T is injective;
registration
let L be complete continuous LATTICE;
cluster Scott -> injective for TopAugmentation of L;
end;
registration
let T be injective non empty TopSpace;
cluster the TopStruct of T -> injective;
end;
begin :: Specialization order
::p.124 definition 3.6
definition
let T be TopStruct;
func Omega T -> strict TopRelStr means
:: WAYBEL25:def 2
the TopStruct of it = the
TopStruct of T & for x, y being Element of it holds x <= y iff ex Y being
Subset of T st Y = {y} & x in Cl Y;
end;
registration
let T be empty TopStruct;
cluster Omega T -> empty;
end;
registration
let T be non empty TopStruct;
cluster Omega T -> non empty;
end;
registration
let T be TopSpace;
cluster Omega T -> TopSpace-like;
end;
registration
let T be TopStruct;
cluster Omega T -> reflexive;
end;
registration
let T be TopStruct;
cluster Omega T -> transitive;
end;
registration
let T be T_0-TopSpace;
cluster Omega T -> antisymmetric;
end;
theorem :: WAYBEL25:13
for S, T being TopSpace st the TopStruct of S = the TopStruct of
T holds Omega S = Omega T;
theorem :: WAYBEL25:14
for M being non empty set, T being non empty TopSpace holds the RelStr
of Omega product(M --> T) = the RelStr of product(M --> Omega T);
::p.124 theorem 3.8 (i, part b)
theorem :: WAYBEL25:15
for S being Scott complete TopLattice holds Omega S = the TopRelStr of S;
::p.124 theorem 3.8 (i, part b)
theorem :: WAYBEL25:16
for L being complete LATTICE, S being Scott TopAugmentation of L
holds the RelStr of Omega S = the RelStr of L;
registration
let S be Scott complete TopLattice;
cluster Omega S -> complete;
end;
theorem :: WAYBEL25:17
for T being non empty TopSpace, S being non empty SubSpace of T
holds Omega S is full SubRelStr of Omega T;
theorem :: WAYBEL25:18
for S, T being TopSpace, h being Function of S, T, g being
Function of Omega S, Omega T st h = g & h is being_homeomorphism holds g is
isomorphic;
theorem :: WAYBEL25:19
for S, T being TopSpace st S, T are_homeomorphic holds Omega S,
Omega T are_isomorphic;
::p.124 proposition 3.7
::p.124 theorem 3.8 (ii, part a)
theorem :: WAYBEL25:20
for T being injective T_0-TopSpace holds Omega T is complete
continuous LATTICE;
registration
let T be injective T_0-TopSpace;
cluster Omega T -> complete continuous;
end;
theorem :: WAYBEL25:21
for X, Y being non empty TopSpace, f being continuous Function
of Omega X, Omega Y holds f is monotone;
registration
let X, Y be non empty TopSpace;
cluster continuous -> monotone for Function of Omega X, Omega Y;
end;
theorem :: WAYBEL25:22
for T being non empty TopSpace, x being Element of Omega T holds
Cl {x} = downarrow x;
registration
let T be non empty TopSpace, x be Element of Omega T;
cluster Cl {x} -> non empty lower directed;
cluster downarrow x -> closed;
end;
theorem :: WAYBEL25:23
for X being TopSpace, A being open Subset of Omega X holds A is upper;
registration
let T be TopSpace;
cluster open -> upper for Subset of Omega T;
end;
definition
let I be non empty set, S, T be non empty RelStr, N be net of T, i be
Element of I such that
the carrier of T c= the carrier of S |^ I;
func commute(N,i,S) -> strict net of S means
:: WAYBEL25:def 3
the RelStr of it = the
RelStr of N & the mapping of it = (commute the mapping of N).i;
end;
theorem :: WAYBEL25:24
for X, Y being non empty TopSpace, N being net of ContMaps(X,
Omega Y), i being Element of N, x being Point of X holds (the mapping of
commute(N,x,Omega Y)).i = (the mapping of N).i.x;
theorem :: WAYBEL25:25
for X, Y being non empty TopSpace, N being eventually-directed
net of ContMaps(X,Omega Y), x being Point of X holds commute(N,x,Omega Y) is
eventually-directed;
registration
let X, Y be non empty TopSpace, N be eventually-directed net of ContMaps(X,
Omega Y), x be Point of X;
cluster commute(N,x,Omega Y) -> eventually-directed;
end;
registration
let X, Y be non empty TopSpace;
cluster -> Function-yielding for net of ContMaps(X,Omega Y);
end;
theorem :: WAYBEL25:26
for X being non empty TopSpace, Y being T_0-TopSpace, N being
net of ContMaps(X,Omega Y) st for x being Point of X holds ex_sup_of commute(N,
x,Omega Y) holds ex_sup_of rng the mapping of N, (Omega Y) |^ the carrier of X;
begin :: Monotone convergence topological spaces
::p.125 definition 3.9
definition
let T be non empty TopSpace;
attr T is monotone-convergence means
:: WAYBEL25:def 4
for D being non empty directed
Subset of Omega T holds ex_sup_of D,Omega T & for V being open Subset of T st
sup D in V holds D meets V;
end;
theorem :: WAYBEL25:27
for S, T being non empty TopSpace st the TopStruct of S = the
TopStruct of T & S is monotone-convergence holds T is monotone-convergence;
registration
cluster trivial -> monotone-convergence for T_0-TopSpace;
end;
theorem :: WAYBEL25:28
for S being monotone-convergence T_0-TopSpace, T being T_0-TopSpace st
S, T are_homeomorphic holds T is monotone-convergence;
theorem :: WAYBEL25:29
for S being Scott complete TopLattice holds S is monotone-convergence;
registration
let L be complete LATTICE;
cluster -> monotone-convergence for Scott TopAugmentation of L;
end;
registration
let L be complete LATTICE, S be Scott TopAugmentation of L;
cluster the TopStruct of S -> monotone-convergence;
end;
theorem :: WAYBEL25:30
for X being monotone-convergence T_0-TopSpace holds Omega X is up-complete;
registration
let X be monotone-convergence T_0-TopSpace;
cluster Omega X -> up-complete;
end;
theorem :: WAYBEL25:31
for X being monotone-convergence non empty TopSpace, N being
eventually-directed prenet of Omega X holds ex_sup_of N;
theorem :: WAYBEL25:32
for X being monotone-convergence non empty TopSpace, N being
eventually-directed net of Omega X holds sup N in Lim N;
theorem :: WAYBEL25:33
for X being monotone-convergence non empty TopSpace, N being
eventually-directed net of Omega X holds N is convergent;
registration
let X be monotone-convergence non empty TopSpace;
cluster -> convergent for eventually-directed net of Omega X;
end;
theorem :: WAYBEL25:34
for X being non empty TopSpace st for N being eventually-directed net
of Omega X holds ex_sup_of N & sup N in Lim N holds X is monotone-convergence
;
::p.125 lemma 3.10
theorem :: WAYBEL25:35
for X being monotone-convergence non empty TopSpace, Y being
T_0-TopSpace, f being continuous Function of Omega X, Omega Y holds f is
directed-sups-preserving;
registration
let X be monotone-convergence non empty TopSpace, Y be T_0-TopSpace;
cluster continuous -> directed-sups-preserving for
Function of Omega X, Omega Y;
end;
theorem :: WAYBEL25:36
for T being monotone-convergence T_0-TopSpace, R being
T_0-TopSpace st R is_Retract_of T holds R is monotone-convergence;
::p.124 theorem 3.8 (ii, part b)
theorem :: WAYBEL25:37
for T being injective T_0-TopSpace, S being Scott
TopAugmentation of Omega T holds the TopStruct of S = the TopStruct of T;
theorem :: WAYBEL25:38
for T being injective T_0-TopSpace holds T is compact locally-compact sober;
theorem :: WAYBEL25:39
for T being injective T_0-TopSpace holds T is monotone-convergence;
registration
cluster injective -> monotone-convergence for T_0-TopSpace;
end;
theorem :: WAYBEL25:40
for X being non empty TopSpace, Y being monotone-convergence
T_0-TopSpace, N being net of ContMaps(X,Omega Y), f, g being Function of X,
Omega Y st f = "\/"(rng the mapping of N, (Omega Y) |^ the carrier of X) &
ex_sup_of rng the mapping of N, (Omega Y) |^ the carrier of X & g in rng the
mapping of N holds g <= f;
theorem :: WAYBEL25:41
for X being non empty TopSpace, Y being monotone-convergence
T_0-TopSpace, N being net of ContMaps(X,Omega Y), x being Point of X, f being
Function of X, Omega Y st (for a being Point of X holds commute(N,a,Omega Y) is
eventually-directed) & f = "\/"(rng the mapping of N, (Omega Y) |^ the carrier
of X) holds f.x = sup commute(N,x,Omega Y);
::p.125 lemma 3.11
theorem :: WAYBEL25:42
for X being non empty TopSpace, Y being monotone-convergence
T_0-TopSpace, N being net of ContMaps(X,Omega Y) st for x being Point of X
holds commute(N,x,Omega Y) is eventually-directed holds "\/"(rng the mapping of
N, (Omega Y) |^ the carrier of X) is continuous Function of X, Y;
::p.126 lemma 3.12 (i)
theorem :: WAYBEL25:43
for X being non empty TopSpace, Y being monotone-convergence
T_0-TopSpace holds ContMaps(X,Omega Y) is directed-sups-inheriting SubRelStr of
(Omega Y) |^ the carrier of X;