:: On $T_{1}$ Reflex of Topological Space
::  by Adam Naumowicz and Mariusz {\L}api\'nski
::
:: Received March 7, 1998
:: Copyright (c) 1998-2012 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, STRUCT_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 by PRE_TOPC:def 3;
    then om in the topology of space S by PRE_TOPC:def 2;
    then [#](T) \ B in the topology of T by A2,A1,BORSUK_1:27;
    then [#](T) \ B is open by PRE_TOPC:def 2;
    hence thesis by PRE_TOPC:def 3;
  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 by PRE_TOPC:def 3;
    then [#](T) \ union A in the topology of T by A2,PRE_TOPC:def 2;
    then om in the topology of space S by A1,BORSUK_1:27;
    then [#](space S) \ A is open by PRE_TOPC:def 2;
    hence thesis by PRE_TOPC:def 3;
  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 set;
    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
    proof
      let A be Subset of T;
      assume A in ct;
      then A = [#](T) by TARSKI:def 1;
      hence thesis;
    end;
    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 set;
      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 set 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 by PRE_TOPC:def 3;
    then
A7: [#](T) \ p in the topology of T by PRE_TOPC:def 2;
    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,PRE_TOPC:def 2;
    hence {p} is closed by PRE_TOPC:def 3;
  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;
      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 set 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 set 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;
      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 by XBOOLE_0:def 10;
    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 set;
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[set,set] means for z being Element of T1 holds (z in rng f & $1 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 st y in the carrier of T_1-reflex T ex w st X[y,w]
  proof
    let y;
    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};
    take w;
    let z be Element of T1;
    assume that
A6: z in rng f and
A7: y 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;
    y is non empty by A5,EQREL_1:def 6;
    then
A9: ex z1 being set st z1 in y by XBOOLE_0:def 1;
    f"{z} in fx by A6;
    then
A10: w misses f"{z} or w = f"{z} by A8,EQREL_1:def 4;
    y 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 st y in the carrier of
  T_1-reflex T holds X[y,h1.y] from CLASSES1:sch 1(A4);
  defpred X[set,set] means for z being Element of T1 holds (z in rng f & $1 =
  f"{z}) implies $2 = z;
A12: for y st y in fx ex w st X[y,w]
  proof
    let y be set;
    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 set 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 st y in fx holds X[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 set;
    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: z c= f"{w} by A2,Th7;
    h1.z = f"{w} by A11,A21,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 set;
    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 set st x in dom f holds f.x = (h*g).x
  proof
    let x be set;
    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;
    (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 A11,A31,A30
      .= f.x by A19,A31,A32;
    hence thesis;
  end;
  then
A33: f = h*g by A3,A24,FUNCT_1:2;
A34: rng h2 c= the carrier of T1
  proof
    let y;
    assume y in rng h2;
    then consider w being set such that
A35: w in dom h2 and
A36: y = h2.w by FUNCT_1:def 3;
    consider x being Element of T1 such that
A37: w = f"{x} & x in rng f by A19,A35;
    h2.w = x by A19,A35,A37;
    hence thesis by A36;
  end;
  rng h c= rng h2
  proof
    let z be set;
    thus thesis by FUNCT_1:14;
  end;
  then rng h c= the carrier of T1 by A34,XBOOLE_1:1;
  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 set;
      assume z1 in union hy;
      then consider z2 being set such that
A38:  z1 in z2 and
A39:  z2 in hy by TARSKI:def 4;
      z2 in the carrier of space Intersection(Closed_Partitions T) by A39;
      then z2 in Intersection(Closed_Partitions T) by BORSUK_1:def 7;
      hence thesis by A38;
    end;
    then reconsider uhy = union hy as Subset of T;
    assume y is closed;
    then (h*g)"y is closed by A33,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 set;
      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;
      ty in (Intersection Closed_Partitions T) by A5;
      then
A7:   ty misses x 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 x 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;