:: Complex Spaces
:: by Czes{\l}aw Byli\'nski and Andrzej Trybulec
::
:: Received September 27, 1990
:: Copyright (c) 1990-2018 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, REAL, SUBSET, BOOLE, 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;