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