t_1topsp.miz



    begin

    reserve y,w for set;

    theorem :: T_1TOPSP:1

    

     Th1: for T be non empty TopSpace, A be non empty a_partition of the carrier of T, y be 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 :: T_1TOPSP:2

    

     Th2: for T be non empty TopSpace, S be non empty a_partition of the carrier of T, A be Subset of ( space S), B be 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 T for non empty TopSpace;

    theorem :: T_1TOPSP:3

    

     Th3: { A where A be a_partition of the carrier of T : A is closed } is Part-Family of the carrier of T

    proof

      set S = { A where A be a_partition of the carrier of T : A is closed };

       A1:

      now

        let B be set;

        assume B in { A where A be a_partition of the carrier of T : A is closed };

        then ex A be 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 be 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;

      :: T_1TOPSP:def1

      func Closed_Partitions T -> non empty Part-Family of the carrier of T equals { A where A be 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 be a_partition of the carrier of T : A is closed };

        for A be 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

    definition

      let T be non empty TopSpace;

      :: T_1TOPSP:def2

      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 :: T_1TOPSP:4

    

     Th4: for T be 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 be 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 be 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 be a_partition of the carrier of T : S in ( Closed_Partitions T) };

          then ex Y be 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 be a_partition of the carrier of T : S in ( Closed_Partitions T) } is non empty

        proof

          consider Y be 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 be 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 be 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 be 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 be a_partition of the carrier of T such that

           A6: A = ( EqClass (x,S)) & S in ( Closed_Partitions T);

          (ex B be 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 be 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 be 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 be 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;

      :: T_1TOPSP:def3

      func T_1-reflect T -> continuous Function of T, ( T_1-reflex T) equals ( Proj ( Intersection ( Closed_Partitions T)));

      correctness ;

    end

    theorem :: T_1TOPSP:5

    

     Th5: for T,T1 be non empty TopSpace, f be continuous Function of T, T1 holds T1 is T_1 implies { (f " {z}) where z be Element of T1 : z in ( rng f) } is a_partition of the carrier of T & for A be Subset of T st A in { (f " {z}) where z be 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 be Element of T1 : z in ( rng f) } is a_partition of the carrier of T

      proof

        { (f " {z}) where z be 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 be Element of T1 : z in ( rng f) };

          then ex z be Element of T1 st y = (f " {z}) & z in ( rng f);

          hence thesis;

        end;

        then

        reconsider fz = { (f " {z}) where z be Element of T1 : z in ( rng f) } as Subset-Family of T;

        reconsider fz as Subset-Family of T;

        

         A3: for A be Subset of T st A in fz holds A <> {} & for B be 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 be Element of T1 such that

           A4: A = (f " {z}) and

           A5: z in ( rng f);

          consider y be 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 be Element of T1 such that

           A7: B = (f " {w}) and w in ( rng f);

          now

            assume not A misses B;

            then

            consider v be 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 be 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 be Subset of T st A in { (f " {z}) where z be 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 be Element of T1 : z in ( rng f) };

        then

        consider z be 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 :: T_1TOPSP:6

    

     Th6: for T,T1 be non empty TopSpace, f be continuous Function of T, T1 holds T1 is T_1 implies for w holds for x be 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 be 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 be 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 be a_partition of the carrier of T : B is closed };

      then

       A2: ( EqClass (x,fz)) in { ( EqClass (x,S)) where S be 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 be 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 :: T_1TOPSP:7

    

     Th7: for T,T1 be non empty TopSpace, f be continuous Function of T, T1 holds T1 is T_1 implies for w st w in the carrier of ( T_1-reflex T) holds ex z be 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 be 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;

    theorem :: T_1TOPSP:8

    

     Th8: for T,T1 be non empty TopSpace, f be continuous Function of T, T1 holds T1 is T_1 implies ex h be 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 be set st D1 = $1 & for z be 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 be 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 be object st y in the carrier of ( T_1-reflex T) holds ex w be 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 be 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 be 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 be Function such that

       A11: ( dom h1) = the carrier of ( T_1-reflex T) & for y be 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 be Element of T1 holds (z in ( rng f) & $1 = (f " {z})) implies $2 = z;

      

       A12: for y be object st y in fx holds ex w be object st X1[y, w]

      proof

        let y be object;

        assume y in fx;

        then

        consider w be 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 be 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 be Function such that

       A19: ( dom h2) = fx & for y be 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 be 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 be 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 be 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 be object such that

         A36: w in ( dom h2) and

         A37: y = (h2 . w) by FUNCT_1:def 3;

        consider x be 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 be 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;

      :: T_1TOPSP:def4

      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 be 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