The abstract of the Mizar article:

\Tzero\ Topological Spaces

by

Mariusz Zynel, and

Adam Guzowski

Received May 6, 1994

MML identifier: T_0TOPSP

[ Mizar article, MML identifier index ]

environ

 vocabulary RELAT_1, FUNCT_1, PRE_TOPC, TOPS_2, EQREL_1, RELAT_2, BORSUK_1,
      SUBSET_1, TARSKI, BOOLE, METRIC_1, RFINSEQ, ORDINAL2, T_0TOPSP, PARTFUN1;
 notation TARSKI, XBOOLE_0, SUBSET_1, RFINSEQ, RELAT_2, RELSET_1, RELAT_1,
      FUNCT_1, STRUCT_0, PARTFUN1, FUNCT_2, PRE_TOPC, TOPS_2, BORSUK_1,
      EQREL_1;
 constructors RFINSEQ, RELAT_2, TOPS_2, BORSUK_1, MEMBERED, PARTFUN1, XBOOLE_0;
 clusters BORSUK_1, RELSET_1, STRUCT_0, PRE_TOPC, SUBSET_1, MEMBERED, ZFMISC_1,
      PARTFUN1, FUNCT_2, XBOOLE_0;
 requirements SUBSET, BOOLE;


begin
::
::    Preliminaries
::

theorem :: T_0TOPSP:1
for A,B being non empty set,
    R1,R2 being Relation of A,B st
  for x being Element of A, y being Element of B holds
   [x,y] in R1 iff [x,y] in R2
    holds R1 = R2;

theorem :: T_0TOPSP:2
for X,Y being non empty set,
    f being Function of X,Y holds
  for A being Subset of X st
    for x1,x2 being Element of X holds (x1 in A & f.x1=f.x2) implies x2 in A
      holds f"(f.:A) = A;

:::::::::::::::::::::::::::::::::::::::::::
::    Homeomorphic TopSpaces             ::
:::::::::::::::::::::::::::::::::::::::::::

definition
  let T,S be TopStruct;
  pred T,S are_homeomorphic means
:: T_0TOPSP:def 1
    ex f being map of T,S st f is_homeomorphism;
end;

:::::::::::::::::::::::::::::::::::::::::::
::    Open Function                      ::
:::::::::::::::::::::::::::::::::::::::::::

definition
  let T,S be TopStruct;
  let f be map of T,S;
  attr f is open means
:: T_0TOPSP:def 2
  for A being Subset of T st A is open holds f.:A is open;
end;

::
::    Indiscernibility Relation
::

definition
  let T be non empty TopStruct;
  func Indiscernibility(T) -> Equivalence_Relation of the carrier of T means
:: T_0TOPSP:def 3

  for p,q being Point of T holds
    [p,q] in it iff
       for A being Subset of T st A is open
       holds p in A iff q in A;
end;


::
::    Indiscernibility Partition
::

definition
  let T be non empty TopStruct;
  func Indiscernible(T) -> non empty a_partition of the carrier of T equals
:: T_0TOPSP:def 4

   Class Indiscernibility(T);
end;

::
::    T_0 Reflex of TopSpace
::

definition
  let T be non empty TopSpace;
  func T_0-reflex(T) -> TopSpace equals
:: T_0TOPSP:def 5
   space Indiscernible(T);
end;

definition
  let T be non empty TopSpace;
  cluster T_0-reflex(T) -> non empty;
end;

::
::    Function from TopSpace to its T_0 Reflex
::

definition
  let T be non empty TopSpace;
  func T_0-canonical_map T -> continuous map of T,T_0-reflex T equals
:: T_0TOPSP:def 6
   Proj Indiscernible T;
end;

::
::    Properties of Canonical Map and T_0 Reflex
::

theorem :: T_0TOPSP:3
for T being non empty TopSpace,
    p being Point of T holds p in (T_0-canonical_map(T)).p;

theorem :: T_0TOPSP:4
for T being non empty TopSpace holds
  dom T_0-canonical_map(T) = the carrier of T &
  rng T_0-canonical_map(T) c= the carrier of T_0-reflex(T);

theorem :: T_0TOPSP:5
for T being non empty TopSpace holds
  the carrier of T_0-reflex(T) = Indiscernible(T) &
  the topology of T_0-reflex(T) =
    { A where A is Subset of Indiscernible(T) : union A in the topology of T};

theorem :: T_0TOPSP:6
for T being non empty TopSpace,
    V being Subset of T_0-reflex(T) holds
  V is open iff union V in the topology of T;

theorem :: T_0TOPSP:7
for T being non empty TopSpace,
   C being set holds
  C is Point of T_0-reflex(T) iff
    ex p being Point of T st C = Class(Indiscernibility(T),p);

theorem :: T_0TOPSP:8
for T being non empty TopSpace,
    p being Point of T holds
  (T_0-canonical_map(T)).p = Class(Indiscernibility(T),p);

theorem :: T_0TOPSP:9
for T being non empty TopSpace,
    p,q being Point of T holds
  (T_0-canonical_map(T)).q = (T_0-canonical_map(T)).p iff
       [q,p] in Indiscernibility(T);

theorem :: T_0TOPSP:10
for T being non empty TopSpace,
    A being Subset of T st A is open holds
     for p,q being Point of T holds
       p in A & (T_0-canonical_map(T)).p = (T_0-canonical_map(T)).q
         implies q in A;

theorem :: T_0TOPSP:11
for T being non empty TopSpace, A being Subset of T st A is open
  for C being Subset of T st C in Indiscernible(T) & C meets A
  holds C c= A;

theorem :: T_0TOPSP:12
for T being non empty TopSpace holds T_0-canonical_map(T) is open;

::
::    Discernible TopStruct
::

definition let IT be TopStruct;
  attr IT is discerning means
:: T_0TOPSP:def 7
 IT is empty or
  for x,y being Point of IT st x <> y holds
    ex V being Subset of IT st V is open &
      ((x in V & not y in V) or (y in V & not x in V));
end;

definition
  cluster discerning non empty TopSpace;
end;

::
::    T_0 TopSpace
::

definition
  mode T_0-TopSpace is discerning non empty TopSpace;
end;

theorem :: T_0TOPSP:13
  for T being non empty TopSpace holds T_0-reflex(T) is T_0-TopSpace;

::
::    Homeomorphism of T_0 Reflexes
::

theorem :: T_0TOPSP:14
  for T,S being non empty TopSpace st
   ex h being map of T_0-reflex(S),T_0-reflex(T)
     st h is_homeomorphism & T_0-canonical_map(T),h*T_0-canonical_map(S)
       are_fiberwise_equipotent holds T,S are_homeomorphic;

::
::    Properties of Continuous Mapping from TopSpace to its T_0 Reflex
::

theorem :: T_0TOPSP:15
for T being non empty TopSpace,
    T0 being T_0-TopSpace,
    f being continuous map of T,T0 holds
  for p,q being Point of T holds
         [p,q] in Indiscernibility(T) implies f.p = f.q;

theorem :: T_0TOPSP:16
for T being non empty TopSpace,
    T0 being T_0-TopSpace,
    f being continuous map of T,T0 holds
  for p being Point of T holds f.:Class(Indiscernibility(T),p) = {f.p};

::
::    Factorization
::

theorem :: T_0TOPSP:17
  for T being non empty TopSpace,
    T0 being T_0-TopSpace,
    f being continuous map of T,T0
  ex h being continuous map of T_0-reflex(T),T0 st
     f = h*T_0-canonical_map(T);