:: COMPLSP1 semantic presentation begin definition let n be Element of NAT ; func the_Complex_Space n -> strict TopSpace equals :: COMPLSP1:def 1 TopStruct(# (COMPLEX n),(ComplexOpenSets n) #); coherence TopStruct(# (COMPLEX n),(ComplexOpenSets n) #) is strict TopSpace proof set T = TopStruct(# (COMPLEX n),(ComplexOpenSets n) #); TopStruct(# (COMPLEX n),(ComplexOpenSets n) #) 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 TopStruct(# (COMPLEX n),(ComplexOpenSets n) #) in the topology of TopStruct(# (COMPLEX n),(ComplexOpenSets n) #) ; :: according to PRE_TOPC:def_1 ::_thesis: ( ( for b1 being Element of K10(K10( the carrier of TopStruct(# (COMPLEX n),(ComplexOpenSets n) #))) holds ( not b1 c= the topology of TopStruct(# (COMPLEX n),(ComplexOpenSets n) #) or union b1 in the topology of TopStruct(# (COMPLEX n),(ComplexOpenSets n) #) ) ) & ( for b1, b2 being Element of K10( the carrier of TopStruct(# (COMPLEX n),(ComplexOpenSets n) #)) holds ( not b1 in the topology of TopStruct(# (COMPLEX n),(ComplexOpenSets n) #) or not b2 in the topology of TopStruct(# (COMPLEX n),(ComplexOpenSets n) #) or b1 /\ b2 in the topology of TopStruct(# (COMPLEX n),(ComplexOpenSets n) #) ) ) ) thus for A being Subset-Family of TopStruct(# (COMPLEX n),(ComplexOpenSets n) #) st A c= the topology of TopStruct(# (COMPLEX n),(ComplexOpenSets n) #) holds union A in the topology of TopStruct(# (COMPLEX n),(ComplexOpenSets n) #) ::_thesis: for b1, b2 being Element of K10( the carrier of TopStruct(# (COMPLEX n),(ComplexOpenSets n) #)) holds ( not b1 in the topology of TopStruct(# (COMPLEX n),(ComplexOpenSets n) #) or not b2 in the topology of TopStruct(# (COMPLEX n),(ComplexOpenSets n) #) or b1 /\ b2 in the topology of TopStruct(# (COMPLEX n),(ComplexOpenSets n) #) ) proof let A be Subset-Family of TopStruct(# (COMPLEX n),(ComplexOpenSets n) #); ::_thesis: ( A c= the topology of TopStruct(# (COMPLEX n),(ComplexOpenSets n) #) implies union A in the topology of TopStruct(# (COMPLEX n),(ComplexOpenSets n) #) ) assume A c= the topology of TopStruct(# (COMPLEX n),(ComplexOpenSets n) #) ; ::_thesis: union A in the topology of TopStruct(# (COMPLEX n),(ComplexOpenSets n) #) then A1: for B being 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 union A in the topology of TopStruct(# (COMPLEX n),(ComplexOpenSets n) #) ; ::_thesis: verum end; let A, B be Subset of TopStruct(# (COMPLEX n),(ComplexOpenSets n) #); ::_thesis: ( not A in the topology of TopStruct(# (COMPLEX n),(ComplexOpenSets n) #) or not B in the topology of TopStruct(# (COMPLEX n),(ComplexOpenSets n) #) or A /\ B in the topology of TopStruct(# (COMPLEX n),(ComplexOpenSets n) #) ) 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 TopStruct(# (COMPLEX n),(ComplexOpenSets n) #) & B in the topology of TopStruct(# (COMPLEX n),(ComplexOpenSets n) #) ) ; ::_thesis: A /\ B in the topology of TopStruct(# (COMPLEX n),(ComplexOpenSets n) #) then ( z1 is open & z2 is open ) by SEQ_4:131; then z is open by SEQ_4:109; hence A /\ B in the topology of TopStruct(# (COMPLEX n),(ComplexOpenSets n) #) ; ::_thesis: verum end; hence TopStruct(# (COMPLEX n),(ComplexOpenSets n) #) is strict TopSpace ; ::_thesis: verum end; end; :: deftheorem defines the_Complex_Space COMPLSP1:def_1_:_ for n being Element of NAT holds the_Complex_Space n = TopStruct(# (COMPLEX n),(ComplexOpenSets n) #); registration let n be Element of NAT ; cluster the_Complex_Space n -> non empty strict ; coherence not the_Complex_Space n is empty ; end; theorem :: COMPLSP1:1 for n being Element of NAT holds the topology of (the_Complex_Space n) = ComplexOpenSets n ; theorem :: COMPLSP1:2 for n being Element of NAT holds the carrier of (the_Complex_Space n) = COMPLEX n ; theorem :: COMPLSP1:3 for n being Element of NAT for p being Point of (the_Complex_Space n) holds p is Element of COMPLEX n ; theorem Th4: :: COMPLSP1:4 for n being Element of NAT for V being Subset of (the_Complex_Space n) for A being Subset of (COMPLEX n) st A = V holds ( A is open iff V is open ) proof let n be Element of NAT ; ::_thesis: for V being Subset of (the_Complex_Space n) for A being Subset of (COMPLEX n) st A = V holds ( A is open iff V is open ) let V be Subset of (the_Complex_Space n); ::_thesis: for A being Subset of (COMPLEX n) st A = V holds ( A is open iff V is open ) let A be Subset of (COMPLEX n); ::_thesis: ( A = V implies ( A is open iff V is open ) ) assume A = V ; ::_thesis: ( A is open iff V is open ) then ( A in ComplexOpenSets n iff V in the topology of (the_Complex_Space n) ) ; hence ( A is open iff V is open ) by PRE_TOPC:def_2, SEQ_4:131; ::_thesis: verum end; theorem Th5: :: COMPLSP1:5 for n being Element of NAT for V being Subset of (the_Complex_Space n) for A being Subset of (COMPLEX n) st A = V holds ( A is closed iff V is closed ) proof let n be Element of NAT ; ::_thesis: for V being Subset of (the_Complex_Space n) for A being Subset of (COMPLEX n) st A = V holds ( A is closed iff V is closed ) let V be Subset of (the_Complex_Space n); ::_thesis: for A being Subset of (COMPLEX n) st A = V holds ( A is closed iff V is closed ) let A be Subset of (COMPLEX n); ::_thesis: ( A = V implies ( A is closed iff V is closed ) ) assume A = V ; ::_thesis: ( A is closed iff V is closed ) then ( ([#] (the_Complex_Space n)) \ V is open iff A ` is open ) by Th4; hence ( A is closed iff V is closed ) by PRE_TOPC:def_3, SEQ_4:132; ::_thesis: verum end; theorem :: COMPLSP1:6 for n being Element of NAT holds the_Complex_Space n is T_2 proof let n be Element of NAT ; ::_thesis: the_Complex_Space n is T_2 let p be Point of (the_Complex_Space n); :: according to PRE_TOPC:def_10 ::_thesis: for b1 being Element of the carrier of (the_Complex_Space n) holds ( p = b1 or ex b2, b3 being Element of K10( the carrier of (the_Complex_Space n)) st ( b2 is open & b3 is open & p in b2 & b1 in b3 & b2 misses b3 ) ) let q be Point of (the_Complex_Space n); ::_thesis: ( p = q or ex b1, b2 being Element of K10( the carrier of (the_Complex_Space n)) st ( b1 is open & b2 is open & p in b1 & q in b2 & b1 misses b2 ) ) assume A1: p <> q ; ::_thesis: ex b1, b2 being Element of K10( the carrier of (the_Complex_Space n)) st ( b1 is open & b2 is open & p in b1 & q in b2 & b1 misses b2 ) reconsider z1 = p, z2 = q as Element of COMPLEX n ; set d = |.(z1 - z2).| / 2; reconsider K1 = Ball (z1,(|.(z1 - z2).| / 2)), K2 = Ball (z2,(|.(z1 - z2).| / 2)) as Subset of (the_Complex_Space n) ; take K1 ; ::_thesis: ex b1 being Element of K10( the carrier of (the_Complex_Space n)) st ( K1 is open & b1 is open & p in K1 & q in b1 & K1 misses b1 ) take K2 ; ::_thesis: ( K1 is open & K2 is open & p in K1 & q in K2 & K1 misses K2 ) ( Ball (z1,(|.(z1 - z2).| / 2)) is open & Ball (z2,(|.(z1 - z2).| / 2)) is open ) by SEQ_4:112; hence ( K1 is open & K2 is open ) by Th4; ::_thesis: ( p in K1 & q in K2 & K1 misses K2 ) 0 < |.(z1 - z2).| by A1, SEQ_4:103; hence ( p in K1 & q in K2 ) by SEQ_4:111, XREAL_1:215; ::_thesis: K1 misses K2 assume K1 /\ K2 <> {} ; :: according to XBOOLE_0:def_7 ::_thesis: contradiction then consider x being Element of COMPLEX n such that A2: x in (Ball (z1,(|.(z1 - z2).| / 2))) /\ (Ball (z2,(|.(z1 - z2).| / 2))) by SUBSET_1:4; x in K2 by A2, XBOOLE_0:def_4; then A3: |.(z2 - x).| < |.(z1 - z2).| / 2 by SEQ_4:110; x in K1 by A2, XBOOLE_0:def_4; then |.(z1 - x).| < |.(z1 - z2).| / 2 by SEQ_4:110; then |.(z1 - x).| + |.(z2 - x).| < (|.(z1 - z2).| / 2) + (|.(z1 - z2).| / 2) by A3, XREAL_1:8; then |.(z1 - x).| + |.(x - z2).| < |.(z1 - z2).| by SEQ_4:104; hence contradiction by SEQ_4:105; ::_thesis: verum end; theorem :: COMPLSP1:7 for n being Element of NAT holds the_Complex_Space n is regular proof let n be Element of NAT ; ::_thesis: the_Complex_Space n is regular let p be Point of (the_Complex_Space n); :: according to COMPTS_1:def_2 ::_thesis: for b1 being Element of K10( the carrier of (the_Complex_Space n)) holds ( b1 = {} or not b1 is closed or not p in b1 ` or ex b2, b3 being Element of K10( the carrier of (the_Complex_Space n)) st ( b2 is open & b3 is open & p in b2 & b1 c= b3 & b2 misses b3 ) ) let P be Subset of (the_Complex_Space n); ::_thesis: ( P = {} or not P is closed or not p in P ` or ex b1, b2 being Element of K10( the carrier of (the_Complex_Space n)) st ( b1 is open & b2 is open & p in b1 & P c= b2 & b1 misses b2 ) ) assume that A1: P <> {} and A2: ( P is closed & p in P ` ) ; ::_thesis: ex b1, b2 being Element of K10( the carrier of (the_Complex_Space n)) st ( b1 is open & b2 is open & p in b1 & P c= b2 & b1 misses b2 ) 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,((dist (z1,A)) / 2)), K2 = Ball (A,((dist (z1,A)) / 2)) as Subset of (the_Complex_Space n) ; take K1 ; ::_thesis: ex b1 being Element of K10( the carrier of (the_Complex_Space n)) st ( K1 is open & b1 is open & p in K1 & P c= b1 & K1 misses b1 ) take K2 ; ::_thesis: ( K1 is open & K2 is open & p in K1 & P c= K2 & K1 misses K2 ) A3: Ball (z1,((dist (z1,A)) / 2)) is open by SEQ_4:112; Ball (A,((dist (z1,A)) / 2)) is open by A1, SEQ_4:122; hence ( K1 is open & K2 is open ) by A3, Th4; ::_thesis: ( p in K1 & P c= K2 & K1 misses K2 ) ( A is closed & not p in P ) by A2, Th5, XBOOLE_0:def_5; then 0 < (dist (z1,A)) / 2 by A1, SEQ_4:117, XREAL_1:215; hence ( p in K1 & P c= K2 ) by SEQ_4:111, SEQ_4:121; ::_thesis: K1 misses K2 assume K1 /\ K2 <> {} ; :: according to XBOOLE_0:def_7 ::_thesis: contradiction then consider x being Element of COMPLEX n such that A4: x in (Ball (z1,((dist (z1,A)) / 2))) /\ (Ball (A,((dist (z1,A)) / 2))) by SUBSET_1:4; x in K2 by A4, XBOOLE_0:def_4; then A5: dist (x,A) < (dist (z1,A)) / 2 by SEQ_4:119; x in K1 by A4, XBOOLE_0:def_4; then |.(z1 - x).| < (dist (z1,A)) / 2 by SEQ_4:110; then |.(z1 - x).| + (dist (x,A)) < ((dist (z1,A)) / 2) + ((dist (z1,A)) / 2) by A5, XREAL_1:8; hence contradiction by A1, SEQ_4:118; ::_thesis: verum end;