complsp1.miz

    begin

    reserve n for Element of NAT ,

x for Element of ( COMPLEX n);

    definition

      let n;

      :: COMPLSP1:def1

      func the_Complex_Space n -> strict TopSpace equals TopStruct (# ( COMPLEX n), ( ComplexOpenSets n) #);

      coherence

      proof

        set T = TopStruct (# ( COMPLEX n), ( ComplexOpenSets n) #);

        T is TopSpace-like

        proof

          reconsider z = ( COMPLEX n) as Subset of ( COMPLEX n) by ZFMISC_1:def 1;

          z is open by SEQ_4: 107;

          hence the carrier of T in the topology of T;

          thus for A be Subset-Family of T st A c= the topology of T holds ( union A) in the topology of T

          proof

            let A be Subset-Family of T;

            assume A c= the topology of T;

            then

             A1: for B be Subset of ( COMPLEX n) st B in A holds B is open by SEQ_4: 131;

            reconsider z = ( union A) as Subset of ( COMPLEX n);

            z is open by A1, SEQ_4: 108;

            hence thesis;

          end;

          let A,B be Subset of T;

          reconsider z1 = A, z2 = B as Subset of ( COMPLEX n);

          reconsider z = (A /\ B) as Subset of ( COMPLEX n);

          assume A in the topology of T & B in the topology of T;

          then z1 is open & z2 is open by SEQ_4: 131;

          then z is open by SEQ_4: 109;

          hence thesis;

        end;

        hence thesis;

      end;

    end

    registration

      let n;

      cluster ( the_Complex_Space n) -> non empty;

      coherence ;

    end

    theorem :: COMPLSP1:1

    the topology of ( the_Complex_Space n) = ( ComplexOpenSets n);

    theorem :: COMPLSP1:2

    the carrier of ( the_Complex_Space n) = ( COMPLEX n);

    reserve p,q for Point of ( the_Complex_Space n),

V for Subset of ( the_Complex_Space n);

    theorem :: COMPLSP1:3

    p is Element of ( COMPLEX n);

    theorem :: COMPLSP1:4



     Th4: for A be Subset of ( COMPLEX n) st A = V holds A is open iff V is open by SEQ_4: 131;

    theorem :: COMPLSP1:5



     Th5: for A be Subset of ( COMPLEX n) st A = V holds A is closed iff V is closed

    proof

      let A be Subset of ( COMPLEX n);

      assume A = V;

      then (( [#] ( the_Complex_Space n)) \ V) is open iff (A ` ) is open by Th4;

      hence thesis by SEQ_4: 132;

    end;

    theorem :: COMPLSP1:6

    ( the_Complex_Space n) is T_2

    proof

      let p, q;

      assume

       A1: p <> q;

      reconsider z1 = p, z2 = q as Element of ( COMPLEX n);

      set d = ( |.(z1 - z2).| / 2);

      reconsider K1 = ( Ball (z1,d)), K2 = ( Ball (z2,d)) as Subset of ( the_Complex_Space n);

      take K1, K2;

      ( Ball (z1,d)) is open & ( Ball (z2,d)) is open by SEQ_4: 112;

      hence K1 is open & K2 is open;

       0 < |.(z1 - z2).| by A1, SEQ_4: 103;

      hence p in K1 & q in K2 by SEQ_4: 111, XREAL_1: 215;

      assume (K1 /\ K2) <> {} ;

      then

      consider x such that

       A2: x in (( Ball (z1,d)) /\ ( Ball (z2,d))) by SUBSET_1: 4;

      x in K2 by A2, XBOOLE_0:def 4;

      then

       A3: |.(z2 - x).| < d by SEQ_4: 110;

      x in K1 by A2, XBOOLE_0:def 4;

      then |.(z1 - x).| < d by SEQ_4: 110;

      then ( |.(z1 - x).| + |.(z2 - x).|) < (d + d) by A3, XREAL_1: 8;

      then ( |.(z1 - x).| + |.(x - z2).|) < |.(z1 - z2).| by SEQ_4: 104;

      hence contradiction by SEQ_4: 105;

    end;

    theorem :: COMPLSP1:7

    ( the_Complex_Space n) is regular

    proof

      let p;

      let P be Subset of ( the_Complex_Space n) such that

       A1: P <> {} and

       A2: P is closed & p in (P ` );

      reconsider A = P as Subset of ( COMPLEX n);

      reconsider z1 = p as Element of ( COMPLEX n);

      set d = (( dist (z1,A)) / 2);

      reconsider K1 = ( Ball (z1,d)), K2 = ( Ball (A,d)) as Subset of ( the_Complex_Space n);

      take K1, K2;



       A3: ( Ball (z1,d)) is open by SEQ_4: 112;

      ( Ball (A,d)) is open by A1, SEQ_4: 122;

      hence K1 is open & K2 is open by A3;

      A is closed & not p in P by A2, Th5, XBOOLE_0:def 5;

      then 0 < d by A1, SEQ_4: 117, XREAL_1: 215;

      hence p in K1 & P c= K2 by SEQ_4: 111, SEQ_4: 121;

      assume (K1 /\ K2) <> {} ;

      then

      consider x such that

       A4: x in (( Ball (z1,d)) /\ ( Ball (A,d))) by SUBSET_1: 4;

      x in K2 by A4, XBOOLE_0:def 4;

      then

       A5: ( dist (x,A)) < d by SEQ_4: 119;

      x in K1 by A4, XBOOLE_0:def 4;

      then |.(z1 - x).| < d by SEQ_4: 110;

      then ( |.(z1 - x).| + ( dist (x,A))) < (d + d) by A5, XREAL_1: 8;

      hence contradiction by A1, SEQ_4: 118;

    end;