:: The Lattice of Domains of an Extremally Disconnected Space
:: by Zbigniew Karno
::
:: Received August 27, 1992
:: Copyright (c) 1992-2012 Association of Mizar Users
begin
theorem
Th1
:
:: TDLAT_3:1
for
X
being
TopSpace
for
C
being
Subset
of
X
holds
Cl
C
=
(
Int
(
C
`
)
)
`
proof
end;
theorem
Th2
:
:: TDLAT_3:2
for
X
being
TopSpace
for
C
being
Subset
of
X
holds
Cl
(
C
`
)
=
(
Int
C
)
`
proof
end;
theorem
Th3
:
:: TDLAT_3:3
for
X
being
TopSpace
for
C
being
Subset
of
X
holds
Int
(
C
`
)
=
(
Cl
C
)
`
proof
end;
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
proof
end;
theorem
Th5
:
:: TDLAT_3:5
for
X
being
TopSpace
for
A
being
Subset
of
X
holds
( (
A
is
open
&
A
is
closed
) iff
Cl
A
=
Int
A
)
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
)
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
)
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
)
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
)
)
proof
end;
begin
:: 2. Discrete Topological Structures.
definition
let
IT
be
TopStruct
;
attr
IT
is
discrete
means
:
Def1
:
:: TDLAT_3:def 1
the
topology
of
IT
=
bool
the
carrier
of
IT
;
attr
IT
is
anti-discrete
means
:
Def2
:
:: TDLAT_3:def 2
the
topology
of
IT
=
{
{}
, the
carrier
of
IT
}
;
end;
::
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
);
::
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
}
);
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
}
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
)
proof
end;
registration
cluster
non
empty
strict
discrete
anti-discrete
for
TopStruct
;
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
)
proof
end;
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
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
proof
end;
registration
cluster
discrete
->
TopSpace-like
for
TopStruct
;
coherence
for
b
1
being
TopStruct
st
b
1
is
discrete
holds
b
1
is
TopSpace-like
proof
end;
cluster
anti-discrete
->
TopSpace-like
for
TopStruct
;
coherence
for
b
1
being
TopStruct
st
b
1
is
anti-discrete
holds
b
1
is
TopSpace-like
proof
end;
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
)
proof
end;
definition
let
IT
be
TopStruct
;
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
;
end;
::
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
);
registration
cluster
discrete
->
almost_discrete
for
TopStruct
;
coherence
for
b
1
being
TopStruct
st
b
1
is
discrete
holds
b
1
is
almost_discrete
proof
end;
cluster
anti-discrete
->
almost_discrete
for
TopStruct
;
coherence
for
b
1
being
TopStruct
st
b
1
is
anti-discrete
holds
b
1
is
almost_discrete
proof
end;
end;
registration
cluster
strict
almost_discrete
for
TopStruct
;
existence
ex
b
1
being
TopStruct
st
(
b
1
is
almost_discrete
&
b
1
is
strict
)
proof
end;
end;
begin
:: 3. Discrete Topological Spaces.
registration
cluster
non
empty
strict
TopSpace-like
discrete
anti-discrete
for
TopStruct
;
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
)
proof
end;
end;
theorem
Th15
:
:: TDLAT_3:15
for
X
being
TopSpace
holds
(
X
is
discrete
iff for
A
being
Subset
of
X
holds
A
is
open
)
proof
end;
theorem
Th16
:
:: TDLAT_3:16
for
X
being
TopSpace
holds
(
X
is
discrete
iff for
A
being
Subset
of
X
holds
A
is
closed
)
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
proof
end;
registration
let
X
be non
empty
discrete
TopSpace
;
cluster
->
closed
open
discrete
for
SubSpace
of
X
;
coherence
for
b
1
being
SubSpace
of
X
holds
(
b
1
is
open
&
b
1
is
closed
&
b
1
is
discrete
)
proof
end;
end;
registration
let
X
be non
empty
discrete
TopSpace
;
cluster
strict
TopSpace-like
closed
open
discrete
almost_discrete
for
SubSpace
of
X
;
existence
ex
b
1
being
SubSpace
of
X
st
(
b
1
is
discrete
&
b
1
is
strict
)
proof
end;
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
) )
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
) )
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
proof
end;
registration
let
X
be non
empty
anti-discrete
TopSpace
;
cluster
->
anti-discrete
for
SubSpace
of
X
;
coherence
for
b
1
being
SubSpace
of
X
holds
b
1
is
anti-discrete
proof
end;
end;
registration
let
X
be non
empty
anti-discrete
TopSpace
;
cluster
TopSpace-like
anti-discrete
almost_discrete
for
SubSpace
of
X
;
existence
ex
b
1
being
SubSpace
of
X
st
b
1
is
anti-discrete
proof
end;
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
)
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
)
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
)
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
)
proof
end;
registration
cluster
strict
TopSpace-like
almost_discrete
for
TopStruct
;
existence
ex
b
1
being
TopSpace
st
(
b
1
is
almost_discrete
&
b
1
is
strict
)
proof
end;
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
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
) ) )
proof
end;
registration
cluster
TopSpace-like
discrete
->
almost_discrete
for
TopStruct
;
coherence
for
b
1
being
TopSpace
st
b
1
is
discrete
holds
b
1
is
almost_discrete
;
cluster
TopSpace-like
anti-discrete
->
almost_discrete
for
TopStruct
;
coherence
for
b
1
being
TopSpace
st
b
1
is
anti-discrete
holds
b
1
is
almost_discrete
;
end;
registration
let
X
be non
empty
almost_discrete
TopSpace
;
cluster
non
empty
->
non
empty
almost_discrete
for
SubSpace
of
X
;
coherence
for
b
1
being non
empty
SubSpace
of
X
holds
b
1
is
almost_discrete
proof
end;
end;
registration
let
X
be non
empty
almost_discrete
TopSpace
;
cluster
open
->
closed
for
SubSpace
of
X
;
coherence
for
b
1
being
SubSpace
of
X
st
b
1
is
open
holds
b
1
is
closed
proof
end;
cluster
closed
->
open
for
SubSpace
of
X
;
coherence
for
b
1
being
SubSpace
of
X
st
b
1
is
closed
holds
b
1
is
open
proof
end;
end;
registration
let
X
be non
empty
almost_discrete
TopSpace
;
cluster
non
empty
strict
TopSpace-like
almost_discrete
for
SubSpace
of
X
;
existence
ex
b
1
being
SubSpace
of
X
st
(
b
1
is
almost_discrete
&
b
1
is
strict
& not
b
1
is
empty
)
proof
end;
end;
begin
:: 4. Extremally Disconnected Topological Spaces.
definition
let
IT
be non
empty
TopSpace
;
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
;
end;
::
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
);
registration
cluster
non
empty
strict
TopSpace-like
extremally_disconnected
for
TopStruct
;
existence
ex
b
1
being non
empty
TopSpace
st
(
b
1
is
extremally_disconnected
&
b
1
is
strict
)
proof
end;
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
)
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
)
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
)
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
)
)
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
)
)
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
) )
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
) )
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
)
)
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
)
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
) ) )
proof
end;
definition
let
IT
be non
empty
TopSpace
;
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
;
end;
::
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
);
registration
cluster
non
empty
strict
TopSpace-like
hereditarily_extremally_disconnected
for
TopStruct
;
existence
ex
b
1
being non
empty
TopSpace
st
(
b
1
is
hereditarily_extremally_disconnected
&
b
1
is
strict
)
proof
end;
end;
registration
cluster
non
empty
TopSpace-like
hereditarily_extremally_disconnected
->
non
empty
extremally_disconnected
for
TopStruct
;
coherence
for
b
1
being non
empty
TopSpace
st
b
1
is
hereditarily_extremally_disconnected
holds
b
1
is
extremally_disconnected
proof
end;
cluster
non
empty
TopSpace-like
almost_discrete
->
non
empty
hereditarily_extremally_disconnected
for
TopStruct
;
coherence
for
b
1
being non
empty
TopSpace
st
b
1
is
almost_discrete
holds
b
1
is
hereditarily_extremally_disconnected
proof
end;
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
proof
end;
registration
let
X
be non
empty
extremally_disconnected
TopSpace
;
cluster
non
empty
open
->
non
empty
extremally_disconnected
for
SubSpace
of
X
;
coherence
for
b
1
being non
empty
SubSpace
of
X
st
b
1
is
open
holds
b
1
is
extremally_disconnected
proof
end;
end;
registration
let
X
be non
empty
extremally_disconnected
TopSpace
;
cluster
non
empty
strict
TopSpace-like
extremally_disconnected
for
SubSpace
of
X
;
existence
ex
b
1
being non
empty
SubSpace
of
X
st
(
b
1
is
extremally_disconnected
&
b
1
is
strict
)
proof
end;
end;
registration
let
X
be non
empty
hereditarily_extremally_disconnected
TopSpace
;
cluster
non
empty
->
non
empty
hereditarily_extremally_disconnected
for
SubSpace
of
X
;
coherence
for
b
1
being non
empty
SubSpace
of
X
holds
b
1
is
hereditarily_extremally_disconnected
proof
end;
end;
registration
let
X
be non
empty
hereditarily_extremally_disconnected
TopSpace
;
cluster
non
empty
strict
TopSpace-like
extremally_disconnected
hereditarily_extremally_disconnected
for
SubSpace
of
X
;
existence
ex
b
1
being non
empty
SubSpace
of
X
st
(
b
1
is
hereditarily_extremally_disconnected
&
b
1
is
strict
)
proof
end;
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
proof
end;
begin
theorem
Th39
:
:: TDLAT_3:39
for
Y
being non
empty
extremally_disconnected
TopSpace
holds
Domains_of
Y
=
Closed_Domains_of
Y
proof
end;
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
)
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
Th42
:
:: TDLAT_3:42
for
Y
being non
empty
extremally_disconnected
TopSpace
holds
Domains_of
Y
=
Open_Domains_of
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
)
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
)
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
)
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
)
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
) )
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
)
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
;
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
;
theorem
:: TDLAT_3:52
for
X
being non
empty
TopSpace
holds
X
is
extremally_disconnected
proof
end;
theorem
:: TDLAT_3:53
for
X
being non
empty
TopSpace
holds
(
X
is
extremally_disconnected
iff
Domains_Lattice
X
is
B_Lattice
)
proof
end;