:: On $T_{1}$ Reflex of Topological Space
:: by Adam Naumowicz and Mariusz {\L}api\'nski
::
:: Received March 7, 1998
:: Copyright (c) 1998-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, PRE_TOPC, EQREL_1, STRUCT_0, SUBSET_1, BORSUK_1,
RELAT_1, TARSKI, CARD_3, RCOMP_1, ZFMISC_1, SETFAM_1, ORDINAL2, FUNCT_1,
T_1TOPSP;
notations TARSKI, XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1, RELSET_1, PARTFUN1,
FUNCT_2, SETFAM_1, DOMAIN_1, STRUCT_0, PRE_TOPC, EQREL_1, TOPS_2,
BORSUK_1;
constructors TOPS_2, BORSUK_1;
registrations SUBSET_1, FUNCT_1, RELSET_1, FUNCT_2, EQREL_1, STRUCT_0,
PRE_TOPC, BORSUK_1;
requirements BOOLE, SUBSET;
definitions TARSKI, PRE_TOPC, XBOOLE_0;
equalities XBOOLE_0, STRUCT_0;
expansions TARSKI, PRE_TOPC, XBOOLE_0;
theorems PRE_TOPC, TARSKI, SETFAM_1, EQREL_1, URYSOHN1, BORSUK_1, FUNCT_2,
FUNCT_1, TOPS_2, RELSET_1, RELAT_1, XBOOLE_0, XBOOLE_1;
schemes CLASSES1;
begin
reserve y,w for set;
theorem Th1:
for T being non empty TopSpace, A being non empty a_partition of
the carrier of T, y being Subset of space A holds (Proj(A))"y = union y
proof
let T be non empty TopSpace;
let A be non empty a_partition of the carrier of T;
let y be Subset of space A;
reconsider y as Subset of A by BORSUK_1:def 7;
(Proj(A))"y = (proj A)"y by BORSUK_1:def 8
.= union y by EQREL_1:67;
hence thesis;
end;
theorem Th2:
for T being non empty TopSpace, S being non empty a_partition of
the carrier of T, A being Subset of space S, B being Subset of T holds B =
union A implies (A is closed iff B is closed)
proof
let T be non empty TopSpace;
let S be non empty a_partition of the carrier of T;
let A be Subset of space S;
let B be Subset of T;
reconsider C = A as Subset of S by BORSUK_1:def 7;
A1: [#](T) \ union A = (union S) \ (union C) by EQREL_1:def 4
.= union (S \ A) by EQREL_1:43
.= union ([#](space S) \ A) by BORSUK_1:def 7;
assume
A2: B = union A;
thus A is closed implies B is closed
proof
reconsider om = [#](space S) \ A as Subset of S by BORSUK_1:def 7;
assume A is closed;
then [#](space S) \ A is open;
then om in the topology of space S;
then [#](T) \ B in the topology of T by A2,A1,BORSUK_1:27;
then [#](T) \ B is open;
hence thesis;
end;
thus B is closed implies A is closed
proof
reconsider om = [#](space S) \ A as Subset of S by BORSUK_1:def 7;
assume B is closed;
then [#](T) \ B is open;
then [#](T) \ union A in the topology of T by A2;
then om in the topology of space S by A1,BORSUK_1:27;
then [#](space S) \ A is open;
hence thesis;
end;
end;
::reserve F for Part-Family of X;
:: Families of partitions of topological spaces
reserve T for non empty TopSpace;
theorem Th3:
{ A where A is a_partition of the carrier of T : A is closed }
is Part-Family of the carrier of T
proof
set S = { A where A is a_partition of the carrier of T : A is closed };
A1: now
let B be set;
assume B in { A where A is a_partition of the carrier of T : A is closed };
then ex A being a_partition of the carrier of T st B = A & A is closed;
hence B is a_partition of the carrier of T;
end;
S c= bool bool the carrier of T
proof
let B be object;
assume B in S;
then ex A being a_partition of the carrier of T st B = A & A is closed;
hence thesis;
end;
hence thesis by A1,EQREL_1:def 7;
end;
definition
let T;
func Closed_Partitions T -> non empty Part-Family of the carrier of T equals
{ A where A is a_partition of the carrier of T : A is closed };
coherence
proof
reconsider ct = {the carrier of T} as a_partition of the carrier of T by
EQREL_1:39;
set F = { A where A is a_partition of the carrier of T : A is closed };
for A being Subset of T st A in ct holds A is closed
by TARSKI:def 1;
then ct is closed by TOPS_2:def 2;
then ct in F;
hence thesis by Th3;
end;
end;
:: T_1 reflex of a topological space
definition
let T be non empty TopSpace;
func T_1-reflex T -> TopSpace equals
space (Intersection Closed_Partitions T
);
correctness;
end;
registration
let T;
cluster T_1-reflex T -> strict non empty;
coherence;
end;
theorem Th4:
for T being non empty TopSpace holds T_1-reflex T is T_1
proof
let T be non empty TopSpace;
now
let p be Point of T_1-reflex T;
reconsider I = (Intersection Closed_Partitions T) \ {p} as Subset of (
Intersection Closed_Partitions T) by XBOOLE_1:36;
A1: the carrier of T_1-reflex T = Intersection Closed_Partitions T by
BORSUK_1:def 7;
then consider x being Element of T such that
A2: p = EqClass(x,Intersection Closed_Partitions T) by EQREL_1:42;
reconsider q=p as Subset of T by A2;
A3: { EqClass(x,S) where S is a_partition of the carrier of T : S in
Closed_Partitions T } c= bool the carrier of T
proof
let Z be object;
assume Z in { EqClass(x,S) where S is a_partition of the carrier of T
: S in Closed_Partitions T };
then ex Y being a_partition of the carrier of T st Z = EqClass( x,Y) & Y
in Closed_Partitions T;
hence thesis;
end;
{ EqClass(x,S) where S is a_partition of the carrier of T : S in
Closed_Partitions T } is non empty
proof
consider Y being object such that
A4: Y in Closed_Partitions T by XBOOLE_0:def 1;
reconsider Y as a_partition of the carrier of T by A4,EQREL_1:def 7;
EqClass(x,Y) in {EqClass(x,S) where S is a_partition of the carrier
of T : S in Closed_Partitions T} by A4;
hence thesis;
end;
then reconsider
m = { EqClass(x,S) where S is a_partition of the carrier of T:
S in Closed_Partitions T } as non empty Subset-Family of T by A3;
reconsider m as non empty Subset-Family of T;
A5: for A being Subset of T st A in m holds A is closed
proof
let A be Subset of T;
assume A in m;
then consider S being a_partition of the carrier of T such that
A6: A = EqClass(x,S) & S in Closed_Partitions T;
(ex B being a_partition of the carrier of T st S = B & B is closed
)& A in S by A6,EQREL_1:def 6;
hence thesis by TOPS_2:def 2;
end;
p = meet { EqClass(x,S) where S is a_partition of the carrier of T : S
in Closed_Partitions T } by A2,EQREL_1:def 8;
then q is closed by A5,PRE_TOPC:14;
then [#](T) \ q is open;
then
A7: [#](T) \ p in the topology of T;
p in Intersection Closed_Partitions T by A1;
then union((Intersection Closed_Partitions T) \ {p}) in the topology of T
by A7,EQREL_1:44;
then
A8: I in {A where A is Subset of (Intersection Closed_Partitions T) :
union A in the topology of T};
reconsider I as Subset of space(Intersection Closed_Partitions T) by
BORSUK_1:def 7;
reconsider I as Subset of T_1-reflex T;
the topology of space(Intersection Closed_Partitions T) = {A where A
is Subset of (Intersection Closed_Partitions T) : union A in the topology of T}
& I = ([#] T_1-reflex T) \ {p} by BORSUK_1:def 7;
then ([#] T_1-reflex T) \ {p} is open by A8;
hence {p} is closed;
end;
hence thesis by URYSOHN1:19;
end;
registration
let T;
cluster T_1-reflex T -> T_1;
coherence by Th4;
end;
registration
cluster T_1 non empty for TopSpace;
existence
proof
set T = the non empty TopSpace;
take T_1-reflex T;
thus thesis;
end;
end;
definition
let T be non empty TopSpace;
func T_1-reflect T -> continuous Function of T,T_1-reflex T equals
Proj
Intersection Closed_Partitions T;
correctness;
end;
theorem Th5:
for T,T1 being non empty TopSpace,f being continuous Function of
T,T1 holds T1 is T_1 implies {f"{z} where z is Element of T1 : z in rng f} is
a_partition of the carrier of T & for A being Subset of T st A in {f"{z} where
z is Element of T1 : z in rng f} holds A is closed
proof
let T,T1 be non empty TopSpace;
let f be continuous Function of T,T1;
assume
A1: T1 is T_1;
A2: dom f = the carrier of T by FUNCT_2:def 1;
thus {f"{z} where z is Element of T1 : z in rng f} is a_partition of the
carrier of T
proof
{f"{z} where z is Element of T1 : z in rng f} c= bool the carrier of T
proof
let y be object;
assume y in {f"{z} where z is Element of T1 : z in rng f};
then ex z being Element of T1 st y = f"{z} & z in rng f;
hence thesis;
end;
then reconsider fz = {f"{z} where z is Element of T1 : z in rng f} as
Subset-Family of T;
reconsider fz as Subset-Family of T;
A3: for A being Subset of T st A in fz holds A <> {} & for B being Subset
of T st B in fz holds A = B or A misses B
proof
let A be Subset of T;
assume A in fz;
then consider z being Element of T1 such that
A4: A = f"{z} and
A5: z in rng f;
consider y being object such that
A6: y in dom f & z = f.y by A5,FUNCT_1:def 3;
f.y in {f.y} by TARSKI:def 1;
hence A <> {} by A4,A6,FUNCT_1:def 7;
let B be Subset of T;
assume B in fz;
then consider w being Element of T1 such that
A7: B = f"{w} and
w in rng f;
now
assume not A misses B;
then consider v being object such that
A8: v in A and
A9: v in B by XBOOLE_0:3;
f.v in {z} by A4,A8,FUNCT_1:def 7;
then
A10: f.v = z by TARSKI:def 1;
f.v in {w} by A7,A9,FUNCT_1:def 7;
hence A = B by A4,A7,A10,TARSKI:def 1;
end;
hence A = B or A misses B;
end;
the carrier of T c= union fz
proof
let y be object;
consider z being set such that
A11: z = f.y;
assume
A12: y in the carrier of T;
then
A13: z in rng f by A2,A11,FUNCT_1:def 3;
then reconsider z as Element of T1;
A14: f"{z} in fz by A13;
f.y in {f.y} by TARSKI:def 1;
then y in f"{z} by A2,A12,A11,FUNCT_1:def 7;
hence thesis by A14,TARSKI:def 4;
end;
then union fz = the carrier of T;
hence thesis by A3,EQREL_1:def 4;
end;
thus for A being Subset of T st A in {f"{z} where z is Element of T1 : z in
rng f} holds A is closed
proof
let A be Subset of T;
assume A in {f"{z} where z is Element of T1 : z in rng f};
then consider z being Element of T1 such that
A15: A = f"{z} and
z in rng f;
{z} is closed by A1,URYSOHN1:19;
hence thesis by A15,PRE_TOPC:def 6;
end;
end;
theorem Th6:
for T,T1 being non empty TopSpace,f being continuous Function of
T,T1 holds T1 is T_1 implies for w for x being Element of T holds w = EqClass(x
,(Intersection Closed_Partitions T)) implies w c= f"{f.x}
proof
let T,T1 be non empty TopSpace;
let f be continuous Function of T,T1;
assume
A1: T1 is T_1;
then reconsider
fz = {f"{z} where z is Element of T1 : z in rng f} as a_partition
of the carrier of T by Th5;
let w be set;
let x be Element of T;
for A being Subset of T st A in fz holds A is closed by A1,Th5;
then fz is closed by TOPS_2:def 2;
then fz in {B where B is a_partition of the carrier of T : B is closed};
then
A2: EqClass(x,fz) in {EqClass(x,S) where S is a_partition of the carrier of
T: S in Closed_Partitions T};
assume
A3: w = EqClass(x,(Intersection Closed_Partitions T));
A4: dom f = the carrier of T by FUNCT_2:def 1;
A5: f"{f.x} = EqClass(x,fz)
proof
reconsider fx = f.x as Element of T1;
f.x in rng f by A4,FUNCT_1:def 3;
then
A6: f"{fx} in fz;
f.x in {f.x} by TARSKI:def 1;
then x in f"{f.x} by A4,FUNCT_1:def 7;
hence thesis by A6,EQREL_1:def 6;
end;
let y be object;
A7: EqClass(x,(Intersection Closed_Partitions T)) = meet{EqClass(x,S) where
S is a_partition of the carrier of T : S in Closed_Partitions T} by
EQREL_1:def 8;
assume y in w;
hence thesis by A3,A2,A5,A7,SETFAM_1:def 1;
end;
theorem Th7:
for T,T1 being non empty TopSpace,f being continuous Function of
T,T1 holds T1 is T_1 implies for w st w in the carrier of T_1-reflex T ex z
being Element of T1 st z in rng f & w c= f"{z}
proof
let T,T1 be non empty TopSpace;
let f be continuous Function of T,T1;
assume
A1: T1 is T_1;
let w be set;
assume w in the carrier of T_1-reflex T;
then w in Intersection (Closed_Partitions T) by BORSUK_1:def 7;
then consider x being Element of T such that
A2: w = EqClass(x,Intersection (Closed_Partitions T)) by EQREL_1:42;
reconsider x as Element of T;
reconsider fx = f.x as Element of T1;
take fx;
dom f = the carrier of T by FUNCT_2:def 1;
hence thesis by A1,A2,Th6,FUNCT_1:def 3;
end;
:: The theorem on factorization
theorem Th8:
for T,T1 being non empty TopSpace,f being continuous Function of
T,T1 holds T1 is T_1 implies ex h being continuous Function of T_1-reflex T, T1
st f = h*T_1-reflect T
proof
let T,T1 be non empty TopSpace;
let f be continuous Function of T,T1;
set g = T_1-reflect T;
A1: dom g = the carrier of T by FUNCT_2:def 1;
defpred X[object,object] means
ex D1 being set st D1 = $1 &
for z being Element of T1 holds (z in rng f & D1 c=
f"{z}) implies $2 = f"{z};
assume
A2: T1 is T_1;
then reconsider
fx = {f"{x} where x is Element of T1 : x in rng f} as a_partition
of the carrier of T by Th5;
A3: dom f = the carrier of T by FUNCT_2:def 1;
A4: for y being object st y in the carrier of T_1-reflex T
ex w being object st X[y,w]
proof
let y be object;
assume y in the carrier of T_1-reflex T;
then y in Intersection(Closed_Partitions T) by BORSUK_1:def 7;
then consider x being Element of T such that
A5: y = EqClass(x,Intersection(Closed_Partitions T)) by EQREL_1:42;
reconsider x as Element of T;
set w = f"{f.x};
reconsider yy=y as set by TARSKI:1;
take w,yy;
thus yy = y;
let z be Element of T1;
assume that
A6: z in rng f and
A7: yy c= f"{z};
reconsider fix = f.x as Element of T1;
f.x in rng f by A3,FUNCT_1:def 3;
then
A8: f"{fix} in fx;
yy is non empty by A5,EQREL_1:def 6;
then
A9: ex z1 being object st z1 in yy;
f"{z} in fx by A6;
then
A10: w misses f"{z} or w = f"{z} by A8,EQREL_1:def 4;
yy c= w by A2,A5,Th6;
hence thesis by A7,A10,A9,XBOOLE_0:3;
end;
consider h1 being Function such that
A11: dom h1 = the carrier of T_1-reflex T &
for y being object st y in the carrier of
T_1-reflex T holds X[y,h1.y] from CLASSES1:sch 1(A4);
defpred X1[object,object] means
for z being Element of T1 holds (z in rng f & $1 =
f"{z}) implies $2 = z;
A12: for y being object st y in fx ex w being object st X1[y,w]
proof
let y be object;
assume y in fx;
then consider w being Element of T1 such that
A13: y = f"{w} and
w in rng f;
take w;
let z be Element of T1;
assume that
A14: z in rng f and
A15: y = f"{z};
now
assume
A16: z <> w;
consider v being object such that
A17: v in dom f and
A18: z = f.v by A14,FUNCT_1:def 3;
z in {z} by TARSKI:def 1;
then v in f"{w} by A13,A15,A17,A18,FUNCT_1:def 7;
then f.v in {w} by FUNCT_1:def 7;
hence contradiction by A16,A18,TARSKI:def 1;
end;
hence thesis;
end;
consider h2 being Function such that
A19: dom h2 = fx &
for y being object st y in fx holds X1[y,h2.y] from CLASSES1:sch 1(
A12);
set h = h2*h1;
A20: dom h = the carrier of T_1-reflex T
proof
thus dom h c= the carrier of T_1-reflex T by A11,RELAT_1:25;
let z be object;
reconsider zz=z as set by TARSKI:1;
assume
A21: z in the carrier of T_1-reflex T;
then consider w being Element of T1 such that
A22: w in rng f and
A23: zz c= f"{w} by A2,Th7;
X[z,h1.z] by A11,A21;
then h1.z = f"{w} by A22,A23;
then h1.z in dom h2 by A19,A22;
hence thesis by A11,A21,FUNCT_1:11;
end;
A24: dom (h*g) = the carrier of T
proof
thus dom (h*g) c= the carrier of T by A1,RELAT_1:25;
let y be object;
assume
A25: y in the carrier of T;
then g.y in rng g by A1,FUNCT_1:def 3;
hence thesis by A1,A20,A25,FUNCT_1:11;
end;
A26: for x being object st x in dom f holds f.x = (h*g).x
proof
let x be object;
assume
A27: x in dom f;
then g.x in rng g by A1,FUNCT_1:def 3;
then g.x in the carrier of T_1-reflex T;
then g.x in Intersection (Closed_Partitions T) by BORSUK_1:def 7;
then consider y being Element of T such that
A28: g.x = EqClass(y,Intersection (Closed_Partitions T)) by EQREL_1:42;
reconsider x as Element of T by A27;
reconsider fix = f.x as Element of T1;
A29: x in EqClass(x,Intersection (Closed_Partitions T)) by EQREL_1:def 6;
g = proj (Intersection Closed_Partitions T) by BORSUK_1:def 8;
then x in g.x by EQREL_1:def 9;
then EqClass(x,Intersection (Closed_Partitions T)) meets EqClass(y,
Intersection (Closed_Partitions T)) by A28,A29,XBOOLE_0:3;
then
A30: g.x c= f"{fix} by A2,A28,Th6,EQREL_1:41;
A31: fix in rng f by A27,FUNCT_1:def 3;
then
A32: f"{fix} in fx;
A33: X[g.x,h1.(g.x)] by A11;
(h*g).x = (h2*h1).(g.x) by A24,FUNCT_1:12
.= h2.(h1.(g.x)) by A11,FUNCT_1:13
.= h2.(f"{fix}) by A31,A30,A33
.= f.x by A19,A31,A32;
hence thesis;
end;
then
A34: f = h*g by A3,A24,FUNCT_1:2;
A35: rng h2 c= the carrier of T1
proof
let y be object;
assume y in rng h2;
then consider w being object such that
A36: w in dom h2 and
A37: y = h2.w by FUNCT_1:def 3;
consider x being Element of T1 such that
A38: w = f"{x} & x in rng f by A19,A36;
h2.w = x by A19,A36,A38;
hence thesis by A37;
end;
rng h c= rng h2
by FUNCT_1:14;
then rng h c= the carrier of T1 by A35;
then reconsider
h as Function of the carrier of T_1-reflex T,the carrier of T1 by A20,
FUNCT_2:def 1,RELSET_1:4;
reconsider h as Function of T_1-reflex T,T1;
h is continuous
proof
let y be Subset of T1;
reconsider hy = h"y as Subset of space Intersection(Closed_Partitions T);
union hy c= the carrier of T
proof
let z1 be object;
assume z1 in union hy;
then consider z2 being set such that
A39: z1 in z2 and
A40: z2 in hy by TARSKI:def 4;
z2 in the carrier of space Intersection(Closed_Partitions T) by A40;
then z2 in Intersection(Closed_Partitions T) by BORSUK_1:def 7;
hence thesis by A39;
end;
then reconsider uhy = union hy as Subset of T;
assume y is closed;
then (h*g)"y is closed by A34,PRE_TOPC:def 6;
then g"(h"y) is closed by RELAT_1:146;
then uhy is closed by Th1;
hence thesis by Th2;
end;
then reconsider h as continuous Function of T_1-reflex T,T1;
take h;
thus thesis by A3,A24,A26,FUNCT_1:2;
end;
definition
let T,S be non empty TopSpace;
let f be continuous Function of T,S;
func T_1-reflex f -> continuous Function of T_1-reflex T, T_1-reflex S means
(T_1-reflect S) * f = it * (T_1-reflect T);
existence by Th8;
uniqueness
proof
let g1,g2 be continuous Function of T_1-reflex T, T_1-reflex S;
assume
A1: (T_1-reflect S) * f = g1 * (T_1-reflect T) & (T_1-reflect S) * f =
g2 * ( T_1-reflect T);
A2: now
let x be object;
assume
A3: x in dom g1;
then
A4: x in the carrier of T_1-reflex T;
A5: the carrier of T_1-reflex T = (Intersection Closed_Partitions T) by
BORSUK_1:def 7;
then consider y being Element of T such that
A6: x = EqClass(y,(Intersection (Closed_Partitions T))) by A3,EQREL_1:42;
reconsider y as Element of T;
set ty=(T_1-reflect T).y;
reconsider xx=x as set by TARSKI:1;
ty in (Intersection Closed_Partitions T) by A5;
then
A7: ty misses xx or ty = x by A4,A5,EQREL_1:def 4;
T_1-reflect T = proj (Intersection Closed_Partitions T) by BORSUK_1:def 8
;
then
A8: dom (T_1-reflect T) = the carrier of T & y in (T_1-reflect T).y by
EQREL_1:def 9,FUNCT_2:def 1;
A9: y in xx by A6,EQREL_1:def 6;
hence g2.x = (g2 * (T_1-reflect T)).y by A8,A7,FUNCT_1:13,XBOOLE_0:3
.= g1.x by A1,A8,A9,A7,FUNCT_1:13,XBOOLE_0:3;
end;
dom g1 = the carrier of (T_1-reflex T) & dom g2 = the carrier of (
T_1-reflex T) by FUNCT_2:def 1;
hence g1=g2 by A2,FUNCT_1:2;
end;
end;