:: $T_0$ Topological Spaces
:: by Mariusz \.Zynel and Adam Guzowski
::
:: Received May 6, 1994
:: Copyright (c) 1994-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 XBOOLE_0, FUNCT_1, SUBSET_1, RELAT_1, TARSKI, PRE_TOPC, TOPS_2,
RCOMP_1, EQREL_1, STRUCT_0, RELAT_2, BORSUK_1, ORDINAL2, CARD_3,
CLASSES1, T_0TOPSP, FUNCT_2;
notations TARSKI, XBOOLE_0, SUBSET_1, CLASSES1, RELAT_2, RELAT_1, FUNCT_1,
RELSET_1, PARTFUN1, FUNCT_2, STRUCT_0, PRE_TOPC, TOPS_2, BORSUK_1,
EQREL_1;
constructors SETFAM_1, RFINSEQ, TOPS_2, BORSUK_1, CLASSES1;
registrations XBOOLE_0, FUNCT_1, PARTFUN1, FUNCT_2, STRUCT_0, PRE_TOPC,
BORSUK_1, EQREL_1, RELSET_1;
requirements SUBSET, BOOLE;
begin
::
:: Preliminaries
::
theorem :: T_0TOPSP:1
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 Function of T,S st f is being_homeomorphism;
end;
:: Open Function
definition
let T,S be TopStruct;
let f be Function 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;
registration
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 Function of T,T_0-reflex T equals
:: T_0TOPSP:def 6
Proj Indiscernible T;
end;
theorem :: T_0TOPSP:2
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:3
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:4
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:5
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:6
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:7
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:8
for T being non empty TopSpace holds T_0-canonical_map(T) is open;
::
:: Discernible TopStruct
::
definition
let T be TopStruct;
redefine attr T is T_0 means
:: T_0TOPSP:def 7
T is empty or for x,y being Point of T
st x <> y holds ex V being Subset of T st V is open & ( x in V & not y in V or
y in V & not x in V );
end;
registration
cluster T_0 non empty for TopSpace;
end;
::
:: T_0 TopSpace
::
definition
mode T_0-TopSpace is T_0 non empty TopSpace;
end;
theorem :: T_0TOPSP:9
for T being non empty TopSpace holds T_0-reflex(T) is T_0-TopSpace;
::
:: Homeomorphism of T_0 Reflexes
::
theorem :: T_0TOPSP:10
for T,S being non empty TopSpace st ex h being Function of T_0-reflex(
S),T_0-reflex(T) st h is being_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:11
for T being non empty TopSpace, T0 being T_0-TopSpace, f being
continuous Function 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:12
for T being non empty TopSpace, T0 being T_0-TopSpace, f being
continuous Function of T,T0 holds for p being Point of T holds f.:Class(
Indiscernibility(T),p) = {f.p};
::
:: Factorization
::
theorem :: T_0TOPSP:13
for T being non empty TopSpace, T0 being T_0-TopSpace, f being
continuous Function of T,T0 ex h being continuous Function of T_0-reflex(T),T0
st f = h*T_0-canonical_map(T);