:: Alexandroff One Point Compactification
:: by Czeslaw Bylinski
::
:: Received August 13, 2007
:: Copyright (c) 2007-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 PRE_TOPC, SETFAM_1, RCOMP_1, SUBSET_1, XBOOLE_0, WAYBEL_3,
YELLOW13, CONNSP_2, TARSKI, ZFMISC_1, TOPS_1, CARD_5, COMPTS_1, NATTRA_1,
RELAT_1, FUNCT_3, FUNCT_1, QUOFIELD, TOPS_2, ORDINAL2, STRUCT_0,
ORDINAL1, FINSET_1, COMPACT1;
notations TARSKI, XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1, RELSET_1, SETFAM_1,
ORDINAL1, FINSET_1, FINSUB_1, DOMAIN_1, STRUCT_0, PRE_TOPC, TOPS_1,
TOPS_2, TDLAT_3, TSEP_1, TEX_3, COMPTS_1, CONNSP_2, WAYBEL_3, YELLOW_9,
YELLOW13;
constructors FINSOP_1, DOMAIN_1, TOPS_1, TOPS_2, YELLOW_9, YELLOW13, TDLAT_3,
CONNSP_2, T_0TOPSP, WAYBEL_3, TSEP_1, TEX_3, COMPTS_1, RELSET_1;
registrations XBOOLE_0, SUBSET_1, FINSET_1, STRUCT_0, FINSUB_1, RELAT_1,
TOPS_1, BORSUK_2, FUNCT_1, PRE_TOPC, TEX_1, YELLOW13, COMPTS_1, RELSET_1;
requirements BOOLE, SUBSET;
begin :: Preliminaires
definition
let X be TopSpace, P be Subset-Family of X;
attr P is compact means
:: COMPACT1:def 1
for U being Subset of X st U in P holds U is compact;
end;
definition
let X be TopSpace, U be Subset of X;
attr U is relatively-compact means
:: COMPACT1:def 2
Cl U is compact;
end;
registration
let X be TopSpace;
cluster empty -> relatively-compact for Subset of X;
end;
registration
let T be TopSpace;
cluster relatively-compact for Subset of T;
end;
registration
let X be TopSpace, U be relatively-compact Subset of X;
cluster Cl U -> compact;
end;
notation
let X be TopSpace, U be Subset of X;
synonym U is pre-compact for U is relatively-compact;
end;
:: see WAYBEL_3:def 9
notation
let X be non empty TopSpace;
synonym X is liminally-compact for X is locally-compact;
end;
:: see WAYBEL_3:def 9
definition
let X be non empty TopSpace;
redefine attr X is liminally-compact means
:: COMPACT1:def 3
for x being Point of X ex B being basis of x st B is compact;
end;
definition
let X be non empty TopSpace;
attr X is locally-relatively-compact means
:: COMPACT1:def 4
for x being Point of X ex
U being a_neighborhood of x st U is relatively-compact;
end;
definition
let X be non empty TopSpace;
attr X is locally-closed/compact means
:: COMPACT1:def 5
for x being Point of X ex U being a_neighborhood of x st U is closed compact;
end;
definition
let X be non empty TopSpace;
attr X is locally-compact means
:: COMPACT1:def 6
for x being Point of X ex U being a_neighborhood of x st U is compact;
end;
registration
cluster liminally-compact -> locally-compact for non empty TopSpace;
end;
registration
cluster locally-compact -> liminally-compact for
non empty regular TopSpace;
end;
registration
cluster locally-relatively-compact -> locally-closed/compact for non empty
TopSpace;
end;
registration
cluster locally-closed/compact -> locally-relatively-compact for non empty
TopSpace;
end;
registration
cluster locally-relatively-compact -> locally-compact for
non empty TopSpace;
end;
registration
cluster locally-compact -> locally-relatively-compact for
non empty Hausdorff
TopSpace;
end;
registration
cluster compact -> locally-compact for non empty TopSpace;
end;
registration
cluster discrete -> locally-compact for non empty TopSpace;
end;
registration
cluster discrete non empty for TopSpace;
end;
registration
let X be locally-compact non empty TopSpace, C be closed non empty Subset
of X;
cluster X | C -> locally-compact;
end;
registration
let X be locally-compact non empty regular TopSpace, P be open non empty
Subset of X;
cluster X | P -> locally-compact;
end;
theorem :: COMPACT1:1
for X being Hausdorff non empty TopSpace, E being non empty Subset of
X st X|E is dense locally-compact holds X|E is open;
theorem :: COMPACT1:2
for X,Y being TopSpace, A being Subset of X st [#]X c= [#]Y holds
incl(X,Y).:A = A;
definition
let X,Y be TopSpace, f be Function of X,Y;
attr f is embedding means
:: COMPACT1:def 7
ex h being Function of X, Y | (rng f) st h = f & h is being_homeomorphism;
end;
theorem :: COMPACT1:3
for X,Y being TopSpace st [#]X c= [#]Y & ex Xy being Subset of Y
st Xy = [#]X & the topology of Y|Xy = the topology of X holds incl(X,Y) is
embedding;
definition
let X be TopSpace, Y be TopSpace, h be Function of X,Y;
attr h is compactification means
:: COMPACT1:def 8
h is embedding & Y is compact & h.:( [#]X) is dense;
end;
registration
let X be TopSpace, Y be TopSpace;
cluster compactification -> embedding for Function of X,Y;
end;
definition
let X be TopStruct;
func One-Point_Compactification(X) -> strict TopStruct means
:: COMPACT1:def 9
the
carrier of it = succ([#]X) & the topology of it = (the topology of X) \/ {U \/
{[#]X} where U is Subset of X: U is open & U` is compact};
end;
registration
let X be TopStruct;
cluster One-Point_Compactification(X) -> non empty;
end;
theorem :: COMPACT1:4
for X being TopStruct holds [#]X c= [#]One-Point_Compactification (X);
registration
let X be TopSpace;
cluster One-Point_Compactification(X) -> TopSpace-like;
end;
theorem :: COMPACT1:5
for X being TopStruct holds X is SubSpace of One-Point_Compactification(X);
registration
let X be TopSpace;
cluster One-Point_Compactification(X) -> compact;
end;
theorem :: COMPACT1:6
for X being non empty TopSpace holds X is Hausdorff locally-compact
iff One-Point_Compactification(X) is Hausdorff;
theorem :: COMPACT1:7
for X being non empty TopSpace holds X is non compact iff ex X9
being Subset of One-Point_Compactification(X) st X9 = [#]X & X9 is dense;
theorem :: COMPACT1:8
for X being non empty TopSpace st X is non compact holds incl(X,
One-Point_Compactification X) is compactification;