The abstract of the Mizar article:

On \Tone\ Reflex of Topological Space

by

Adam Naumowicz, and

Mariusz \Lapinski

Received March 7, 1998

MML identifier: T_1TOPSP

[ Mizar article, MML identifier index ]

environ

 vocabulary FUNCT_1, RELAT_1, PRE_TOPC, EQREL_1, BORSUK_1, TARSKI, BOOLE,
      SUBSET_1, SETFAM_1, PROB_1, URYSOHN1, ORDINAL2, T_1TOPSP;
 notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_1, FUNCT_1, FUNCT_2,
      SETFAM_1, STRUCT_0, PRE_TOPC, EQREL_1, TOPS_2, URYSOHN1, BORSUK_1;
 constructors URYSOHN1, TOPS_2;
 clusters PRE_TOPC, BORSUK_1, STRUCT_0, FSM_1, FUNCT_1, RELSET_1, SUBSET_1,
      XBOOLE_0, EQREL_1, PARTFUN1;
 requirements BOOLE, SUBSET;


begin

reserve X for non empty set, x for Element of X, y,v,w for set;

canceled;

theorem :: T_1TOPSP:2
 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;

theorem :: T_1TOPSP:3
 for X being non empty set,
     S being a_partition of X,
     A being Subset of S holds (union S) \ (union A) = union (S \ A);

theorem :: T_1TOPSP:4
 for X being non empty set,A being Subset of X,
     S being a_partition of X holds A in S implies union(S \ {A}) = X \ A;

theorem :: T_1TOPSP:5
 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);

:: Classes of partitions of a set

definition
 let X be non empty set,x be Element of X,S1 be a_partition of X;
 func EqClass(x,S1) -> Subset of X means
:: T_1TOPSP:def 1
 x in it & it in S1;
end;

theorem :: T_1TOPSP:6
 for S1,S2 being a_partition of X st
 (for x being Element of X holds EqClass(x,S1) = EqClass(x,S2)) holds S1=S2;

theorem :: T_1TOPSP:7
 for X being non empty set holds {X} is a_partition of X;

definition let X be set;
  mode Family-Class of X means
:: T_1TOPSP:def 2
   it c= bool bool X;
end;

definition let X be set;
 let F be Family-Class of X;
 attr F is partition-membered means
:: T_1TOPSP:def 3
   for S being set st S in F holds S is a_partition of X;
end;

definition let X be set;
 cluster partition-membered Family-Class of X;
end;

definition let X be set;
  mode Part-Family of X is partition-membered Family-Class of X;
end;

reserve F for Part-Family of X;

definition
 let X be non empty set;
 cluster non empty a_partition of X;
end;

theorem :: T_1TOPSP:8
 for X being set, p being a_partition of X holds
  {p} is Part-Family of X;

definition
 let X be set;
 cluster non empty Part-Family of X;
end;

theorem :: T_1TOPSP:9
 for S1 being a_partition of X,
     x,y being Element of X holds
    EqClass(x,S1) meets EqClass(y,S1) implies EqClass(x,S1) = EqClass(y,S1);

theorem :: T_1TOPSP:10
 for A being set,X being non empty set,S being a_partition of X holds
 A in S implies ex x being Element of X st A = EqClass(x,S);

definition
 let X be non empty set,F be non empty Part-Family of X;
 func Intersection F -> non empty a_partition of X means
:: T_1TOPSP:def 4
 for x being Element of X holds EqClass(x,it)
  = meet{EqClass(x,S) where S is a_partition of X : S in F};
end;

:: Families of partitions of topological spaces

reserve T for non empty TopSpace;

theorem :: T_1TOPSP:11
 { A where A is a_partition of the carrier of T : A is closed } is
                                        Part-Family of the carrier of T;

definition
 let T;
 func Closed_Partitions T -> non empty Part-Family of the carrier of T equals
:: T_1TOPSP:def 5

 { A where A is a_partition of the carrier of T : A is closed };
end;

:: T_1 reflex of a topological space

definition
 let T be non empty TopSpace;
 func T_1-reflex T -> TopSpace equals
:: T_1TOPSP:def 6
   space (Intersection Closed_Partitions T);
end;

definition
 let T;
 cluster T_1-reflex T -> strict non empty;
end;

theorem :: T_1TOPSP:12
 for T being non empty TopSpace holds T_1-reflex T is being_T1;

definition let T;
 cluster T_1-reflex T -> being_T1;
end;

definition
 let T be non empty TopSpace;
  func T_1-reflect T -> continuous map of T,T_1-reflex T equals
:: T_1TOPSP:def 7
   Proj Intersection Closed_Partitions T;
end;

theorem :: T_1TOPSP:13
 for T,T1 being non empty TopSpace,f being continuous map of T,T1 holds
   T1 is being_T1 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);

theorem :: T_1TOPSP:14
 for T,T1 being non empty TopSpace,f being continuous map of T,T1 holds
   T1 is being_T1 implies for w for x being Element of T holds
    w = EqClass(x,(Intersection Closed_Partitions T)) implies w c= f"{f.x};

theorem :: T_1TOPSP:15
 for T,T1 being non empty TopSpace,f being continuous map of T,T1 holds
   T1 is being_T1 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};

:: The theorem on factorization

theorem :: T_1TOPSP:16
 for T,T1 being non empty TopSpace,f being continuous map of T,T1 holds
   T1 is being_T1 implies
    ex h being continuous map of T_1-reflex T, T1 st
     f = h*T_1-reflect T;

definition
 let T,S be non empty TopSpace;
 let f be continuous map of T,S;
  func T_1-reflex f -> continuous map of T_1-reflex T, T_1-reflex S means
:: T_1TOPSP:def 8
   (T_1-reflect S) * f = it * (T_1-reflect T);
end;