:: Baire Spaces, Sober Spaces
:: by Andrzej Trybulec
::
:: Received January 8, 1997
:: Copyright (c) 1997-2012 Association of Mizar Users
begin
theorem
Th1
:
:: YELLOW_8:1
for
X
,
A
,
B
being
set
st
A
in
Fin
X
&
B
c=
A
holds
B
in
Fin
X
proof
end;
theorem
Th2
:
:: YELLOW_8:2
for
X
being
set
for
F
being
Subset-Family
of
X
st
F
c=
Fin
X
holds
meet
F
in
Fin
X
proof
end;
begin
theorem
Th3
:
:: YELLOW_8:3
for
X
being
set
for
F
being
Subset-Family
of
X
holds
F
,
COMPLEMENT
F
are_equipotent
proof
end;
theorem
Th4
:
:: YELLOW_8:4
for
X
,
Y
being
set
st
X
,
Y
are_equipotent
&
X
is
countable
holds
Y
is
countable
proof
end;
theorem
:: YELLOW_8:5
for
X
being
1-sorted
for
F
being
Subset-Family
of
X
for
P
being
Subset
of
X
holds
(
P
`
in
COMPLEMENT
F
iff
P
in
F
)
proof
end;
theorem
Th6
:
:: YELLOW_8:6
for
X
being
1-sorted
for
F
being
Subset-Family
of
X
holds
Intersect
(
COMPLEMENT
F
)
=
(
union
F
)
`
proof
end;
theorem
Th7
:
:: YELLOW_8:7
for
X
being
1-sorted
for
F
being
Subset-Family
of
X
holds
union
(
COMPLEMENT
F
)
=
(
Intersect
F
)
`
proof
end;
begin
theorem
:: YELLOW_8:8
for
T
being non
empty
TopSpace
for
A
,
B
being
Subset
of
T
st
B
c=
A
&
A
is
closed
& ( for
C
being
Subset
of
T
st
B
c=
C
&
C
is
closed
holds
A
c=
C
) holds
A
=
Cl
B
proof
end;
theorem
Th9
:
:: YELLOW_8:9
for
T
being
TopStruct
for
B
being
Basis
of
T
for
V
being
Subset
of
T
st
V
is
open
holds
V
=
union
{
G
where
G
is
Subset
of
T
: (
G
in
B
&
G
c=
V
)
}
proof
end;
theorem
Th10
:
:: YELLOW_8:10
for
T
being
TopStruct
for
B
being
Basis
of
T
for
S
being
Subset
of
T
st
S
in
B
holds
S
is
open
proof
end;
theorem
:: YELLOW_8:11
for
T
being non
empty
TopSpace
for
B
being
Basis
of
T
for
V
being
Subset
of
T
holds
Int
V
=
union
{
G
where
G
is
Subset
of
T
: (
G
in
B
&
G
c=
V
)
}
proof
end;
begin
definition
let
T
be non
empty
TopStruct
;
let
x
be
Point
of
T
;
let
F
be
Subset-Family
of
T
;
attr
F
is
x
-quasi_basis
means
:
Def1
:
:: YELLOW_8:def 1
(
x
in
Intersect
F
& ( for
S
being
Subset
of
T
st
S
is
open
&
x
in
S
holds
ex
V
being
Subset
of
T
st
(
V
in
F
&
V
c=
S
) ) );
end;
::
deftheorem
Def1
defines
-quasi_basis
YELLOW_8:def 1 :
for
T
being non
empty
TopStruct
for
x
being
Point
of
T
for
F
being
Subset-Family
of
T
holds
(
F
is
x
-quasi_basis
iff (
x
in
Intersect
F
& ( for
S
being
Subset
of
T
st
S
is
open
&
x
in
S
holds
ex
V
being
Subset
of
T
st
(
V
in
F
&
V
c=
S
) ) ) );
registration
let
T
be non
empty
TopStruct
;
let
x
be
Point
of
T
;
cluster
open
x
-quasi_basis
for
Element
of
bool
(
bool
the
carrier
of
T
)
;
existence
ex
b
1
being
Subset-Family
of
T
st
(
b
1
is
open
&
b
1
is
x
-quasi_basis
)
proof
end;
end;
definition
let
T
be non
empty
TopStruct
;
let
x
be
Point
of
T
;
mode
Basis of
x
is
open
x
-quasi_basis
Subset-Family
of
T
;
end;
theorem
Th12
:
:: YELLOW_8:12
for
T
being non
empty
TopStruct
for
x
being
Point
of
T
for
B
being
Basis
of
x
for
V
being
Subset
of
T
st
V
in
B
holds
(
V
is
open
&
x
in
V
)
proof
end;
theorem
:: YELLOW_8:13
for
T
being non
empty
TopStruct
for
x
being
Point
of
T
for
B
being
Basis
of
x
for
V
being
Subset
of
T
st
x
in
V
&
V
is
open
holds
ex
W
being
Subset
of
T
st
(
W
in
B
&
W
c=
V
)
by
Def1
;
theorem
:: YELLOW_8:14
for
T
being non
empty
TopStruct
for
P
being
Subset-Family
of
T
st
P
c=
the
topology
of
T
& ( for
x
being
Point
of
T
ex
B
being
Basis
of
x
st
B
c=
P
) holds
P
is
Basis
of
T
proof
end;
definition
let
T
be non
empty
TopSpace
;
attr
T
is
Baire
means
:
Def2
:
:: YELLOW_8:def 2
for
F
being
Subset-Family
of
T
st
F
is
countable
& ( for
S
being
Subset
of
T
st
S
in
F
holds
S
is
everywhere_dense
) holds
ex
I
being
Subset
of
T
st
(
I
=
Intersect
F
&
I
is
dense
);
end;
::
deftheorem
Def2
defines
Baire
YELLOW_8:def 2 :
for
T
being non
empty
TopSpace
holds
(
T
is
Baire
iff for
F
being
Subset-Family
of
T
st
F
is
countable
& ( for
S
being
Subset
of
T
st
S
in
F
holds
S
is
everywhere_dense
) holds
ex
I
being
Subset
of
T
st
(
I
=
Intersect
F
&
I
is
dense
) );
theorem
:: YELLOW_8:15
for
T
being non
empty
TopSpace
holds
(
T
is
Baire
iff for
F
being
Subset-Family
of
T
st
F
is
countable
& ( for
S
being
Subset
of
T
st
S
in
F
holds
S
is
nowhere_dense
) holds
union
F
is
boundary
)
proof
end;
begin
definition
let
T
be
TopStruct
;
let
S
be
Subset
of
T
;
attr
S
is
irreducible
means
:
Def3
:
:: YELLOW_8:def 3
( not
S
is
empty
&
S
is
closed
& ( for
S1
,
S2
being
Subset
of
T
st
S1
is
closed
&
S2
is
closed
&
S
=
S1
\/
S2
& not
S1
=
S
holds
S2
=
S
) );
end;
::
deftheorem
Def3
defines
irreducible
YELLOW_8:def 3 :
for
T
being
TopStruct
for
S
being
Subset
of
T
holds
(
S
is
irreducible
iff ( not
S
is
empty
&
S
is
closed
& ( for
S1
,
S2
being
Subset
of
T
st
S1
is
closed
&
S2
is
closed
&
S
=
S1
\/
S2
& not
S1
=
S
holds
S2
=
S
) ) );
registration
let
T
be
TopStruct
;
cluster
irreducible
->
non
empty
for
Element
of
bool
the
carrier
of
T
;
coherence
for
b
1
being
Subset
of
T
st
b
1
is
irreducible
holds
not
b
1
is
empty
by
Def3
;
end;
definition
let
T
be non
empty
TopSpace
;
let
S
be
Subset
of
T
;
let
p
be
Point
of
T
;
pred
p
is_dense_point_of
S
means
:
Def4
:
:: YELLOW_8:def 4
(
p
in
S
&
S
c=
Cl
{
p
}
);
end;
::
deftheorem
Def4
defines
is_dense_point_of
YELLOW_8:def 4 :
for
T
being non
empty
TopSpace
for
S
being
Subset
of
T
for
p
being
Point
of
T
holds
(
p
is_dense_point_of
S
iff (
p
in
S
&
S
c=
Cl
{
p
}
) );
theorem
:: YELLOW_8:16
for
T
being non
empty
TopSpace
for
S
being
Subset
of
T
st
S
is
closed
holds
for
p
being
Point
of
T
st
p
is_dense_point_of
S
holds
S
=
Cl
{
p
}
proof
end;
theorem
Th17
:
:: YELLOW_8:17
for
T
being non
empty
TopSpace
for
p
being
Point
of
T
holds
Cl
{
p
}
is
irreducible
proof
end;
registration
let
T
be non
empty
TopSpace
;
cluster
irreducible
for
Element
of
bool
the
carrier
of
T
;
existence
ex
b
1
being
Subset
of
T
st
b
1
is
irreducible
proof
end;
end;
definition
let
T
be non
empty
TopSpace
;
attr
T
is
sober
means
:
Def5
:
:: YELLOW_8:def 5
for
S
being
irreducible
Subset
of
T
ex
p
being
Point
of
T
st
(
p
is_dense_point_of
S
& ( for
q
being
Point
of
T
st
q
is_dense_point_of
S
holds
p
=
q
) );
end;
::
deftheorem
Def5
defines
sober
YELLOW_8:def 5 :
for
T
being non
empty
TopSpace
holds
(
T
is
sober
iff for
S
being
irreducible
Subset
of
T
ex
p
being
Point
of
T
st
(
p
is_dense_point_of
S
& ( for
q
being
Point
of
T
st
q
is_dense_point_of
S
holds
p
=
q
) ) );
theorem
Th18
:
:: YELLOW_8:18
for
T
being non
empty
TopSpace
for
p
being
Point
of
T
holds
p
is_dense_point_of
Cl
{
p
}
proof
end;
theorem
Th19
:
:: YELLOW_8:19
for
T
being non
empty
TopSpace
for
p
being
Point
of
T
holds
p
is_dense_point_of
{
p
}
proof
end;
theorem
Th20
:
:: YELLOW_8:20
for
T
being non
empty
TopSpace
for
G
,
F
being
Subset
of
T
st
G
is
open
&
F
is
closed
holds
F
\
G
is
closed
proof
end;
theorem
Th21
:
:: YELLOW_8:21
for
T
being non
empty
Hausdorff
TopSpace
for
S
being
irreducible
Subset
of
T
holds
S
is
trivial
proof
end;
registration
let
T
be non
empty
Hausdorff
TopSpace
;
cluster
irreducible
->
trivial
for
Element
of
bool
the
carrier
of
T
;
coherence
for
b
1
being
Subset
of
T
st
b
1
is
irreducible
holds
b
1
is
trivial
by
Th21
;
end;
theorem
Th22
:
:: YELLOW_8:22
for
T
being non
empty
Hausdorff
TopSpace
holds
T
is
sober
proof
end;
registration
cluster
non
empty
TopSpace-like
Hausdorff
->
non
empty
sober
for
TopStruct
;
coherence
for
b
1
being non
empty
TopSpace
st
b
1
is
Hausdorff
holds
b
1
is
sober
by
Th22
;
end;
registration
cluster
non
empty
TopSpace-like
sober
for
TopStruct
;
existence
ex
b
1
being non
empty
TopSpace
st
b
1
is
sober
proof
end;
end;
theorem
Th23
:
:: YELLOW_8:23
for
T
being non
empty
TopSpace
holds
(
T
is
T_0
iff for
p
,
q
being
Point
of
T
st
Cl
{
p
}
=
Cl
{
q
}
holds
p
=
q
)
proof
end;
theorem
Th24
:
:: YELLOW_8:24
for
T
being non
empty
sober
TopSpace
holds
T
is
T_0
proof
end;
registration
cluster
non
empty
TopSpace-like
sober
->
non
empty
T_0
for
TopStruct
;
coherence
for
b
1
being non
empty
TopSpace
st
b
1
is
sober
holds
b
1
is
T_0
by
Th24
;
end;
definition
let
X
be
set
;
func
CofinTop
X
->
strict
TopStruct
means
:
Def6
:
:: YELLOW_8:def 6
( the
carrier
of
it
=
X
&
COMPLEMENT
the
topology
of
it
=
{
X
}
\/
(
Fin
X
)
);
existence
ex
b
1
being
strict
TopStruct
st
( the
carrier
of
b
1
=
X
&
COMPLEMENT
the
topology
of
b
1
=
{
X
}
\/
(
Fin
X
)
)
proof
end;
uniqueness
for
b
1
,
b
2
being
strict
TopStruct
st the
carrier
of
b
1
=
X
&
COMPLEMENT
the
topology
of
b
1
=
{
X
}
\/
(
Fin
X
)
& the
carrier
of
b
2
=
X
&
COMPLEMENT
the
topology
of
b
2
=
{
X
}
\/
(
Fin
X
)
holds
b
1
=
b
2
by
SETFAM_1:38
;
end;
::
deftheorem
Def6
defines
CofinTop
YELLOW_8:def 6 :
for
X
being
set
for
b
2
being
strict
TopStruct
holds
(
b
2
=
CofinTop
X
iff ( the
carrier
of
b
2
=
X
&
COMPLEMENT
the
topology
of
b
2
=
{
X
}
\/
(
Fin
X
)
) );
registration
let
X
be non
empty
set
;
cluster
CofinTop
X
->
non
empty
strict
;
coherence
not
CofinTop
X
is
empty
by
Def6
;
end;
registration
let
X
be
set
;
cluster
CofinTop
X
->
strict
TopSpace-like
;
coherence
CofinTop
X
is
TopSpace-like
proof
end;
end;
theorem
Th25
:
:: YELLOW_8:25
for
X
being non
empty
set
for
P
being
Subset
of
(
CofinTop
X
)
holds
(
P
is
closed
iff (
P
=
X
or
P
is
finite
) )
proof
end;
theorem
Th26
:
:: YELLOW_8:26
for
T
being non
empty
TopSpace
st
T
is
T_1
holds
for
p
being
Point
of
T
holds
Cl
{
p
}
=
{
p
}
proof
end;
registration
let
X
be non
empty
set
;
cluster
CofinTop
X
->
strict
T_1
;
coherence
CofinTop
X
is
T_1
proof
end;
end;
registration
let
X
be
infinite
set
;
cluster
CofinTop
X
->
strict
non
sober
;
coherence
not
CofinTop
X
is
sober
proof
end;
end;
registration
cluster
non
empty
TopSpace-like
T_1
non
sober
for
TopStruct
;
existence
ex
b
1
being non
empty
TopSpace
st
(
b
1
is
T_1
& not
b
1
is
sober
)
proof
end;
end;
begin
theorem
Th27
:
:: YELLOW_8:27
for
T
being non
empty
TopSpace
holds
(
T
is
regular
iff for
p
being
Point
of
T
for
P
being
Subset
of
T
st
p
in
Int
P
holds
ex
Q
being
Subset
of
T
st
(
Q
is
closed
&
Q
c=
P
&
p
in
Int
Q
) )
proof
end;
theorem
:: YELLOW_8:28
for
T
being non
empty
TopSpace
st
T
is
regular
holds
(
T
is
locally-compact
iff for
x
being
Point
of
T
ex
Y
being
Subset
of
T
st
(
x
in
Int
Y
&
Y
is
compact
) )
proof
end;