:: by Zbigniew Karno

::

:: Received April 6, 1993

:: Copyright (c) 1993-2021 Association of Mizar Users

theorem Th1: :: TEX_1:1

for X being non empty TopSpace

for D, B being Subset of X

for C being Subset of (X modified_with_respect_to D) st B = C & B is open holds

C is open

for D, B being Subset of X

for C being Subset of (X modified_with_respect_to D) st B = C & B is open holds

C is open

proof end;

theorem :: TEX_1:2

for X being non empty TopSpace

for D, B being Subset of X

for C being Subset of (X modified_with_respect_to D) st B = C & B is closed holds

C is closed

for D, B being Subset of X

for C being Subset of (X modified_with_respect_to D) st B = C & B is closed holds

C is closed

proof end;

theorem Th3: :: TEX_1:3

for X being non empty TopSpace

for D being Subset of X

for C being Subset of (X modified_with_respect_to (D `)) st C = D holds

C is closed

for D being Subset of X

for C being Subset of (X modified_with_respect_to (D `)) st C = D holds

C is closed

proof end;

theorem Th4: :: TEX_1:4

for X being non empty TopSpace

for D being Subset of X

for C being Subset of (X modified_with_respect_to D) st C = D & D is dense holds

( C is dense & C is open )

for D being Subset of X

for C being Subset of (X modified_with_respect_to D) st C = D & D is dense holds

( C is dense & C is open )

proof end;

theorem Th5: :: TEX_1:5

for X being non empty TopSpace

for D being Subset of X

for C being Subset of (X modified_with_respect_to D) st D c= C & D is dense holds

C is everywhere_dense

for D being Subset of X

for C being Subset of (X modified_with_respect_to D) st D c= C & D is dense holds

C is everywhere_dense

proof end;

theorem Th6: :: TEX_1:6

for X being non empty TopSpace

for D being Subset of X

for C being Subset of (X modified_with_respect_to (D `)) st C = D & D is boundary holds

( C is boundary & C is closed )

for D being Subset of X

for C being Subset of (X modified_with_respect_to (D `)) st C = D & D is boundary holds

( C is boundary & C is closed )

proof end;

theorem Th7: :: TEX_1:7

for X being non empty TopSpace

for D being Subset of X

for C being Subset of (X modified_with_respect_to (D `)) st C c= D & D is boundary holds

C is nowhere_dense

for D being Subset of X

for C being Subset of (X modified_with_respect_to (D `)) st C c= D & D is boundary holds

C is nowhere_dense

proof end;

Lm1: for X, Y being set holds

( X c= Y iff X is Subset of Y )

;

:: 2. Trivial Topological Spaces.

definition

let Y be non empty 1-sorted ;

( Y is trivial iff ex d being Element of Y st the carrier of Y = {d} )

end;
redefine attr Y is trivial means :Def1: :: TEX_1:def 1

ex d being Element of Y st the carrier of Y = {d};

compatibility ex d being Element of Y st the carrier of Y = {d};

( Y is trivial iff ex d being Element of Y st the carrier of Y = {d} )

proof end;

:: deftheorem Def1 defines trivial TEX_1:def 1 :

for Y being non empty 1-sorted holds

( Y is trivial iff ex d being Element of Y st the carrier of Y = {d} );

for Y being non empty 1-sorted holds

( Y is trivial iff ex d being Element of Y st the carrier of Y = {d} );

registration

existence

ex b_{1} being TopStruct st

( b_{1} is 1 -element & b_{1} is strict )

ex b_{1} being TopStruct st

( not b_{1} is trivial & b_{1} is strict )

end;
ex b

( b

proof end;

existence ex b

( not b

proof end;

theorem :: TEX_1:8

for Y being 1 -element TopStruct st not the topology of Y is empty & Y is almost_discrete holds

Y is TopSpace-like

Y is TopSpace-like

proof end;

registration
end;

registration

coherence

for b_{1} being 1 -element TopSpace holds

( b_{1} is anti-discrete & b_{1} is discrete )

for b_{1} being non empty TopSpace st b_{1} is discrete & b_{1} is anti-discrete holds

b_{1} is trivial

end;
for b

( b

proof end;

coherence for b

b

proof end;

registration
end;

registration

coherence

for b_{1} being non empty TopSpace st not b_{1} is discrete holds

not b_{1} is trivial
;

coherence

for b_{1} being non empty TopSpace st not b_{1} is anti-discrete holds

not b_{1} is trivial
;

end;
for b

not b

coherence

for b

not b

:: 3. Examples of Discrete and Anti-discrete Topological Spaces.

:: deftheorem defines ADTS TEX_1:def 3 :

for D being set holds ADTS D = TopStruct(# D,(cobool D) #);

for D being set holds ADTS D = TopStruct(# D,(cobool D) #);

registration

let D be set ;

coherence

( ADTS D is strict & ADTS D is anti-discrete & ADTS D is TopSpace-like )

end;
coherence

( ADTS D is strict & ADTS D is anti-discrete & ADTS D is TopSpace-like )

proof end;

registration
end;

theorem Th9: :: TEX_1:9

for X being non empty anti-discrete TopSpace

for A being Subset of X holds

( ( A is empty implies Cl A = {} ) & ( not A is empty implies Cl A = the carrier of X ) ) by PCOMPS_1:2, TDLAT_3:19;

for A being Subset of X holds

( ( A is empty implies Cl A = {} ) & ( not A is empty implies Cl A = the carrier of X ) ) by PCOMPS_1:2, TDLAT_3:19;

theorem Th10: :: TEX_1:10

for X being non empty anti-discrete TopSpace

for A being Subset of X holds

( ( A <> the carrier of X implies Int A = {} ) & ( A = the carrier of X implies Int A = the carrier of X ) )

for A being Subset of X holds

( ( A <> the carrier of X implies Int A = {} ) & ( A = the carrier of X implies Int A = the carrier of X ) )

proof end;

theorem Th11: :: TEX_1:11

for X being non empty TopSpace st ( for A being Subset of X st not A is empty holds

Cl A = the carrier of X ) holds

X is anti-discrete

Cl A = the carrier of X ) holds

X is anti-discrete

proof end;

theorem Th12: :: TEX_1:12

for X being non empty TopSpace st ( for A being Subset of X st A <> the carrier of X holds

Int A = {} ) holds

X is anti-discrete

Int A = {} ) holds

X is anti-discrete

proof end;

theorem :: TEX_1:13

for X being non empty anti-discrete TopSpace

for A being Subset of X holds

( ( A <> {} implies A is dense ) & ( A <> the carrier of X implies A is boundary ) )

for A being Subset of X holds

( ( A <> {} implies A is dense ) & ( A <> the carrier of X implies A is boundary ) )

proof end;

theorem :: TEX_1:14

for X being non empty TopSpace st ( for A being Subset of X st A <> {} holds

A is dense ) holds

X is anti-discrete

A is dense ) holds

X is anti-discrete

proof end;

theorem :: TEX_1:15

for X being non empty TopSpace st ( for A being Subset of X st A <> the carrier of X holds

A is boundary ) holds

X is anti-discrete

A is boundary ) holds

X is anti-discrete

proof end;

theorem :: TEX_1:16

for X being non empty discrete TopSpace

for A being Subset of X holds

( Cl A = A & Int A = A ) by TDLAT_3:16, TDLAT_3:15, PRE_TOPC:22, TOPS_1:23;

for A being Subset of X holds

( Cl A = A & Int A = A ) by TDLAT_3:16, TDLAT_3:15, PRE_TOPC:22, TOPS_1:23;

registration

existence

ex b_{1} being TopSpace st

( b_{1} is discrete & not b_{1} is anti-discrete & b_{1} is strict & not b_{1} is empty )

ex b_{1} being TopSpace st

( b_{1} is anti-discrete & not b_{1} is discrete & b_{1} is strict & not b_{1} is empty )

end;
ex b

( b

proof end;

existence ex b

( b

proof end;

:: 4. An Example of a Topological Space.

definition

let D be set ;

let d0 be Element of D;

TopStruct(# D,((bool D) \ { A where A is Subset of D : ( d0 in A & A <> D ) } ) #) is TopStruct ;

end;
let d0 be Element of D;

func STS (D,d0) -> TopStruct equals :: TEX_1:def 4

TopStruct(# D,((bool D) \ { A where A is Subset of D : ( d0 in A & A <> D ) } ) #);

coherence TopStruct(# D,((bool D) \ { A where A is Subset of D : ( d0 in A & A <> D ) } ) #);

TopStruct(# D,((bool D) \ { A where A is Subset of D : ( d0 in A & A <> D ) } ) #) is TopStruct ;

:: deftheorem defines STS TEX_1:def 4 :

for D being set

for d0 being Element of D holds STS (D,d0) = TopStruct(# D,((bool D) \ { A where A is Subset of D : ( d0 in A & A <> D ) } ) #);

for D being set

for d0 being Element of D holds STS (D,d0) = TopStruct(# D,((bool D) \ { A where A is Subset of D : ( d0 in A & A <> D ) } ) #);

registration

let D be set ;

let d0 be Element of D;

coherence

( STS (D,d0) is strict & STS (D,d0) is TopSpace-like )

end;
let d0 be Element of D;

coherence

( STS (D,d0) is strict & STS (D,d0) is TopSpace-like )

proof end;

registration
end;

theorem Th20: :: TEX_1:20

for D being non empty set

for d0 being Element of D

for A being Subset of (STS (D,d0)) holds

( ( {d0} c= A implies A is closed ) & ( not A is empty & A is closed implies {d0} c= A ) )

for d0 being Element of D

for A being Subset of (STS (D,d0)) holds

( ( {d0} c= A implies A is closed ) & ( not A is empty & A is closed implies {d0} c= A ) )

proof end;

theorem Th21: :: TEX_1:21

for D being non empty set

for d0 being Element of D st not D \ {d0} is empty holds

for A being Subset of (STS (D,d0)) holds

( ( A = {d0} implies ( A is closed & A is boundary ) ) & ( not A is empty & A is closed & A is boundary implies A = {d0} ) )

for d0 being Element of D st not D \ {d0} is empty holds

for A being Subset of (STS (D,d0)) holds

( ( A = {d0} implies ( A is closed & A is boundary ) ) & ( not A is empty & A is closed & A is boundary implies A = {d0} ) )

proof end;

theorem Th22: :: TEX_1:22

for D being non empty set

for d0 being Element of D

for A being Subset of (STS (D,d0)) holds

( ( A c= D \ {d0} implies A is open ) & ( A <> D & A is open implies A c= D \ {d0} ) )

for d0 being Element of D

for A being Subset of (STS (D,d0)) holds

( ( A c= D \ {d0} implies A is open ) & ( A <> D & A is open implies A c= D \ {d0} ) )

proof end;

theorem :: TEX_1:23

for D being non empty set

for d0 being Element of D st not D \ {d0} is empty holds

for A being Subset of (STS (D,d0)) holds

( ( A = D \ {d0} implies ( A is open & A is dense ) ) & ( A <> D & A is open & A is dense implies A = D \ {d0} ) )

for d0 being Element of D st not D \ {d0} is empty holds

for A being Subset of (STS (D,d0)) holds

( ( A = D \ {d0} implies ( A is open & A is dense ) ) & ( A <> D & A is open & A is dense implies A = D \ {d0} ) )

proof end;

registration

existence

ex b_{1} being TopSpace st

( not b_{1} is anti-discrete & not b_{1} is discrete & b_{1} is strict & not b_{1} is empty )

end;
ex b

( not b

proof end;

theorem Th24: :: TEX_1:24

for D being non empty set

for d0 being Element of D

for Y being non empty TopSpace holds

( TopStruct(# the carrier of Y, the topology of Y #) = TopStruct(# the carrier of (STS (D,d0)), the topology of (STS (D,d0)) #) iff ( the carrier of Y = D & ( for A being Subset of Y holds

( ( {d0} c= A implies A is closed ) & ( not A is empty & A is closed implies {d0} c= A ) ) ) ) )

for d0 being Element of D

for Y being non empty TopSpace holds

( TopStruct(# the carrier of Y, the topology of Y #) = TopStruct(# the carrier of (STS (D,d0)), the topology of (STS (D,d0)) #) iff ( the carrier of Y = D & ( for A being Subset of Y holds

( ( {d0} c= A implies A is closed ) & ( not A is empty & A is closed implies {d0} c= A ) ) ) ) )

proof end;

theorem Th25: :: TEX_1:25

for D being non empty set

for d0 being Element of D

for Y being non empty TopSpace holds

( TopStruct(# the carrier of Y, the topology of Y #) = TopStruct(# the carrier of (STS (D,d0)), the topology of (STS (D,d0)) #) iff ( the carrier of Y = D & ( for A being Subset of Y holds

( ( A c= D \ {d0} implies A is open ) & ( A <> D & A is open implies A c= D \ {d0} ) ) ) ) )

for d0 being Element of D

for Y being non empty TopSpace holds

( TopStruct(# the carrier of Y, the topology of Y #) = TopStruct(# the carrier of (STS (D,d0)), the topology of (STS (D,d0)) #) iff ( the carrier of Y = D & ( for A being Subset of Y holds

( ( A c= D \ {d0} implies A is open ) & ( A <> D & A is open implies A c= D \ {d0} ) ) ) ) )

proof end;

theorem :: TEX_1:26

for D being non empty set

for d0 being Element of D

for Y being non empty TopSpace holds

( TopStruct(# the carrier of Y, the topology of Y #) = TopStruct(# the carrier of (STS (D,d0)), the topology of (STS (D,d0)) #) iff ( the carrier of Y = D & ( for A being non empty Subset of Y holds Cl A = A \/ {d0} ) ) )

for d0 being Element of D

for Y being non empty TopSpace holds

( TopStruct(# the carrier of Y, the topology of Y #) = TopStruct(# the carrier of (STS (D,d0)), the topology of (STS (D,d0)) #) iff ( the carrier of Y = D & ( for A being non empty Subset of Y holds Cl A = A \/ {d0} ) ) )

proof end;

theorem :: TEX_1:27

for D being non empty set

for d0 being Element of D

for Y being non empty TopSpace holds

( TopStruct(# the carrier of Y, the topology of Y #) = TopStruct(# the carrier of (STS (D,d0)), the topology of (STS (D,d0)) #) iff ( the carrier of Y = D & ( for A being Subset of Y st A <> D holds

Int A = A \ {d0} ) ) )

for d0 being Element of D

for Y being non empty TopSpace holds

( TopStruct(# the carrier of Y, the topology of Y #) = TopStruct(# the carrier of (STS (D,d0)), the topology of (STS (D,d0)) #) iff ( the carrier of Y = D & ( for A being Subset of Y st A <> D holds

Int A = A \ {d0} ) ) )

proof end;

Lm2: now :: thesis: for D being non empty set

for d0 being Element of D

for G being set st G = { P where P is Subset of D : ( d0 in P & P <> D ) } & D = {d0} holds

not G <> {}

for d0 being Element of D

for G being set st G = { P where P is Subset of D : ( d0 in P & P <> D ) } & D = {d0} holds

not G <> {}

let D be non empty set ; :: thesis: for d0 being Element of D

for G being set st G = { P where P is Subset of D : ( d0 in P & P <> D ) } & D = {d0} holds

not G <> {}

let d0 be Element of D; :: thesis: for G being set st G = { P where P is Subset of D : ( d0 in P & P <> D ) } & D = {d0} holds

not G <> {}

let G be set ; :: thesis: ( G = { P where P is Subset of D : ( d0 in P & P <> D ) } & D = {d0} implies not G <> {} )

assume A1: G = { P where P is Subset of D : ( d0 in P & P <> D ) } ; :: thesis: ( D = {d0} implies not G <> {} )

set x = the Element of G;

assume A2: D = {d0} ; :: thesis: not G <> {}

assume G <> {} ; :: thesis: contradiction

then the Element of G in G ;

then consider S being Subset of D such that

the Element of G = S and

A3: d0 in S and

A4: S <> D by A1;

set d1 = the Element of D \ S;

d0 <> d1 by A3, A5, XBOOLE_0:def 5;

hence contradiction by A2, TARSKI:def 1; :: thesis: verum

end;
for G being set st G = { P where P is Subset of D : ( d0 in P & P <> D ) } & D = {d0} holds

not G <> {}

let d0 be Element of D; :: thesis: for G being set st G = { P where P is Subset of D : ( d0 in P & P <> D ) } & D = {d0} holds

not G <> {}

let G be set ; :: thesis: ( G = { P where P is Subset of D : ( d0 in P & P <> D ) } & D = {d0} implies not G <> {} )

assume A1: G = { P where P is Subset of D : ( d0 in P & P <> D ) } ; :: thesis: ( D = {d0} implies not G <> {} )

set x = the Element of G;

assume A2: D = {d0} ; :: thesis: not G <> {}

assume G <> {} ; :: thesis: contradiction

then the Element of G in G ;

then consider S being Subset of D such that

the Element of G = S and

A3: d0 in S and

A4: S <> D by A1;

set d1 = the Element of D \ S;

A5: now :: thesis: not D \ S = {}

then reconsider d1 = the Element of D \ S as Element of D by XBOOLE_0:def 5;
assume
D \ S = {}
; :: thesis: contradiction

then D c= S by XBOOLE_1:37;

hence contradiction by A4, XBOOLE_0:def 10; :: thesis: verum

end;
then D c= S by XBOOLE_1:37;

hence contradiction by A4, XBOOLE_0:def 10; :: thesis: verum

d0 <> d1 by A3, A5, XBOOLE_0:def 5;

hence contradiction by A2, TARSKI:def 1; :: thesis: verum

theorem :: TEX_1:30

for D being non empty set

for d0 being Element of D

for A being Subset of (STS (D,d0)) st A = {d0} holds

1TopSp D = (STS (D,d0)) modified_with_respect_to A

for d0 being Element of D

for A being Subset of (STS (D,d0)) st A = {d0} holds

1TopSp D = (STS (D,d0)) modified_with_respect_to A

proof end;

:: 5. Discrete and Almost Discrete Spaces.

definition

let X be non empty TopSpace;

( X is discrete iff for A being non empty Subset of X holds not A is boundary )

end;
redefine attr X is discrete means :: TEX_1:def 5

for A being non empty Subset of X holds not A is boundary ;

compatibility for A being non empty Subset of X holds not A is boundary ;

( X is discrete iff for A being non empty Subset of X holds not A is boundary )

proof end;

:: deftheorem defines discrete TEX_1:def 5 :

for X being non empty TopSpace holds

( X is discrete iff for A being non empty Subset of X holds not A is boundary );

for X being non empty TopSpace holds

( X is discrete iff for A being non empty Subset of X holds not A is boundary );

theorem :: TEX_1:31

for X being non empty TopSpace holds

( X is discrete iff for A being Subset of X st A <> the carrier of X holds

not A is dense )

( X is discrete iff for A being Subset of X st A <> the carrier of X holds

not A is dense )

proof end;

registration

for b_{1} being non empty TopSpace st not b_{1} is almost_discrete holds

( not b_{1} is discrete & not b_{1} is anti-discrete )
;

end;

cluster non empty TopSpace-like non almost_discrete -> non empty non discrete non anti-discrete for TopStruct ;

coherence for b

( not b

definition

let X be non empty TopSpace;

( X is almost_discrete iff for A being non empty Subset of X holds not A is nowhere_dense )

end;
redefine attr X is almost_discrete means :: TEX_1:def 6

for A being non empty Subset of X holds not A is nowhere_dense ;

compatibility for A being non empty Subset of X holds not A is nowhere_dense ;

( X is almost_discrete iff for A being non empty Subset of X holds not A is nowhere_dense )

proof end;

:: deftheorem defines almost_discrete TEX_1:def 6 :

for X being non empty TopSpace holds

( X is almost_discrete iff for A being non empty Subset of X holds not A is nowhere_dense );

for X being non empty TopSpace holds

( X is almost_discrete iff for A being non empty Subset of X holds not A is nowhere_dense );

theorem Th32: :: TEX_1:32

for X being non empty TopSpace holds

( X is almost_discrete iff for A being Subset of X st A <> the carrier of X holds

not A is everywhere_dense )

( X is almost_discrete iff for A being Subset of X st A <> the carrier of X holds

not A is everywhere_dense )

proof end;

theorem Th33: :: TEX_1:33

for X being non empty TopSpace holds

( not X is almost_discrete iff ex A being non empty Subset of X st

( A is boundary & A is closed ) )

( not X is almost_discrete iff ex A being non empty Subset of X st

( A is boundary & A is closed ) )

proof end;

theorem :: TEX_1:34

for X being non empty TopSpace holds

( not X is almost_discrete iff ex A being Subset of X st

( A <> the carrier of X & A is dense & A is open ) )

( not X is almost_discrete iff ex A being Subset of X st

( A <> the carrier of X & A is dense & A is open ) )

proof end;

registration

ex b_{1} being TopSpace st

( b_{1} is almost_discrete & not b_{1} is discrete & not b_{1} is anti-discrete & b_{1} is strict & not b_{1} is empty )
end;

cluster non empty strict TopSpace-like non discrete non anti-discrete almost_discrete for TopStruct ;

existence ex b

( b

proof end;

theorem Th35: :: TEX_1:35

for C being non empty set

for c0 being Element of C holds

( not C \ {c0} is empty iff not STS (C,c0) is almost_discrete )

for c0 being Element of C holds

( not C \ {c0} is empty iff not STS (C,c0) is almost_discrete )

proof end;

registration

existence

ex b_{1} being TopSpace st

( not b_{1} is almost_discrete & b_{1} is strict & not b_{1} is empty )

end;
ex b

( not b

proof end;

theorem :: TEX_1:36

for X being non empty TopSpace

for A being non empty Subset of X st A is boundary holds

not X modified_with_respect_to (A `) is almost_discrete

for A being non empty Subset of X st A is boundary holds

not X modified_with_respect_to (A `) is almost_discrete

proof end;

theorem :: TEX_1:37

for X being non empty TopSpace

for A being Subset of X st A <> the carrier of X & A is dense holds

not X modified_with_respect_to A is almost_discrete

for A being Subset of X st A <> the carrier of X & A is dense holds

not X modified_with_respect_to A is almost_discrete

proof end;