Journal of Formalized Mathematics
Volume 6, 1994
University of Bialystok
Copyright (c) 1994 Association of Mizar Users

### \Tzero\ Topological Spaces

by
Mariusz Zynel, and

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);
```