:: YELLOW_8 semantic presentation
begin
theorem
:: YELLOW_8:1
for
X
,
A
,
B
being ( ( ) ( )
set
) st
A
: ( ( ) ( )
set
)
in
Fin
X
: ( ( ) ( )
set
) : ( (
preBoolean
) ( non
empty
cup-closed
diff-closed
preBoolean
)
set
) &
B
: ( ( ) ( )
set
)
c=
A
: ( ( ) ( )
set
) holds
B
: ( ( ) ( )
set
)
in
Fin
X
: ( ( ) ( )
set
) : ( (
preBoolean
) ( non
empty
cup-closed
diff-closed
preBoolean
)
set
) ;
theorem
:: YELLOW_8:2
for
X
being ( ( ) ( )
set
)
for
F
being ( ( ) ( )
Subset-Family
of ) st
F
: ( ( ) ( )
Subset-Family
of )
c=
Fin
X
: ( ( ) ( )
set
) : ( (
preBoolean
) ( non
empty
cup-closed
diff-closed
preBoolean
)
set
) holds
meet
F
: ( ( ) ( )
Subset-Family
of ) : ( ( ) ( )
Element
of
bool
b
1
: ( ( ) ( )
set
) : ( ( ) ( non
empty
cup-closed
diff-closed
preBoolean
)
set
) )
in
Fin
X
: ( ( ) ( )
set
) : ( (
preBoolean
) ( non
empty
cup-closed
diff-closed
preBoolean
)
set
) ;
begin
theorem
:: YELLOW_8:3
for
X
being ( ( ) ( )
set
)
for
F
being ( ( ) ( )
Subset-Family
of ) holds
F
: ( ( ) ( )
Subset-Family
of ) ,
COMPLEMENT
F
: ( ( ) ( )
Subset-Family
of ) : ( ( ) ( )
Element
of
bool
(
bool
b
1
: ( ( ) ( )
set
)
)
: ( ( ) ( non
empty
cup-closed
diff-closed
preBoolean
)
set
) : ( ( ) ( non
empty
cup-closed
diff-closed
preBoolean
)
set
) )
are_equipotent
;
theorem
:: YELLOW_8:4
for
X
,
Y
being ( ( ) ( )
set
) st
X
: ( ( ) ( )
set
) ,
Y
: ( ( ) ( )
set
)
are_equipotent
&
X
: ( ( ) ( )
set
) is
countable
holds
Y
: ( ( ) ( )
set
) is
countable
;
theorem
:: YELLOW_8:5
for
X
being ( ( ) ( )
1-sorted
)
for
F
being ( ( ) ( )
Subset-Family
of )
for
P
being ( ( ) ( )
Subset
of ) holds
(
P
: ( ( ) ( )
Subset
of )
`
: ( ( ) ( )
Element
of
bool
the
carrier
of
b
1
: ( ( ) ( )
1-sorted
) : ( ( ) ( )
set
) : ( ( ) ( non
empty
cup-closed
diff-closed
preBoolean
)
set
) )
in
COMPLEMENT
F
: ( ( ) ( )
Subset-Family
of ) : ( ( ) ( )
Element
of
bool
(
bool
the
carrier
of
b
1
: ( ( ) ( )
1-sorted
) : ( ( ) ( )
set
)
)
: ( ( ) ( non
empty
cup-closed
diff-closed
preBoolean
)
set
) : ( ( ) ( non
empty
cup-closed
diff-closed
preBoolean
)
set
) ) iff
P
: ( ( ) ( )
Subset
of )
in
F
: ( ( ) ( )
Subset-Family
of ) ) ;
theorem
:: YELLOW_8:6
for
X
being ( ( ) ( )
1-sorted
)
for
F
being ( ( ) ( )
Subset-Family
of ) holds
Intersect
(
COMPLEMENT
F
: ( ( ) ( )
Subset-Family
of )
)
: ( ( ) ( )
Element
of
bool
(
bool
the
carrier
of
b
1
: ( ( ) ( )
1-sorted
) : ( ( ) ( )
set
)
)
: ( ( ) ( non
empty
cup-closed
diff-closed
preBoolean
)
set
) : ( ( ) ( non
empty
cup-closed
diff-closed
preBoolean
)
set
) ) : ( ( ) ( )
Element
of
bool
the
carrier
of
b
1
: ( ( ) ( )
1-sorted
) : ( ( ) ( )
set
) : ( ( ) ( non
empty
cup-closed
diff-closed
preBoolean
)
set
) )
=
(
union
F
: ( ( ) ( )
Subset-Family
of )
)
: ( ( ) ( )
Element
of
bool
the
carrier
of
b
1
: ( ( ) ( )
1-sorted
) : ( ( ) ( )
set
) : ( ( ) ( non
empty
cup-closed
diff-closed
preBoolean
)
set
) )
`
: ( ( ) ( )
Element
of
bool
the
carrier
of
b
1
: ( ( ) ( )
1-sorted
) : ( ( ) ( )
set
) : ( ( ) ( non
empty
cup-closed
diff-closed
preBoolean
)
set
) ) ;
theorem
:: YELLOW_8:7
for
X
being ( ( ) ( )
1-sorted
)
for
F
being ( ( ) ( )
Subset-Family
of ) holds
union
(
COMPLEMENT
F
: ( ( ) ( )
Subset-Family
of )
)
: ( ( ) ( )
Element
of
bool
(
bool
the
carrier
of
b
1
: ( ( ) ( )
1-sorted
) : ( ( ) ( )
set
)
)
: ( ( ) ( non
empty
cup-closed
diff-closed
preBoolean
)
set
) : ( ( ) ( non
empty
cup-closed
diff-closed
preBoolean
)
set
) ) : ( ( ) ( )
Element
of
bool
the
carrier
of
b
1
: ( ( ) ( )
1-sorted
) : ( ( ) ( )
set
) : ( ( ) ( non
empty
cup-closed
diff-closed
preBoolean
)
set
) )
=
(
Intersect
F
: ( ( ) ( )
Subset-Family
of )
)
: ( ( ) ( )
Element
of
bool
the
carrier
of
b
1
: ( ( ) ( )
1-sorted
) : ( ( ) ( )
set
) : ( ( ) ( non
empty
cup-closed
diff-closed
preBoolean
)
set
) )
`
: ( ( ) ( )
Element
of
bool
the
carrier
of
b
1
: ( ( ) ( )
1-sorted
) : ( ( ) ( )
set
) : ( ( ) ( non
empty
cup-closed
diff-closed
preBoolean
)
set
) ) ;
begin
theorem
:: YELLOW_8:8
for
T
being ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
)
for
A
,
B
being ( ( ) ( )
Subset
of ) st
B
: ( ( ) ( )
Subset
of )
c=
A
: ( ( ) ( )
Subset
of ) &
A
: ( ( ) ( )
Subset
of ) is
closed
& ( for
C
being ( ( ) ( )
Subset
of ) st
B
: ( ( ) ( )
Subset
of )
c=
C
: ( ( ) ( )
Subset
of ) &
C
: ( ( ) ( )
Subset
of ) is
closed
holds
A
: ( ( ) ( )
Subset
of )
c=
C
: ( ( ) ( )
Subset
of ) ) holds
A
: ( ( ) ( )
Subset
of )
=
Cl
B
: ( ( ) ( )
Subset
of ) : ( ( ) (
closed
)
Element
of
bool
the
carrier
of
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) : ( ( ) ( non
empty
)
set
) : ( ( ) ( non
empty
cup-closed
diff-closed
preBoolean
)
set
) ) ;
theorem
:: YELLOW_8:9
for
T
being ( ( ) ( )
TopStruct
)
for
B
being ( (
quasi_basis
open
) (
quasi_basis
open
)
Basis
of
T
: ( ( ) ( )
TopStruct
) )
for
V
being ( ( ) ( )
Subset
of ) st
V
: ( ( ) ( )
Subset
of ) is
open
holds
V
: ( ( ) ( )
Subset
of )
=
union
{
G
: ( ( ) ( )
Subset
of ) where
G
is ( ( ) ( )
Subset
of ) : (
G
: ( ( ) ( )
Subset
of )
in
B
: ( (
quasi_basis
open
) (
quasi_basis
open
)
Basis
of
b
1
: ( ( ) ( )
TopStruct
) ) &
G
: ( ( ) ( )
Subset
of )
c=
V
: ( ( ) ( )
Subset
of ) )
}
: ( ( ) ( )
set
) ;
theorem
:: YELLOW_8:10
for
T
being ( ( ) ( )
TopStruct
)
for
B
being ( (
quasi_basis
open
) (
quasi_basis
open
)
Basis
of
T
: ( ( ) ( )
TopStruct
) )
for
S
being ( ( ) ( )
Subset
of ) st
S
: ( ( ) ( )
Subset
of )
in
B
: ( (
quasi_basis
open
) (
quasi_basis
open
)
Basis
of
b
1
: ( ( ) ( )
TopStruct
) ) holds
S
: ( ( ) ( )
Subset
of ) is
open
;
theorem
:: YELLOW_8:11
for
T
being ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
)
for
B
being ( (
quasi_basis
open
) (
quasi_basis
open
)
Basis
of
T
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) )
for
V
being ( ( ) ( )
Subset
of ) holds
Int
V
: ( ( ) ( )
Subset
of ) : ( ( ) (
open
)
Element
of
bool
the
carrier
of
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) : ( ( ) ( non
empty
)
set
) : ( ( ) ( non
empty
cup-closed
diff-closed
preBoolean
)
set
) )
=
union
{
G
: ( ( ) ( )
Subset
of ) where
G
is ( ( ) ( )
Subset
of ) : (
G
: ( ( ) ( )
Subset
of )
in
B
: ( (
quasi_basis
open
) (
quasi_basis
open
)
Basis
of
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) ) &
G
: ( ( ) ( )
Subset
of )
c=
V
: ( ( ) ( )
Subset
of ) )
}
: ( ( ) ( )
set
) ;
begin
definition
let
T
be ( ( non
empty
) ( non
empty
)
TopStruct
) ;
let
x
be ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) ) ;
let
F
be ( ( ) ( )
Subset-Family
of ) ;
attr
F
is
x
-quasi_basis
means
:: YELLOW_8:def 1
(
x
: ( ( ) ( )
Element
of
bool
(
bool
T
: ( ( ) ( )
TopStruct
)
)
: ( ( ) ( non
empty
cup-closed
diff-closed
preBoolean
)
set
) : ( ( ) ( non
empty
cup-closed
diff-closed
preBoolean
)
set
) )
in
Intersect
F
: ( ( ) ( )
Element
of
T
: ( ( ) ( )
TopStruct
) ) : ( ( ) ( )
Element
of
bool
the
carrier
of
T
: ( ( ) ( )
TopStruct
) : ( ( ) ( )
set
) : ( ( ) ( non
empty
cup-closed
diff-closed
preBoolean
)
set
) ) & ( for
S
being ( ( ) ( )
Subset
of ) st
S
: ( ( ) ( )
Subset
of ) is
open
&
x
: ( ( ) ( )
Element
of
bool
(
bool
T
: ( ( ) ( )
TopStruct
)
)
: ( ( ) ( non
empty
cup-closed
diff-closed
preBoolean
)
set
) : ( ( ) ( non
empty
cup-closed
diff-closed
preBoolean
)
set
) )
in
S
: ( ( ) ( )
Subset
of ) holds
ex
V
being ( ( ) ( )
Subset
of ) st
(
V
: ( ( ) ( )
Subset
of )
in
F
: ( ( ) ( )
Element
of
T
: ( ( ) ( )
TopStruct
) ) &
V
: ( ( ) ( )
Subset
of )
c=
S
: ( ( ) ( )
Subset
of ) ) ) );
end;
registration
let
T
be ( ( non
empty
) ( non
empty
)
TopStruct
) ;
let
x
be ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) ) ;
cluster
open
x
: ( ( ) ( )
Element
of the
carrier
of
T
: ( ( non
empty
) ( non
empty
)
TopStruct
) : ( ( ) ( non
empty
)
set
) )
-quasi_basis
for ( ( ) ( )
Element
of
bool
(
bool
the
carrier
of
T
: ( ( non
empty
) ( non
empty
)
TopStruct
) : ( ( ) ( non
empty
)
set
)
)
: ( ( ) ( non
empty
cup-closed
diff-closed
preBoolean
)
set
) : ( ( ) ( non
empty
cup-closed
diff-closed
preBoolean
)
set
) ) ;
end;
definition
let
T
be ( ( non
empty
) ( non
empty
)
TopStruct
) ;
let
x
be ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) ) ;
mode
Basis of
x
is
( (
open
x
: ( ( ) ( )
Element
of the
carrier
of
T
: ( ( non
empty
) ( non
empty
)
TopStruct
) : ( ( ) ( non
empty
)
set
) )
-quasi_basis
) (
open
x
: ( ( ) ( )
Element
of the
carrier
of
T
: ( ( non
empty
) ( non
empty
)
TopStruct
) : ( ( ) ( non
empty
)
set
) )
-quasi_basis
)
Subset-Family
of ) ;
end;
theorem
:: YELLOW_8:12
for
T
being ( ( non
empty
) ( non
empty
)
TopStruct
)
for
x
being ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) )
for
B
being ( (
open
b
2
: ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) )
-quasi_basis
) (
open
b
2
: ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) )
-quasi_basis
)
Basis
of
x
: ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) ) )
for
V
being ( ( ) ( )
Subset
of ) st
V
: ( ( ) ( )
Subset
of )
in
B
: ( (
open
b
2
: ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) )
-quasi_basis
) (
open
b
2
: ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) )
-quasi_basis
)
Basis
of
b
2
: ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) ) ) holds
(
V
: ( ( ) ( )
Subset
of ) is
open
&
x
: ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) )
in
V
: ( ( ) ( )
Subset
of ) ) ;
theorem
:: YELLOW_8:13
for
T
being ( ( non
empty
) ( non
empty
)
TopStruct
)
for
x
being ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) )
for
B
being ( (
open
b
2
: ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) )
-quasi_basis
) (
open
b
2
: ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) )
-quasi_basis
)
Basis
of
x
: ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) ) )
for
V
being ( ( ) ( )
Subset
of ) st
x
: ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) )
in
V
: ( ( ) ( )
Subset
of ) &
V
: ( ( ) ( )
Subset
of ) is
open
holds
ex
W
being ( ( ) ( )
Subset
of ) st
(
W
: ( ( ) ( )
Subset
of )
in
B
: ( (
open
b
2
: ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) )
-quasi_basis
) (
open
b
2
: ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) )
-quasi_basis
)
Basis
of
b
2
: ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) ) ) &
W
: ( ( ) ( )
Subset
of )
c=
V
: ( ( ) ( )
Subset
of ) ) ;
theorem
:: YELLOW_8:14
for
T
being ( ( non
empty
) ( non
empty
)
TopStruct
)
for
P
being ( ( ) ( )
Subset-Family
of ) st
P
: ( ( ) ( )
Subset-Family
of )
c=
the
topology
of
T
: ( ( non
empty
) ( non
empty
)
TopStruct
) : ( ( ) ( )
Element
of
bool
(
bool
the
carrier
of
b
1
: ( ( non
empty
) ( non
empty
)
TopStruct
) : ( ( ) ( non
empty
)
set
)
)
: ( ( ) ( non
empty
cup-closed
diff-closed
preBoolean
)
set
) : ( ( ) ( non
empty
cup-closed
diff-closed
preBoolean
)
set
) ) & ( for
x
being ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) ) ex
B
being ( (
open
b
3
: ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) )
-quasi_basis
) (
open
b
3
: ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) )
-quasi_basis
)
Basis
of
x
: ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) ) ) st
B
: ( (
open
b
3
: ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) )
-quasi_basis
) (
open
b
3
: ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) )
-quasi_basis
)
Basis
of
b
3
: ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) ) )
c=
P
: ( ( ) ( )
Subset-Family
of ) ) holds
P
: ( ( ) ( )
Subset-Family
of ) is ( (
quasi_basis
open
) (
quasi_basis
open
)
Basis
of
T
: ( ( non
empty
) ( non
empty
)
TopStruct
) ) ;
definition
let
T
be ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) ;
attr
T
is
Baire
means
:: YELLOW_8:def 2
for
F
being ( ( ) ( )
Subset-Family
of ) st
F
: ( ( ) ( )
Subset-Family
of ) is
countable
& ( for
S
being ( ( ) ( )
Subset
of ) st
S
: ( ( ) ( )
Subset
of )
in
F
: ( ( ) ( )
Subset-Family
of ) holds
S
: ( ( ) ( )
Subset
of ) is
everywhere_dense
) holds
ex
I
being ( ( ) ( )
Subset
of ) st
(
I
: ( ( ) ( )
Subset
of )
=
Intersect
F
: ( ( ) ( )
Subset-Family
of ) : ( ( ) ( )
Element
of
bool
the
carrier
of
T
: ( ( non
empty
) ( non
empty
)
TopStruct
) : ( ( ) ( non
empty
)
set
) : ( ( ) ( non
empty
cup-closed
diff-closed
preBoolean
)
set
) ) &
I
: ( ( ) ( )
Subset
of ) is
dense
);
end;
theorem
:: YELLOW_8:15
for
T
being ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) holds
(
T
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) is
Baire
iff for
F
being ( ( ) ( )
Subset-Family
of ) st
F
: ( ( ) ( )
Subset-Family
of ) is
countable
& ( for
S
being ( ( ) ( )
Subset
of ) st
S
: ( ( ) ( )
Subset
of )
in
F
: ( ( ) ( )
Subset-Family
of ) holds
S
: ( ( ) ( )
Subset
of ) is
nowhere_dense
) holds
union
F
: ( ( ) ( )
Subset-Family
of ) : ( ( ) ( )
Element
of
bool
the
carrier
of
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) : ( ( ) ( non
empty
)
set
) : ( ( ) ( non
empty
cup-closed
diff-closed
preBoolean
)
set
) ) is
boundary
) ;
begin
definition
let
T
be ( ( ) ( )
TopStruct
) ;
let
S
be ( ( ) ( )
Subset
of ) ;
attr
S
is
irreducible
means
:: YELLOW_8:def 3
( not
S
: ( ( ) ( )
Element
of the
carrier
of
T
: ( ( non
empty
) ( non
empty
)
TopStruct
) : ( ( ) ( non
empty
)
set
) ) is
empty
&
S
: ( ( ) ( )
Element
of the
carrier
of
T
: ( ( non
empty
) ( non
empty
)
TopStruct
) : ( ( ) ( non
empty
)
set
) ) is
closed
& ( for
S1
,
S2
being ( ( ) ( )
Subset
of ) st
S1
: ( ( ) ( )
Subset
of ) is
closed
&
S2
: ( ( ) ( )
Subset
of ) is
closed
&
S
: ( ( ) ( )
Element
of the
carrier
of
T
: ( ( non
empty
) ( non
empty
)
TopStruct
) : ( ( ) ( non
empty
)
set
) )
=
S1
: ( ( ) ( )
Subset
of )
\/
S2
: ( ( ) ( )
Subset
of ) : ( ( ) ( )
Element
of
bool
the
carrier
of
T
: ( ( non
empty
) ( non
empty
)
TopStruct
) : ( ( ) ( non
empty
)
set
) : ( ( ) ( non
empty
cup-closed
diff-closed
preBoolean
)
set
) ) & not
S1
: ( ( ) ( )
Subset
of )
=
S
: ( ( ) ( )
Element
of the
carrier
of
T
: ( ( non
empty
) ( non
empty
)
TopStruct
) : ( ( ) ( non
empty
)
set
) ) holds
S2
: ( ( ) ( )
Subset
of )
=
S
: ( ( ) ( )
Element
of the
carrier
of
T
: ( ( non
empty
) ( non
empty
)
TopStruct
) : ( ( ) ( non
empty
)
set
) ) ) );
end;
registration
let
T
be ( ( ) ( )
TopStruct
) ;
cluster
irreducible
->
non
empty
for ( ( ) ( )
Element
of
bool
the
carrier
of
T
: ( ( non
empty
) ( non
empty
)
TopStruct
) : ( ( ) ( non
empty
)
set
) : ( ( ) ( non
empty
cup-closed
diff-closed
preBoolean
)
set
) ) ;
end;
definition
let
T
be ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) ;
let
S
be ( ( ) ( )
Subset
of ) ;
let
p
be ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) ) ;
pred
p
is_dense_point_of
S
means
:: YELLOW_8:def 4
(
p
: ( ( ) ( )
Element
of
T
: ( ( non
empty
) ( non
empty
)
TopStruct
) )
in
S
: ( ( ) ( )
Element
of the
carrier
of
T
: ( ( non
empty
) ( non
empty
)
TopStruct
) : ( ( ) ( non
empty
)
set
) ) &
S
: ( ( ) ( )
Element
of the
carrier
of
T
: ( ( non
empty
) ( non
empty
)
TopStruct
) : ( ( ) ( non
empty
)
set
) )
c=
Cl
{
p
: ( ( ) ( )
Element
of
T
: ( ( non
empty
) ( non
empty
)
TopStruct
) )
}
: ( ( ) ( non
empty
finite
)
Element
of
bool
the
carrier
of
T
: ( ( non
empty
) ( non
empty
)
TopStruct
) : ( ( ) ( non
empty
)
set
) : ( ( ) ( non
empty
cup-closed
diff-closed
preBoolean
)
set
) ) : ( ( ) ( )
Element
of
bool
the
carrier
of
T
: ( ( non
empty
) ( non
empty
)
TopStruct
) : ( ( ) ( non
empty
)
set
) : ( ( ) ( non
empty
cup-closed
diff-closed
preBoolean
)
set
) ) );
end;
theorem
:: YELLOW_8:16
for
T
being ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
)
for
S
being ( ( ) ( )
Subset
of ) st
S
: ( ( ) ( )
Subset
of ) is
closed
holds
for
p
being ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) ) st
p
: ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) )
is_dense_point_of
S
: ( ( ) ( )
Subset
of ) holds
S
: ( ( ) ( )
Subset
of )
=
Cl
{
p
: ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) )
}
: ( ( ) ( non
empty
finite
)
Element
of
bool
the
carrier
of
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) : ( ( ) ( non
empty
)
set
) : ( ( ) ( non
empty
cup-closed
diff-closed
preBoolean
)
set
) ) : ( ( ) (
closed
)
Element
of
bool
the
carrier
of
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) : ( ( ) ( non
empty
)
set
) : ( ( ) ( non
empty
cup-closed
diff-closed
preBoolean
)
set
) ) ;
theorem
:: YELLOW_8:17
for
T
being ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
)
for
p
being ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) ) holds
Cl
{
p
: ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) )
}
: ( ( ) ( non
empty
finite
)
Element
of
bool
the
carrier
of
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) : ( ( ) ( non
empty
)
set
) : ( ( ) ( non
empty
cup-closed
diff-closed
preBoolean
)
set
) ) : ( ( ) (
closed
)
Element
of
bool
the
carrier
of
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) : ( ( ) ( non
empty
)
set
) : ( ( ) ( non
empty
cup-closed
diff-closed
preBoolean
)
set
) ) is
irreducible
;
registration
let
T
be ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) ;
cluster
irreducible
for ( ( ) ( )
Element
of
bool
the
carrier
of
T
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopStruct
) : ( ( ) ( non
empty
)
set
) : ( ( ) ( non
empty
cup-closed
diff-closed
preBoolean
)
set
) ) ;
end;
definition
let
T
be ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) ;
attr
T
is
sober
means
:: YELLOW_8:def 5
for
S
being ( (
irreducible
) ( non
empty
irreducible
)
Subset
of ) ex
p
being ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) ) st
(
p
: ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) )
is_dense_point_of
S
: ( (
irreducible
) ( non
empty
irreducible
)
Subset
of ) & ( for
q
being ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) ) st
q
: ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) )
is_dense_point_of
S
: ( (
irreducible
) ( non
empty
irreducible
)
Subset
of ) holds
p
: ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) )
=
q
: ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) ) ) );
end;
theorem
:: YELLOW_8:18
for
T
being ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
)
for
p
being ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) ) holds
p
: ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) )
is_dense_point_of
Cl
{
p
: ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) )
}
: ( ( ) ( non
empty
finite
)
Element
of
bool
the
carrier
of
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) : ( ( ) ( non
empty
)
set
) : ( ( ) ( non
empty
cup-closed
diff-closed
preBoolean
)
set
) ) : ( ( ) (
closed
)
Element
of
bool
the
carrier
of
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) : ( ( ) ( non
empty
)
set
) : ( ( ) ( non
empty
cup-closed
diff-closed
preBoolean
)
set
) ) ;
theorem
:: YELLOW_8:19
for
T
being ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
)
for
p
being ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) ) holds
p
: ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) )
is_dense_point_of
{
p
: ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) )
}
: ( ( ) ( non
empty
finite
)
Element
of
bool
the
carrier
of
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) : ( ( ) ( non
empty
)
set
) : ( ( ) ( non
empty
cup-closed
diff-closed
preBoolean
)
set
) ) ;
theorem
:: YELLOW_8:20
for
T
being ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
)
for
G
,
F
being ( ( ) ( )
Subset
of ) st
G
: ( ( ) ( )
Subset
of ) is
open
&
F
: ( ( ) ( )
Subset
of ) is
closed
holds
F
: ( ( ) ( )
Subset
of )
\
G
: ( ( ) ( )
Subset
of ) : ( ( ) ( )
Element
of
bool
the
carrier
of
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) : ( ( ) ( non
empty
)
set
) : ( ( ) ( non
empty
cup-closed
diff-closed
preBoolean
)
set
) ) is
closed
;
theorem
:: YELLOW_8:21
for
T
being ( ( non
empty
TopSpace-like
Hausdorff
) ( non
empty
TopSpace-like
T_0
T_1
Hausdorff
)
TopSpace
)
for
S
being ( (
irreducible
) ( non
empty
irreducible
)
Subset
of ) holds
S
: ( (
irreducible
) ( non
empty
irreducible
)
Subset
of ) is
trivial
;
registration
let
T
be ( ( non
empty
TopSpace-like
Hausdorff
) ( non
empty
TopSpace-like
T_0
T_1
Hausdorff
)
TopSpace
) ;
cluster
irreducible
->
trivial
for ( ( ) ( )
Element
of
bool
the
carrier
of
T
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopStruct
) : ( ( ) ( non
empty
)
set
) : ( ( ) ( non
empty
cup-closed
diff-closed
preBoolean
)
set
) ) ;
end;
theorem
:: YELLOW_8:22
for
T
being ( ( non
empty
TopSpace-like
Hausdorff
) ( non
empty
TopSpace-like
T_0
T_1
Hausdorff
)
TopSpace
) holds
T
: ( ( non
empty
TopSpace-like
Hausdorff
) ( non
empty
TopSpace-like
T_0
T_1
Hausdorff
)
TopSpace
) is
sober
;
registration
cluster
non
empty
TopSpace-like
Hausdorff
->
non
empty
TopSpace-like
sober
for ( ( ) ( )
TopStruct
) ;
end;
registration
cluster
non
empty
TopSpace-like
sober
for ( ( ) ( )
TopStruct
) ;
end;
theorem
:: YELLOW_8:23
for
T
being ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) holds
(
T
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) is
T_0
iff for
p
,
q
being ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) ) st
Cl
{
p
: ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) )
}
: ( ( ) ( non
empty
finite
)
Element
of
bool
the
carrier
of
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) : ( ( ) ( non
empty
)
set
) : ( ( ) ( non
empty
cup-closed
diff-closed
preBoolean
)
set
) ) : ( ( ) (
closed
)
Element
of
bool
the
carrier
of
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) : ( ( ) ( non
empty
)
set
) : ( ( ) ( non
empty
cup-closed
diff-closed
preBoolean
)
set
) )
=
Cl
{
q
: ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) )
}
: ( ( ) ( non
empty
finite
)
Element
of
bool
the
carrier
of
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) : ( ( ) ( non
empty
)
set
) : ( ( ) ( non
empty
cup-closed
diff-closed
preBoolean
)
set
) ) : ( ( ) (
closed
)
Element
of
bool
the
carrier
of
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) : ( ( ) ( non
empty
)
set
) : ( ( ) ( non
empty
cup-closed
diff-closed
preBoolean
)
set
) ) holds
p
: ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) )
=
q
: ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) ) ) ;
theorem
:: YELLOW_8:24
for
T
being ( ( non
empty
TopSpace-like
sober
) ( non
empty
TopSpace-like
sober
)
TopSpace
) holds
T
: ( ( non
empty
TopSpace-like
sober
) ( non
empty
TopSpace-like
sober
)
TopSpace
) is
T_0
;
registration
cluster
non
empty
TopSpace-like
sober
->
non
empty
TopSpace-like
T_0
for ( ( ) ( )
TopStruct
) ;
end;
definition
let
X
be ( ( ) ( )
set
) ;
func
CofinTop
X
->
( (
strict
) (
strict
)
TopStruct
)
means
:: YELLOW_8:def 6
( the
carrier
of
it
: ( ( ) ( )
Element
of the
carrier
of
X
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopStruct
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
set
)
=
X
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopStruct
) &
COMPLEMENT
the
topology
of
it
: ( ( ) ( )
Element
of the
carrier
of
X
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopStruct
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Element
of
bool
(
bool
the
carrier
of
it
: ( ( ) ( )
Element
of the
carrier
of
X
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopStruct
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
set
)
)
: ( ( ) ( non
empty
cup-closed
diff-closed
preBoolean
)
set
) : ( ( ) ( non
empty
cup-closed
diff-closed
preBoolean
)
set
) ) : ( ( ) ( )
Element
of
bool
(
bool
the
carrier
of
it
: ( ( ) ( )
Element
of the
carrier
of
X
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopStruct
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
set
)
)
: ( ( ) ( non
empty
cup-closed
diff-closed
preBoolean
)
set
) : ( ( ) ( non
empty
cup-closed
diff-closed
preBoolean
)
set
) )
=
{
X
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopStruct
)
}
: ( ( ) ( non
empty
finite
)
set
)
\/
(
Fin
X
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopStruct
)
)
: ( (
preBoolean
) ( non
empty
cup-closed
diff-closed
preBoolean
)
set
) : ( ( ) ( non
empty
)
set
) );
end;
registration
let
X
be ( ( non
empty
) ( non
empty
)
set
) ;
cluster
CofinTop
X
: ( ( non
empty
) ( non
empty
)
set
) : ( (
strict
) (
strict
)
TopStruct
)
->
non
empty
strict
;
end;
registration
let
X
be ( ( ) ( )
set
) ;
cluster
CofinTop
X
: ( ( ) ( )
set
) : ( (
strict
) (
strict
)
TopStruct
)
->
strict
TopSpace-like
;
end;
theorem
:: YELLOW_8:25
for
X
being ( ( non
empty
) ( non
empty
)
set
)
for
P
being ( ( ) ( )
Subset
of ) holds
(
P
: ( ( ) ( )
Subset
of ) is
closed
iff (
P
: ( ( ) ( )
Subset
of )
=
X
: ( ( non
empty
) ( non
empty
)
set
) or
P
: ( ( ) ( )
Subset
of ) is
finite
) ) ;
theorem
:: YELLOW_8:26
for
T
being ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) st
T
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) is
T_1
holds
for
p
being ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) ) holds
Cl
{
p
: ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) )
}
: ( ( ) ( non
empty
finite
)
Element
of
bool
the
carrier
of
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) : ( ( ) ( non
empty
)
set
) : ( ( ) ( non
empty
cup-closed
diff-closed
preBoolean
)
set
) ) : ( ( ) (
closed
)
Element
of
bool
the
carrier
of
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) : ( ( ) ( non
empty
)
set
) : ( ( ) ( non
empty
cup-closed
diff-closed
preBoolean
)
set
) )
=
{
p
: ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) )
}
: ( ( ) ( non
empty
finite
)
Element
of
bool
the
carrier
of
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) : ( ( ) ( non
empty
)
set
) : ( ( ) ( non
empty
cup-closed
diff-closed
preBoolean
)
set
) ) ;
registration
let
X
be ( ( non
empty
) ( non
empty
)
set
) ;
cluster
CofinTop
X
: ( ( non
empty
) ( non
empty
)
set
) : ( (
strict
) ( non
empty
strict
TopSpace-like
)
TopStruct
)
->
strict
T_1
;
end;
registration
let
X
be ( (
infinite
) ( non
empty
non
trivial
non
empty-membered
infinite
)
set
) ;
cluster
CofinTop
X
: ( (
infinite
) ( non
empty
non
trivial
non
empty-membered
infinite
)
set
) : ( (
strict
) ( non
empty
strict
TopSpace-like
T_0
T_1
)
TopStruct
)
->
strict
non
sober
;
end;
registration
cluster
non
empty
TopSpace-like
T_1
non
sober
for ( ( ) ( )
TopStruct
) ;
end;
begin
theorem
:: YELLOW_8:27
for
T
being ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) holds
(
T
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) is
regular
iff for
p
being ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) )
for
P
being ( ( ) ( )
Subset
of ) st
p
: ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) )
in
Int
P
: ( ( ) ( )
Subset
of ) : ( ( ) (
open
)
Element
of
bool
the
carrier
of
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) : ( ( ) ( non
empty
)
set
) : ( ( ) ( non
empty
cup-closed
diff-closed
preBoolean
)
set
) ) holds
ex
Q
being ( ( ) ( )
Subset
of ) st
(
Q
: ( ( ) ( )
Subset
of ) is
closed
&
Q
: ( ( ) ( )
Subset
of )
c=
P
: ( ( ) ( )
Subset
of ) &
p
: ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) )
in
Int
Q
: ( ( ) ( )
Subset
of ) : ( ( ) (
open
)
Element
of
bool
the
carrier
of
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) : ( ( ) ( non
empty
)
set
) : ( ( ) ( non
empty
cup-closed
diff-closed
preBoolean
)
set
) ) ) ) ;
theorem
:: YELLOW_8:28
for
T
being ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) st
T
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) is
regular
holds
(
T
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) is
locally-compact
iff for
x
being ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) ) ex
Y
being ( ( ) ( )
Subset
of ) st
(
x
: ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) )
in
Int
Y
: ( ( ) ( )
Subset
of ) : ( ( ) (
open
)
Element
of
bool
the
carrier
of
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) : ( ( ) ( non
empty
)
set
) : ( ( ) ( non
empty
cup-closed
diff-closed
preBoolean
)
set
) ) &
Y
: ( ( ) ( )
Subset
of ) is
compact
) ) ;