:: by Zbigniew Karno

::

:: Received August 27, 1992

:: Copyright (c) 1992-2012 Association of Mizar Users

begin

theorem :: TDLAT_3:4

for X being TopSpace

for A, B being Subset of X st A \/ B = the carrier of X & A is closed holds

A \/ (Int B) = the carrier of X

for A, B being Subset of X st A \/ B = the carrier of X & A is closed holds

A \/ (Int B) = the carrier of X

proof end;

theorem :: TDLAT_3:6

for X being TopSpace

for A being Subset of X st A is open & A is closed holds

Int (Cl A) = Cl (Int A)

for A being Subset of X st A is open & A is closed holds

Int (Cl A) = Cl (Int A)

proof end;

::Properties of Domains.

theorem Th7: :: TDLAT_3:7

for X being TopSpace

for A being Subset of X st A is condensed & Cl (Int A) c= Int (Cl A) holds

( A is open_condensed & A is closed_condensed )

for A being Subset of X st A is condensed & Cl (Int A) c= Int (Cl A) holds

( A is open_condensed & A is closed_condensed )

proof end;

theorem Th8: :: TDLAT_3:8

for X being TopSpace

for A being Subset of X st A is condensed & Cl (Int A) c= Int (Cl A) holds

( A is open & A is closed )

for A being Subset of X st A is condensed & Cl (Int A) c= Int (Cl A) holds

( A is open & A is closed )

proof end;

theorem Th9: :: TDLAT_3:9

for X being TopSpace

for A being Subset of X st A is condensed holds

( Int (Cl A) = Int A & Cl A = Cl (Int A) )

for A being Subset of X st A is condensed holds

( Int (Cl A) = Int A & Cl A = Cl (Int A) )

proof end;

begin

:: 2. Discrete Topological Structures.

definition

let IT be TopStruct ;

end;
attr IT is anti-discrete means :Def2: :: TDLAT_3:def 2

the topology of IT = {{}, the carrier of IT};

the topology of IT = {{}, the carrier of IT};

:: deftheorem Def1 defines discrete TDLAT_3:def 1 :

for IT being TopStruct holds

( IT is discrete iff the topology of IT = bool the carrier of IT );

for IT being TopStruct holds

( IT is discrete iff the topology of IT = bool the carrier of IT );

:: deftheorem Def2 defines anti-discrete TDLAT_3:def 2 :

for IT being TopStruct holds

( IT is anti-discrete iff the topology of IT = {{}, the carrier of IT} );

for IT being TopStruct holds

( IT is anti-discrete iff the topology of IT = {{}, the carrier of IT} );

theorem :: TDLAT_3:10

for Y being TopStruct st Y is discrete & Y is anti-discrete holds

bool the carrier of Y = {{}, the carrier of Y}

bool the carrier of Y = {{}, the carrier of Y}

proof end;

theorem Th11: :: TDLAT_3:11

for Y being TopStruct st {} in the topology of Y & the carrier of Y in the topology of Y & bool the carrier of Y = {{}, the carrier of Y} holds

( Y is discrete & Y is anti-discrete )

( Y is discrete & Y is anti-discrete )

proof end;

registration

existence

ex b_{1} being TopStruct st

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

end;
ex b

( b

proof end;

theorem Th12: :: TDLAT_3:12

for Y being discrete TopStruct

for A being Subset of Y holds the carrier of Y \ A in the topology of Y

for A being Subset of Y holds the carrier of Y \ A in the topology of Y

proof end;

theorem Th13: :: TDLAT_3:13

for Y being anti-discrete TopStruct

for A being Subset of Y st A in the topology of Y holds

the carrier of Y \ A in the topology of Y

for A being Subset of Y st A in the topology of Y holds

the carrier of Y \ A in the topology of Y

proof end;

registration

coherence

for b_{1} being TopStruct st b_{1} is discrete holds

b_{1} is TopSpace-like

for b_{1} being TopStruct st b_{1} is anti-discrete holds

b_{1} is TopSpace-like

end;
for b

b

proof end;

coherence for b

b

proof end;

theorem :: TDLAT_3:14

for Y being TopSpace-like TopStruct st bool the carrier of Y = {{}, the carrier of Y} holds

( Y is discrete & Y is anti-discrete )

( Y is discrete & Y is anti-discrete )

proof end;

definition

let IT be TopStruct ;

end;
attr IT is almost_discrete means :Def3: :: TDLAT_3:def 3

for A being Subset of IT st A in the topology of IT holds

the carrier of IT \ A in the topology of IT;

for A being Subset of IT st A in the topology of IT holds

the carrier of IT \ A in the topology of IT;

:: deftheorem Def3 defines almost_discrete TDLAT_3:def 3 :

for IT being TopStruct holds

( IT is almost_discrete iff for A being Subset of IT st A in the topology of IT holds

the carrier of IT \ A in the topology of IT );

for IT being TopStruct holds

( IT is almost_discrete iff for A being Subset of IT st A in the topology of IT holds

the carrier of IT \ A in the topology of IT );

registration

coherence

for b_{1} being TopStruct st b_{1} is discrete holds

b_{1} is almost_discrete

for b_{1} being TopStruct st b_{1} is anti-discrete holds

b_{1} is almost_discrete

end;
for b

b

proof end;

coherence for b

b

proof end;

registration
end;

begin

:: 3. Discrete Topological Spaces.

registration

existence

ex b_{1} being TopSpace st

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

end;
ex b

( b

proof end;

theorem Th17: :: TDLAT_3:17

for X being TopSpace st ( for A being Subset of X

for x being Point of X st A = {x} holds

A is open ) holds

X is discrete

for x being Point of X st A = {x} holds

A is open ) holds

X is discrete

proof end;

registration

let X be non empty discrete TopSpace;

coherence

for b_{1} being SubSpace of X holds

( b_{1} is open & b_{1} is closed & b_{1} is discrete )

end;
coherence

for b

( b

proof end;

registration

let X be non empty discrete TopSpace;

existence

ex b_{1} being SubSpace of X st

( b_{1} is discrete & b_{1} is strict )

end;
existence

ex b

( b

proof end;

theorem Th18: :: TDLAT_3:18

for X being TopSpace holds

( X is anti-discrete iff for A being Subset of X holds

( not A is open or A = {} or A = the carrier of X ) )

( X is anti-discrete iff for A being Subset of X holds

( not A is open or A = {} or A = the carrier of X ) )

proof end;

theorem Th19: :: TDLAT_3:19

for X being TopSpace holds

( X is anti-discrete iff for A being Subset of X holds

( not A is closed or A = {} or A = the carrier of X ) )

( X is anti-discrete iff for A being Subset of X holds

( not A is closed or A = {} or A = the carrier of X ) )

proof end;

theorem :: TDLAT_3:20

for X being TopSpace st ( for A being Subset of X

for x being Point of X st A = {x} holds

Cl A = the carrier of X ) holds

X is anti-discrete

for x being Point of X st A = {x} holds

Cl A = the carrier of X ) holds

X is anti-discrete

proof end;

registration

let X be non empty anti-discrete TopSpace;

coherence

for b_{1} being SubSpace of X holds b_{1} is anti-discrete

end;
coherence

for b

proof end;

registration

let X be non empty anti-discrete TopSpace;

existence

ex b_{1} being SubSpace of X st b_{1} is anti-discrete

end;
existence

ex b

proof end;

theorem Th21: :: TDLAT_3:21

for X being TopSpace holds

( X is almost_discrete iff for A being Subset of X st A is open holds

A is closed )

( X is almost_discrete iff for A being Subset of X st A is open holds

A is closed )

proof end;

theorem Th22: :: TDLAT_3:22

for X being TopSpace holds

( X is almost_discrete iff for A being Subset of X st A is closed holds

A is open )

( X is almost_discrete iff for A being Subset of X st A is closed holds

A is open )

proof end;

theorem :: TDLAT_3:23

for X being TopSpace holds

( X is almost_discrete iff for A being Subset of X st A is open holds

Cl A = A )

( X is almost_discrete iff for A being Subset of X st A is open holds

Cl A = A )

proof end;

theorem :: TDLAT_3:24

for X being TopSpace holds

( X is almost_discrete iff for A being Subset of X st A is closed holds

Int A = A )

( X is almost_discrete iff for A being Subset of X st A is closed holds

Int A = A )

proof end;

registration
end;

theorem :: TDLAT_3:25

for X being TopSpace st ( for A being Subset of X

for x being Point of X st A = {x} holds

Cl A is open ) holds

X is almost_discrete

for x being Point of X st A = {x} holds

Cl A is open ) holds

X is almost_discrete

proof end;

theorem :: TDLAT_3:26

for X being TopSpace holds

( X is discrete iff ( X is almost_discrete & ( for A being Subset of X

for x being Point of X st A = {x} holds

A is closed ) ) )

( X is discrete iff ( X is almost_discrete & ( for A being Subset of X

for x being Point of X st A = {x} holds

A is closed ) ) )

proof end;

registration

coherence

for b_{1} being TopSpace st b_{1} is discrete holds

b_{1} is almost_discrete
;

coherence

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

b_{1} is almost_discrete
;

end;
for b

b

coherence

for b

b

registration

let X be non empty almost_discrete TopSpace;

coherence

for b_{1} being non empty SubSpace of X holds b_{1} is almost_discrete

end;
coherence

for b

proof end;

registration

let X be non empty almost_discrete TopSpace;

coherence

for b_{1} being SubSpace of X st b_{1} is open holds

b_{1} is closed

for b_{1} being SubSpace of X st b_{1} is closed holds

b_{1} is open

end;
coherence

for b

b

proof end;

coherence for b

b

proof end;

registration

let X be non empty almost_discrete TopSpace;

existence

ex b_{1} being SubSpace of X st

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

end;
existence

ex b

( b

proof end;

begin

:: 4. Extremally Disconnected Topological Spaces.

definition

let IT be non empty TopSpace;

end;
attr IT is extremally_disconnected means :Def4: :: TDLAT_3:def 4

for A being Subset of IT st A is open holds

Cl A is open ;

for A being Subset of IT st A is open holds

Cl A is open ;

:: deftheorem Def4 defines extremally_disconnected TDLAT_3:def 4 :

for IT being non empty TopSpace holds

( IT is extremally_disconnected iff for A being Subset of IT st A is open holds

Cl A is open );

for IT being non empty TopSpace holds

( IT is extremally_disconnected iff for A being Subset of IT st A is open holds

Cl A is open );

registration

existence

ex b_{1} being non empty TopSpace st

( b_{1} is extremally_disconnected & b_{1} is strict )

end;
ex b

( b

proof end;

theorem Th27: :: TDLAT_3:27

for X being non empty TopSpace holds

( X is extremally_disconnected iff for A being Subset of X st A is closed holds

Int A is closed )

( X is extremally_disconnected iff for A being Subset of X st A is closed holds

Int A is closed )

proof end;

theorem Th28: :: TDLAT_3:28

for X being non empty TopSpace holds

( X is extremally_disconnected iff for A, B being Subset of X st A is open & B is open & A misses B holds

Cl A misses Cl B )

( X is extremally_disconnected iff for A, B being Subset of X st A is open & B is open & A misses B holds

Cl A misses Cl B )

proof end;

theorem :: TDLAT_3:29

for X being non empty TopSpace holds

( X is extremally_disconnected iff for A, B being Subset of X st A is closed & B is closed & A \/ B = the carrier of X holds

(Int A) \/ (Int B) = the carrier of X )

( X is extremally_disconnected iff for A, B being Subset of X st A is closed & B is closed & A \/ B = the carrier of X holds

(Int A) \/ (Int B) = the carrier of X )

proof end;

theorem Th30: :: TDLAT_3:30

for X being non empty TopSpace holds

( X is extremally_disconnected iff for A being Subset of X st A is open holds

Cl A = Int (Cl A) )

( X is extremally_disconnected iff for A being Subset of X st A is open holds

Cl A = Int (Cl A) )

proof end;

theorem :: TDLAT_3:31

for X being non empty TopSpace holds

( X is extremally_disconnected iff for A being Subset of X st A is closed holds

Int A = Cl (Int A) )

( X is extremally_disconnected iff for A being Subset of X st A is closed holds

Int A = Cl (Int A) )

proof end;

theorem Th32: :: TDLAT_3:32

for X being non empty TopSpace holds

( X is extremally_disconnected iff for A being Subset of X st A is condensed holds

( A is closed & A is open ) )

( X is extremally_disconnected iff for A being Subset of X st A is condensed holds

( A is closed & A is open ) )

proof end;

theorem Th33: :: TDLAT_3:33

for X being non empty TopSpace holds

( X is extremally_disconnected iff for A being Subset of X st A is condensed holds

( A is closed_condensed & A is open_condensed ) )

( X is extremally_disconnected iff for A being Subset of X st A is condensed holds

( A is closed_condensed & A is open_condensed ) )

proof end;

theorem Th34: :: TDLAT_3:34

for X being non empty TopSpace holds

( X is extremally_disconnected iff for A being Subset of X st A is condensed holds

Int (Cl A) = Cl (Int A) )

( X is extremally_disconnected iff for A being Subset of X st A is condensed holds

Int (Cl A) = Cl (Int A) )

proof end;

theorem :: TDLAT_3:35

for X being non empty TopSpace holds

( X is extremally_disconnected iff for A being Subset of X st A is condensed holds

Int A = Cl A )

( X is extremally_disconnected iff for A being Subset of X st A is condensed holds

Int A = Cl A )

proof end;

theorem Th36: :: TDLAT_3:36

for X being non empty TopSpace holds

( X is extremally_disconnected iff for A being Subset of X holds

( ( A is open_condensed implies A is closed_condensed ) & ( A is closed_condensed implies A is open_condensed ) ) )

( X is extremally_disconnected iff for A being Subset of X holds

( ( A is open_condensed implies A is closed_condensed ) & ( A is closed_condensed implies A is open_condensed ) ) )

proof end;

definition

let IT be non empty TopSpace;

end;
attr IT is hereditarily_extremally_disconnected means :Def5: :: TDLAT_3:def 5

for X0 being non empty SubSpace of IT holds X0 is extremally_disconnected ;

for X0 being non empty SubSpace of IT holds X0 is extremally_disconnected ;

:: deftheorem Def5 defines hereditarily_extremally_disconnected TDLAT_3:def 5 :

for IT being non empty TopSpace holds

( IT is hereditarily_extremally_disconnected iff for X0 being non empty SubSpace of IT holds X0 is extremally_disconnected );

for IT being non empty TopSpace holds

( IT is hereditarily_extremally_disconnected iff for X0 being non empty SubSpace of IT holds X0 is extremally_disconnected );

registration

existence

ex b_{1} being non empty TopSpace st

( b_{1} is hereditarily_extremally_disconnected & b_{1} is strict )

end;
ex b

( b

proof end;

registration

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

b_{1} is extremally_disconnected

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

b_{1} is hereditarily_extremally_disconnected
end;

cluster non empty TopSpace-like hereditarily_extremally_disconnected -> non empty extremally_disconnected for TopStruct ;

coherence for b

b

proof end;

cluster non empty TopSpace-like almost_discrete -> non empty hereditarily_extremally_disconnected for TopStruct ;

coherence for b

b

proof end;

theorem Th37: :: TDLAT_3:37

for X being non empty extremally_disconnected TopSpace

for X0 being non empty SubSpace of X

for A being Subset of X st A = the carrier of X0 & A is dense holds

X0 is extremally_disconnected

for X0 being non empty SubSpace of X

for A being Subset of X st A = the carrier of X0 & A is dense holds

X0 is extremally_disconnected

proof end;

registration

let X be non empty extremally_disconnected TopSpace;

coherence

for b_{1} being non empty SubSpace of X st b_{1} is open holds

b_{1} is extremally_disconnected

end;
coherence

for b

b

proof end;

registration

let X be non empty extremally_disconnected TopSpace;

existence

ex b_{1} being non empty SubSpace of X st

( b_{1} is extremally_disconnected & b_{1} is strict )

end;
existence

ex b

( b

proof end;

registration

let X be non empty hereditarily_extremally_disconnected TopSpace;

coherence

for b_{1} being non empty SubSpace of X holds b_{1} is hereditarily_extremally_disconnected

end;
coherence

for b

proof end;

registration

let X be non empty hereditarily_extremally_disconnected TopSpace;

ex b_{1} being non empty SubSpace of X st

( b_{1} is hereditarily_extremally_disconnected & b_{1} is strict )

end;
cluster non empty strict TopSpace-like extremally_disconnected hereditarily_extremally_disconnected for SubSpace of X;

existence ex b

( b

proof end;

theorem :: TDLAT_3:38

for X being non empty TopSpace st ( for X0 being non empty closed SubSpace of X holds X0 is extremally_disconnected ) holds

X is hereditarily_extremally_disconnected

X is hereditarily_extremally_disconnected

proof end;

begin

theorem Th40: :: TDLAT_3:40

for Y being non empty extremally_disconnected TopSpace holds

( D-Union Y = CLD-Union Y & D-Meet Y = CLD-Meet Y )

( D-Union Y = CLD-Union Y & D-Meet Y = CLD-Meet Y )

proof end;

theorem Th41: :: TDLAT_3:41

for Y being non empty extremally_disconnected TopSpace holds Domains_Lattice Y = Closed_Domains_Lattice Y

proof end;

theorem Th43: :: TDLAT_3:43

for Y being non empty extremally_disconnected TopSpace holds

( D-Union Y = OPD-Union Y & D-Meet Y = OPD-Meet Y )

( D-Union Y = OPD-Union Y & D-Meet Y = OPD-Meet Y )

proof end;

theorem Th44: :: TDLAT_3:44

for Y being non empty extremally_disconnected TopSpace holds Domains_Lattice Y = Open_Domains_Lattice Y

proof end;

theorem Th45: :: TDLAT_3:45

for Y being non empty extremally_disconnected TopSpace

for A, B being Element of Domains_of Y holds

( (D-Union Y) . (A,B) = A \/ B & (D-Meet Y) . (A,B) = A /\ B )

for A, B being Element of Domains_of Y holds

( (D-Union Y) . (A,B) = A \/ B & (D-Meet Y) . (A,B) = A /\ B )

proof end;

theorem :: TDLAT_3:46

for Y being non empty extremally_disconnected TopSpace

for a, b being Element of (Domains_Lattice Y)

for A, B being Element of Domains_of Y st a = A & b = B holds

( a "\/" b = A \/ B & a "/\" b = A /\ B )

for a, b being Element of (Domains_Lattice Y)

for A, B being Element of Domains_of Y st a = A & b = B holds

( a "\/" b = A \/ B & a "/\" b = A /\ B )

proof end;

theorem :: TDLAT_3:47

for Y being non empty extremally_disconnected TopSpace

for F being Subset-Family of Y st F is domains-family holds

for S being Subset of (Domains_Lattice Y) st S = F holds

"\/" (S,(Domains_Lattice Y)) = Cl (union F)

for F being Subset-Family of Y st F is domains-family holds

for S being Subset of (Domains_Lattice Y) st S = F holds

"\/" (S,(Domains_Lattice Y)) = Cl (union F)

proof end;

theorem :: TDLAT_3:48

for Y being non empty extremally_disconnected TopSpace

for F being Subset-Family of Y st F is domains-family holds

for S being Subset of (Domains_Lattice Y) st S = F holds

( ( S <> {} implies "/\" (S,(Domains_Lattice Y)) = Int (meet F) ) & ( S = {} implies "/\" (S,(Domains_Lattice Y)) = [#] Y ) )

for F being Subset-Family of Y st F is domains-family holds

for S being Subset of (Domains_Lattice Y) st S = F holds

( ( S <> {} implies "/\" (S,(Domains_Lattice Y)) = Int (meet F) ) & ( S = {} implies "/\" (S,(Domains_Lattice Y)) = [#] Y ) )

proof end;

theorem Th49: :: TDLAT_3:49

for X being non empty TopSpace holds

( X is extremally_disconnected iff Domains_Lattice X is M_Lattice )

( X is extremally_disconnected iff Domains_Lattice X is M_Lattice )

proof end;

theorem :: TDLAT_3:50

for X being non empty TopSpace st Domains_Lattice X = Closed_Domains_Lattice X holds

X is extremally_disconnected by Th49;

X is extremally_disconnected by Th49;

theorem :: TDLAT_3:51

for X being non empty TopSpace st Domains_Lattice X = Open_Domains_Lattice X holds

X is extremally_disconnected by Th49;

X is extremally_disconnected by Th49;

theorem :: TDLAT_3:53

for X being non empty TopSpace holds

( X is extremally_disconnected iff Domains_Lattice X is B_Lattice )

( X is extremally_disconnected iff Domains_Lattice X is B_Lattice )

proof end;