:: $T_0$ Topological Spaces
:: by Mariusz \.Zynel and Adam Guzowski
::
:: Received May 6, 1994
:: Copyright (c) 1994-2026 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;
definitions TOPS_2, RELAT_2, RELSET_1;
equalities STRUCT_0;
expansions TOPS_2, PRE_TOPC;
theorems FUNCT_1, FUNCT_2, EQREL_1, RELAT_1, TOPS_2, BORSUK_1, TARSKI,
RELSET_1, XBOOLE_0, RELAT_2, PARTFUN1, ORDERS_1, CLASSES1;
schemes FUNCT_2, RELSET_1;
begin
::
:: Preliminaries
::
theorem Th1:
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
proof
let X,Y be non empty set;
let f be Function of X,Y;
let A be Subset of X;
assume
A1: for x1,x2 being Element of X holds x1 in A & f.x1=f.x2 implies x2 in A;
for x being object st x in f"(f.:A) holds x in A
proof
let x be object;
assume
A2: x in f"(f.:A);
then f.x in f.:A by FUNCT_1:def 7;
then ex x0 being object st x0 in X & x0 in A & f.x = f.x0 by FUNCT_2:64;
hence thesis by A1,A2;
end;
then A c= f"(f.:A) & f"(f.:A) c= A by FUNCT_2:42,TARSKI:def 3;
hence thesis by XBOOLE_0:def 10;
end;
:: Homeomorphic TopSpaces
definition
let T,S be TopStruct;
pred T,S are_homeomorphic means
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
for A being Subset of T st A is open holds f.:A is open;
correctness;
end;
::
:: Indiscernibility Relation
::
definition
let T be non empty TopStruct;
func Indiscernibility(T) -> Equivalence_Relation of the carrier of T means
:
Def3: 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;
existence
proof
defpred X[set,set] means for A being Subset of T st A is open holds $1 in
A iff $2 in A;
consider R being Relation of the carrier of T,the carrier of T such that
A1: for p,q being Element of T holds [p,q] in R iff X[p,q] from
RELSET_1:sch 2;
A2: R is_transitive_in the carrier of T
proof
let x,y,z be object;
assume that
A3: x in the carrier of T & y in the carrier of T & z in the carrier of T and
A4: [x,y] in R and
A5: [y,z] in R;
reconsider x9 = x, y9 = y, z9 = z as Element of T by A3;
for A being Subset of T st A is open holds x9 in A iff z9 in A
proof
let A be Subset of T;
assume
A6: A is open;
then x9 in A iff y9 in A by A1,A4;
hence thesis by A1,A5,A6;
end;
hence thesis by A1;
end;
R is_reflexive_in the carrier of T
proof
let x be object;
A7: for A being Subset of T st A is open holds x in A iff x in A;
assume x in the carrier of T;
hence thesis by A1,A7;
end;
then
A8: dom R = the carrier of T & field R = the carrier of T by ORDERS_1:13;
R is_symmetric_in the carrier of T
proof
let x,y be object;
assume that
A9: x in the carrier of T & y in the carrier of T and
A10: [x,y] in R;
for A being Subset of T st A is open holds y in A iff x in A by A1,A9,A10
;
hence thesis by A1,A9;
end;
then reconsider R as Equivalence_Relation of the carrier of T by A8,A2,
PARTFUN1:def 2,RELAT_2:def 11,def 16;
take R;
let p,q be Point of T;
thus [p,q] in R implies for A be Subset of T st A is open holds p in A iff
q in A by A1;
assume for A being Subset of T st A is open holds p in A iff q in A;
hence thesis by A1;
end;
uniqueness
proof
let R1,R2 be Equivalence_Relation of the carrier of T;
assume that
A11: for p,q being Point of T holds [p,q] in R1 iff for A being Subset
of T st A is open holds p in A iff q in A and
A12: for p,q being Point of T holds [p,q] in R2 iff for A being Subset
of T st A is open holds p in A iff q in A;
let x,y be Point of T;
[x,y] in R1 iff for A being Subset of T st A is open holds x in A iff
y in A by A11;
hence thesis by A12;
end;
end;
::
:: Indiscernibility Partition
::
definition
let T be non empty TopStruct;
func Indiscernible(T) -> non empty a_partition of the carrier of T equals
Class Indiscernibility(T);
coherence;
end;
::
:: T_0 Reflex of TopSpace
::
definition
let T be non empty TopSpace;
func T_0-reflex(T) -> TopSpace equals
space Indiscernible(T);
correctness;
end;
registration
let T be non empty TopSpace;
cluster T_0-reflex(T) -> non empty;
coherence;
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
Proj Indiscernible T;
coherence;
end;
theorem Th2:
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
proof
let T be non empty TopSpace;
let V be Subset of T_0-reflex(T);
A1: V is Subset of Indiscernible(T) by BORSUK_1:def 7;
thus V is open implies union V in the topology of T
by A1,BORSUK_1:27;
assume union V in the topology of T;
then V in the topology of space Indiscernible(T) by A1,BORSUK_1:27;
hence thesis;
end;
theorem Th3:
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)
proof
let T be non empty TopSpace;
set TR = T_0-reflex(T);
set R = Indiscernibility(T);
let C be set;
hereby
assume C is Point of TR;
then C in the carrier of TR;
then C in Indiscernible(T) by BORSUK_1:def 7;
hence ex p being Point of T st C = Class(R,p) by EQREL_1:36;
end;
assume ex p being Point of T st C = Class(R,p);
then C in Class R by EQREL_1:def 3;
hence thesis by BORSUK_1:def 7;
end;
theorem Th4:
for T being non empty TopSpace, p being Point of T holds (
T_0-canonical_map(T)).p = Class(Indiscernibility(T),p)
proof
let T be non empty TopSpace;
let p be Point of T;
set F = T_0-canonical_map(T);
set R = Indiscernibility(T);
F.p in the carrier of T_0-reflex(T);
then F.p in Indiscernible(T) by BORSUK_1:def 7;
then consider y being Element of T such that
A1: F.p = Class(R,y) by EQREL_1:36;
p in Class(R,y) by A1,BORSUK_1:28;
hence thesis by A1,EQREL_1:23;
end;
theorem Th5:
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)
proof
let T be non empty TopSpace;
let p,q be Point of T;
set F = T_0-canonical_map(T);
set R = Indiscernibility(T);
hereby
assume F.q = F.p;
then q in F.p by BORSUK_1:28;
then q in Class(R,p) by Th4;
hence [q,p] in R by EQREL_1:19;
end;
assume [q,p] in R;
then Class(R,q) = Class(R,p) by EQREL_1:35;
then F.q = Class(R,p) by Th4;
hence thesis by Th4;
end;
theorem Th6:
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
proof
let T be non empty TopSpace;
let A be Subset of T such that
A1: A is open;
set F=T_0-canonical_map(T);
let p,q be Point of T;
assume that
A2: p in A and
A3: F.p = F.q;
A4: F.p = Class(Indiscernibility(T),p) by Th4;
q in F.p by A3,BORSUK_1:28;
then [q,p] in Indiscernibility(T) by A4,EQREL_1:19;
hence thesis by A1,A2,Def3;
end;
theorem Th7:
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
proof
let T be non empty TopSpace;
let A be Subset of T such that
A1: A is open;
set R = Indiscernibility(T);
let C be Subset of T;
assume that
A2: C in Indiscernible(T) and
A3: C meets A;
consider y being object such that
A4: y in C and
A5: y in A by A3,XBOOLE_0:3;
consider x being object such that
x in the carrier of T and
A6: C = Class(R,x) by A2,EQREL_1:def 3;
for p being object st p in C holds p in A
proof
let p be object;
[y,x] in R by A6,A4,EQREL_1:19;
then
A7: [x,y] in R by EQREL_1:6;
assume
A8: p in C;
then [p,x] in R by A6,EQREL_1:19;
then [p,y] in R by A7,EQREL_1:7;
hence thesis by A1,A5,A8,Def3;
end;
hence thesis by TARSKI:def 3;
end;
theorem Th8:
for T being non empty TopSpace holds T_0-canonical_map(T) is open
proof
let T be non empty TopSpace;
set F = T_0-canonical_map(T);
for A being Subset of T st A is open holds F.:A is open
proof
set D = Indiscernible(T);
A1: F = proj D by BORSUK_1:def 8;
let A be Subset of T such that
A2: A is open;
A3: for C being Subset of T st C in D & C meets A holds C c= A by A2,Th7;
set A9 = F.:A;
A9 is Subset of D by BORSUK_1:def 7;
then F"A9 = union A9 by A1,EQREL_1:67;
then A = union A9 by A1,A3,EQREL_1:69;
then union A9 in the topology of T by A2;
hence thesis by Th2;
end;
hence thesis;
end;
Lm1: for T being non empty TopSpace, x,y being Point of T_0-reflex(T) st x <>
y ex V being Subset of T_0-reflex(T) st V is open & ( x in V & not y in V or y
in V & not x in V )
proof
let T be non empty TopSpace;
set S = T_0-reflex(T);
set F = T_0-canonical_map(T);
assume not (for x,y being Point of S st not x = y ex V being Subset of S st
V is open & ( x in V & not y in V or y in V & not x in V ));
then consider x,y being Point of S such that
A1: x <> y and
A2: for V being Subset of S st V is open holds x in V iff y in V;
reconsider x,y as Point of space Indiscernible(T);
consider p being Point of T such that
A3: F.p = x by BORSUK_1:29;
consider q being Point of T such that
A4: F.q = y by BORSUK_1:29;
for A being Subset of T st A is open holds p in A iff q in A
proof
let A be Subset of T such that
A5: A is open;
F is open by Th8;
then
A6: F.:A is open by A5;
reconsider F as Function of the carrier of T, the carrier of S;
hereby
assume p in A;
then x in F.:A by A3,FUNCT_2:35;
then F.q in F.:A by A2,A4,A6;
then
ex x being object st x in the carrier of T & x in A & F.q = F.x by FUNCT_2:64;
hence q in A by A5,Th6;
end;
assume q in A;
then y in F.:A by A4,FUNCT_2:35;
then F.p in F.:A by A2,A3,A6;
then ex x being object st x in the carrier of T & x in A & F.p = F.x by
FUNCT_2:64;
hence thesis by A5,Th6;
end;
then [p,q] in Indiscernibility(T) by Def3;
hence contradiction by A1,A3,A4,Th5;
end;
::
:: Discernible TopStruct
::
definition
let T be TopStruct;
redefine attr T is T_0 means :: redefines T_0 (PRE_TOPC, definition)
:Def7:
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 );
compatibility;
end;
registration
cluster T_0 non empty for TopSpace;
existence
proof
set T = the non empty TopSpace;
take T_0-reflex(T);
for x,y being Point of T_0-reflex(T) st x <> y holds ex V being Subset
of T_0-reflex(T) st V is open & ( x in V & not y in V or y in V & not x in V )
by Lm1;
hence thesis;
end;
end;
::
:: T_0 TopSpace
::
definition
mode T_0-TopSpace is T_0 non empty TopSpace;
end;
theorem
for T being non empty TopSpace holds T_0-reflex(T) is T_0-TopSpace
proof
let T be non empty TopSpace;
for x,y being Point of T_0-reflex(T) st not x = y ex A being Subset of
T_0-reflex(T) st A is open & ( x in A & not y in A or y in A & not x in A ) by
Lm1;
hence thesis by Def7;
end;
::
:: Homeomorphism of T_0 Reflexes
::
theorem
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
proof
let T,S be non empty TopSpace;
set F = T_0-canonical_map(T), G = T_0-canonical_map(S);
set TR = T_0-reflex(T), SR = T_0-reflex(S);
given h being Function of SR,TR such that
A1: h is being_homeomorphism and
A2: F,h*G are_fiberwise_equipotent;
consider f being Function such that
A3: dom f = dom F and
A4: rng f = dom (h*G) and
A5: f is one-to-one and
A6: F = h*G*f by A2,CLASSES1:77;
A7: dom f = the carrier of T by A3,FUNCT_2:def 1;
A8: h is continuous by A1;
A9: h is one-to-one by A1;
reconsider f as Function of T,S by A4,A7,FUNCT_2:def 1,RELSET_1:4;
take f;
thus
A10: dom f = [#] T & rng f = [#] S by A4,FUNCT_2:def 1;
A11: rng h = [#] TR by A1;
A12: [#]SR <> {};
A13: for A being Subset of S st A is open holds f"A is open
proof
set g=(h*G);
let A be Subset of S;
set B=g.:A;
A14: h" is continuous by A1;
assume
A15: A is open;
A16: for x1,x2 being Element of S holds x1 in A & g.x1=g.x2 implies x2 in A
proof
let x1,x2 be Element of S;
assume that
A17: x1 in A and
A18: g.x1=g.x2;
h.(G.x1) = g.x2 by A18,FUNCT_2:15;
then h.(G.x1) = h.(G.x2) by FUNCT_2:15;
then G.x1 = G.x2 by A9,FUNCT_2:19;
hence thesis by A15,A17,Th6;
end;
G is open by Th8;
then G.:A is open by A15;
then
A19: (h")"(G.:A) is open by A12,A14,TOPS_2:43;
A20: h is onto by A11,FUNCT_2:def 3;
h.:(G.:A) = (h qua Function")"(G.:A) by A9,FUNCT_1:84;
then h.:(G.:A) is open by A9,A19,A20,TOPS_2:def 4;
then
A21: (h*G).:A is open by RELAT_1:126;
[#]T_0-reflex T <> {};
then
A22: F"B is open by A21,TOPS_2:43;
F"B = f"(g"(g.:A)) by A6,RELAT_1:146;
hence thesis by A22,A16,Th1;
end;
A23: dom h = [#] SR by A1;
A24: for A being Subset of T st A is open holds (f" qua Function of S,T)"A
is open
proof
set g = h"*F;
let A be Subset of T;
set B = g.:A;
assume
A25: A is open;
A26: for x1,x2 being Element of T holds x1 in A & g.x1=g.x2 implies x2 in A
proof
let x1,x2 be Element of T;
assume that
A27: x1 in A and
A28: g.x1=g.x2;
h".(F.x1) = g.x2 by A28,FUNCT_2:15;
then
A29: h".(F.x1) = h".(F.x2) by FUNCT_2:15;
h" is one-to-one by A11,A9,TOPS_2:50;
then F.x1 = F.x2 by A29,FUNCT_2:19;
hence thesis by A25,A27,Th6;
end;
F = h*(G*f) by A6,RELAT_1:36;
then g = (h"*h)*(G*f) by RELAT_1:36;
then g = (id the carrier of SR)*(G*f) by A23,A11,A9,TOPS_2:52;
then g*f" = G*f*f" by FUNCT_2:17;
then g*f" = G*(f*f") by RELAT_1:36;
then g*f" = G*(id the carrier of S) by A5,A10,TOPS_2:52;
then G = g*f" by FUNCT_2:17;
then
A30: G"B = (f")"(g"B) by RELAT_1:146;
F is open by Th8;
then F.:A is open by A25;
then
A31: h"(F.:A) is open by A11,A8,TOPS_2:43;
B = (h").:(F.:A) by RELAT_1:126;
then G"B = G"(h"(F.:A)) by A11,A9,TOPS_2:55;
then G"B is open by A12,A31,TOPS_2:43;
hence thesis by A26,A30,Th1;
end;
thus f is one-to-one by A5;
[#]S <> {};
hence f is continuous by A13,TOPS_2:43;
[#]T <> {};
hence thesis by A24,TOPS_2:43;
end;
::
:: Properties of Continuous Mapping from TopSpace to its T_0 Reflex
::
theorem Th11:
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
proof
let T be non empty TopSpace;
let T0 be T_0-TopSpace;
let f be continuous Function of T,T0;
let p,q be Point of T;
set p9 = f.p, q9 = f.q;
assume that
A1: [p,q] in Indiscernibility(T) and
A2: not f.p = f.q;
consider V being Subset of T0 such that
A3: V is open and
A4: p9 in V & not q9 in V or q9 in V & not p9 in V by A2,Def7;
set A = f"V;
[#]T0 <> {};
then
A5: A is open by A3,TOPS_2:43;
reconsider f as Function of the carrier of T, the carrier of T0;
q in the carrier of T;
then
A6: q in dom f by FUNCT_2:def 1;
p in the carrier of T;
then p in dom f by FUNCT_2:def 1;
then not (p in A iff q in A) by A4,A6,FUNCT_1:def 7;
hence contradiction by A1,A5,Def3;
end;
theorem Th12:
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}
proof
let T be non empty TopSpace;
let T0 be T_0-TopSpace;
let f be continuous Function of T,T0;
let p be Point of T;
set R = Indiscernibility(T);
for y being object holds y in f.:Class(R,p) iff y in {f.p}
proof
let y be object;
hereby
assume y in f.:Class(R,p);
then consider x being object such that
A1: x in the carrier of T and
A2: x in Class(R,p) and
A3: y = f.x by FUNCT_2:64;
[x,p] in R by A2,EQREL_1:19;
then f.x = f.p by A1,Th11;
hence y in {f.p} by A3,TARSKI:def 1;
end;
assume y in {f.p};
then
A4: y = f.p by TARSKI:def 1;
p in Class(R,p) by EQREL_1:20;
hence thesis by A4,FUNCT_2:35;
end;
hence thesis by TARSKI:2;
end;
::
:: Factorization
::
theorem
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)
proof
let T be non empty TopSpace;
let T0 be T_0-TopSpace;
let f be continuous Function of T,T0;
set F = T_0-canonical_map(T);
set R = Indiscernibility(T);
set TR = T_0-reflex(T);
defpred X[object,object] means ex D1 being set st D1 = $1 & $2 in f.:D1;
A1: for C being object st C in the carrier of TR
ex y being object st y in the carrier of T0 & X[C,y]
proof
let C be object;
assume C in the carrier of TR;
then consider p being Point of T such that
A2: C = Class(R,p) by Th3;
A3: f.p in {f.p} by TARSKI:def 1;
reconsider C as set by TARSKI:1;
f.:C = {f.p} by A2,Th12;
hence thesis by A3;
end;
ex h being Function of the carrier of TR,the carrier of T0 st for C
being object st C in the carrier of TR holds X[C,h.C]
from FUNCT_2:sch 1(A1);
then consider h being Function of the carrier of TR,the carrier of T0
such that
A4: for C being object st C in the carrier of TR holds X[C,h.C];
A5: for p being Point of T holds h.Class(R,p) = f.p
proof
let p be Point of T;
Class(R,p) is Point of TR by Th3;
then X[Class(R,p),h.Class(R,p)] by A4;
then h.Class(R,p) in f.:Class(R,p);
then h.Class(R,p) in {f.p} by Th12;
hence thesis by TARSKI:def 1;
end;
reconsider h as Function of TR,T0;
A6: [#]T0 <> {};
for W being Subset of T0 st W is open holds h"W is open
proof
let W be Subset of T0;
assume W is open;
then
A7: f"W is open by A6,TOPS_2:43;
set V = h"W;
for x being object holds x in union V iff x in f"W
proof
let x be object;
hereby
assume x in union V;
then consider C being set such that
A8: x in C and
A9: C in V by TARSKI:def 4;
consider p being Point of T such that
A10: C = Class(R,p) by A9,Th3;
x in the carrier of T by A8,A10;
then
A11: x in dom f by FUNCT_2:def 1;
[x,p] in R by A8,A10,EQREL_1:19;
then
A12: C = Class(R,x) by A8,A10,EQREL_1:35;
h.C in W by A9,FUNCT_1:def 7;
then f.x in W by A5,A8,A12;
hence x in f"W by A11,FUNCT_1:def 7;
end;
assume
A13: x in f"W;
then f.x in W by FUNCT_1:def 7;
then
A14: h.Class(R,x) in W by A5,A13;
Class(R,x) is Point of TR by A13,Th3;
then
A15: Class(R,x) in V by A14,FUNCT_2:38;
x in Class(R,x) by A13,EQREL_1:20;
hence thesis by A15,TARSKI:def 4;
end;
then union V = f"W by TARSKI:2;
then union V in the topology of T by A7;
hence thesis by Th2;
end;
then reconsider h as continuous Function of TR,T0 by A6,TOPS_2:43;
set H = h*F;
for x being object st x in the carrier of T holds f.x = H.x
proof
let x be object;
assume
A16: x in the carrier of T;
then Class(R,x) in Class R by EQREL_1:def 3;
then
A17: Class(R,x) in the carrier of TR by BORSUK_1:def 7;
x in dom F & F.x = Class(R,x) by A16,Th4,FUNCT_2:def 1;
then
A18: (h*F).x = h.Class(R,x) by FUNCT_1:13;
X[Class(R,x),h.Class(R,x)] by A4,A17;
then H.x in f.:Class(R,x) by A18;
then H.x in {f.x} by A16,Th12;
hence thesis by TARSKI:def 1;
end;
hence thesis by FUNCT_2:12;
end;