COMPLSP1

:: Complex Spaces
::  by Czes{\l}aw Byli\'nski and Andrzej Trybulec
::
:: Received September 27, 1990
:: Copyright (c) 1990-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 NUMBERS, SUBSET_1, COMPLEX1, ARYTM_3, ARYTM_1, TARSKI, XBOOLE_0,
      CARD_1, RCOMP_1, SETFAM_1, METRIC_1, PRE_TOPC, STRUCT_0, CARD_5,
      COMPLSP1;
 notations TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, XXREAL_0,
      XREAL_0, SETFAM_1, REAL_1, COMPLEX1, FUNCT_1, RELSET_1, FUNCT_2,
      STRUCT_0, PRE_TOPC, FINSEQ_1, VALUED_1, RVSUM_1, FINSEQ_2, SEQ_4;
 constructors SETFAM_1, PARTFUN1, BINOP_1, SETWISEO, REAL_1, SQUARE_1, BINOP_2,
      COMPLEX1, SEQ_4, FINSEQOP, RVSUM_1, COMPTS_1, XXREAL_2, RELSET_1;
 registrations NUMBERS, XREAL_0, MEMBERED, FINSEQ_2, PRE_TOPC;
 requirements NUMERALS, SUBSET, ARITHM;
 definitions PRE_TOPC, COMPTS_1, XBOOLE_0;
 equalities SEQ_4, STRUCT_0, SUBSET_1;
 expansions PRE_TOPC;
 theorems SUBSET_1, ZFMISC_1, XBOOLE_0, XREAL_1, SEQ_4;

begin

reserve n for Element of NAT,
        x for Element of COMPLEX n;

definition let n;
  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 being 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
  the topology of the_Complex_Space n = ComplexOpenSets n;

theorem
  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
  p is Element of COMPLEX n;

theorem Th4:
  for A being Subset of COMPLEX n st A = V holds A is open iff V is open
     by SEQ_4:131;

theorem Th5:
  for A being 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
  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
  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,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;