:: TOPGEN_1 semantic presentation
begin
theorem
:: TOPGEN_1:1
for
T
being ( ( ) ( )
1-sorted
)
for
A
,
B
being ( ( ) ( )
Subset
of ) holds
(
A
: ( ( ) ( )
Subset
of )
meets
B
: ( ( ) ( )
Subset
of )
`
: ( ( ) ( )
Element
of
K10
( the
carrier
of
b
1
: ( ( ) ( )
1-sorted
) : ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) iff
A
: ( ( ) ( )
Subset
of )
\
B
: ( ( ) ( )
Subset
of ) : ( ( ) ( )
Element
of
K10
( the
carrier
of
b
1
: ( ( ) ( )
1-sorted
) : ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) )
<>
{}
: ( ( ) ( )
set
) ) ;
theorem
:: TOPGEN_1:2
for
T
being ( ( ) ( )
1-sorted
) holds
(
T
: ( ( ) ( )
1-sorted
) is
countable
iff
card
(
[#]
T
: ( ( ) ( )
1-sorted
)
)
: ( ( ) ( non
proper
)
Element
of
K10
( the
carrier
of
b
1
: ( ( ) ( )
1-sorted
) : ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) : ( (
cardinal
) (
ordinal
cardinal
)
set
)
c=
omega
: ( ( ) (
ordinal
non
finite
cardinal
limit_cardinal
)
set
) ) ;
registration
let
T
be ( (
finite
) (
finite
)
1-sorted
) ;
cluster
[#]
T
: ( (
finite
) (
finite
)
1-sorted
) : ( ( ) ( non
proper
)
Element
of
K10
( the
carrier
of
T
: ( (
finite
) (
finite
)
1-sorted
) : ( ( ) (
finite
)
set
) ) : ( ( ) ( non
empty
)
set
) )
->
finite
;
end;
registration
cluster
finite
->
countable
for ( ( ) ( )
1-sorted
) ;
end;
registration
cluster
non
empty
countable
for ( ( ) ( )
1-sorted
) ;
cluster
non
empty
TopSpace-like
countable
for ( ( ) ( )
TopStruct
) ;
end;
registration
let
T
be ( (
countable
) (
countable
)
1-sorted
) ;
cluster
[#]
T
: ( (
countable
) (
countable
)
1-sorted
) : ( ( ) ( non
proper
)
Element
of
K10
( the
carrier
of
T
: ( (
countable
) (
countable
)
1-sorted
) : ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) )
->
countable
;
end;
registration
cluster
non
empty
TopSpace-like
T_1
for ( ( ) ( )
TopStruct
) ;
end;
begin
theorem
:: TOPGEN_1:3
for
T
being ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
)
for
A
being ( ( ) ( )
Subset
of ) holds
Int
A
: ( ( ) ( )
Subset
of ) : ( ( ) (
open
)
Element
of
K10
( the
carrier
of
b
1
: ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) : ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) )
=
(
Cl
(
A
: ( ( ) ( )
Subset
of )
`
)
: ( ( ) ( )
Element
of
K10
( the
carrier
of
b
1
: ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) : ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) )
)
: ( ( ) (
closed
)
Element
of
K10
( the
carrier
of
b
1
: ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) : ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) )
`
: ( ( ) (
open
)
Element
of
K10
( the
carrier
of
b
1
: ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) : ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) ;
definition
let
T
be ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) ;
let
F
be ( ( ) ( )
Subset-Family
of ) ;
func
Fr
F
->
( ( ) ( )
Subset-Family
of )
means
:: TOPGEN_1:def 1
for
A
being ( ( ) ( )
Subset
of ) holds
(
A
: ( ( ) ( )
Subset
of )
in
it
: ( ( ) ( )
Element
of
T
: ( ( non
empty
V105
()
V106
()
V107
()
V108
() ) ( non
empty
V105
()
V106
()
V107
()
V108
() )
L7
()) ) iff ex
B
being ( ( ) ( )
Subset
of ) st
(
A
: ( ( ) ( )
Subset
of )
=
Fr
B
: ( ( ) ( )
Subset
of ) : ( ( ) ( )
Element
of
K10
( the
carrier
of
T
: ( ( non
empty
V105
()
V106
()
V107
()
V108
() ) ( non
empty
V105
()
V106
()
V107
()
V108
() )
L7
()) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( non
empty
)
set
) ) &
B
: ( ( ) ( )
Subset
of )
in
F
: ( ( ) ( )
Element
of
K10
(
K10
(
T
: ( ( non
empty
V105
()
V106
()
V107
()
V108
() ) ( non
empty
V105
()
V106
()
V107
()
V108
() )
L7
()) ) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( non
empty
)
set
) ) ) );
end;
theorem
:: TOPGEN_1:4
for
T
being ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
)
for
F
being ( ( ) ( )
Subset-Family
of ) st
F
: ( ( ) ( )
Subset-Family
of )
=
{}
: ( ( ) ( )
set
) holds
Fr
F
: ( ( ) ( )
Subset-Family
of ) : ( ( ) ( )
Subset-Family
of )
=
{}
: ( ( ) ( )
set
) ;
theorem
:: TOPGEN_1:5
for
T
being ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
)
for
F
being ( ( ) ( )
Subset-Family
of )
for
A
being ( ( ) ( )
Subset
of ) st
F
: ( ( ) ( )
Subset-Family
of )
=
{
A
: ( ( ) ( )
Subset
of )
}
: ( ( ) ( non
empty
V2
() 1 : ( ( ) ( non
empty
)
set
)
-element
)
Element
of
K10
(
K10
( the
carrier
of
b
1
: ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) : ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( non
empty
)
set
) ) holds
Fr
F
: ( ( ) ( )
Subset-Family
of ) : ( ( ) ( )
Subset-Family
of )
=
{
(
Fr
A
: ( ( ) ( )
Subset
of )
)
: ( ( ) (
closed
)
Element
of
K10
( the
carrier
of
b
1
: ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) : ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) )
}
: ( ( ) ( non
empty
V2
() 1 : ( ( ) ( non
empty
)
set
)
-element
)
Element
of
K10
(
K10
( the
carrier
of
b
1
: ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) : ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( non
empty
)
set
) ) ;
theorem
:: TOPGEN_1:6
for
T
being ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
)
for
F
,
G
being ( ( ) ( )
Subset-Family
of ) st
F
: ( ( ) ( )
Subset-Family
of )
c=
G
: ( ( ) ( )
Subset-Family
of ) holds
Fr
F
: ( ( ) ( )
Subset-Family
of ) : ( ( ) ( )
Subset-Family
of )
c=
Fr
G
: ( ( ) ( )
Subset-Family
of ) : ( ( ) ( )
Subset-Family
of ) ;
theorem
:: TOPGEN_1:7
for
T
being ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
)
for
F
,
G
being ( ( ) ( )
Subset-Family
of ) holds
Fr
(
F
: ( ( ) ( )
Subset-Family
of )
\/
G
: ( ( ) ( )
Subset-Family
of )
)
: ( ( ) ( )
Element
of
K10
(
K10
( the
carrier
of
b
1
: ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) : ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Subset-Family
of )
=
(
Fr
F
: ( ( ) ( )
Subset-Family
of )
)
: ( ( ) ( )
Subset-Family
of )
\/
(
Fr
G
: ( ( ) ( )
Subset-Family
of )
)
: ( ( ) ( )
Subset-Family
of ) : ( ( ) ( )
Element
of
K10
(
K10
( the
carrier
of
b
1
: ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) : ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( non
empty
)
set
) ) ;
theorem
:: TOPGEN_1:8
for
T
being ( ( ) ( )
TopStruct
)
for
A
being ( ( ) ( )
Subset
of ) holds
Fr
A
: ( ( ) ( )
Subset
of ) : ( ( ) ( )
Element
of
K10
( the
carrier
of
b
1
: ( ( ) ( )
TopStruct
) : ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) )
=
(
Cl
A
: ( ( ) ( )
Subset
of )
)
: ( ( ) ( )
Element
of
K10
( the
carrier
of
b
1
: ( ( ) ( )
TopStruct
) : ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) )
\
(
Int
A
: ( ( ) ( )
Subset
of )
)
: ( ( ) ( )
Element
of
K10
( the
carrier
of
b
1
: ( ( ) ( )
TopStruct
) : ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Element
of
K10
( the
carrier
of
b
1
: ( ( ) ( )
TopStruct
) : ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) ;
theorem
:: TOPGEN_1:9
for
T
being ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
)
for
A
being ( ( ) ( )
Subset
of )
for
p
being ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) ) holds
(
p
: ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) )
in
Fr
A
: ( ( ) ( )
Subset
of ) : ( ( ) (
closed
)
Element
of
K10
( the
carrier
of
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( non
empty
)
set
) ) iff for
U
being ( ( ) ( )
Subset
of ) st
U
: ( ( ) ( )
Subset
of ) is
open
&
p
: ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) )
in
U
: ( ( ) ( )
Subset
of ) holds
(
A
: ( ( ) ( )
Subset
of )
meets
U
: ( ( ) ( )
Subset
of ) &
U
: ( ( ) ( )
Subset
of )
\
A
: ( ( ) ( )
Subset
of ) : ( ( ) ( )
Element
of
K10
( the
carrier
of
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( non
empty
)
set
) )
<>
{}
: ( ( ) ( )
set
) ) ) ;
theorem
:: TOPGEN_1:10
for
T
being ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
)
for
A
being ( ( ) ( )
Subset
of )
for
p
being ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) ) holds
(
p
: ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) )
in
Fr
A
: ( ( ) ( )
Subset
of ) : ( ( ) (
closed
)
Element
of
K10
( the
carrier
of
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( non
empty
)
set
) ) iff for
B
being ( (
V115
(
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) ,
b
3
: ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) ) )
V129
(
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) ) ) (
V115
(
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) ,
b
3
: ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) ) )
V129
(
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) ) )
Basis
of )
for
U
being ( ( ) ( )
Subset
of ) st
U
: ( ( ) ( )
Subset
of )
in
B
: ( (
V115
(
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) ,
b
3
: ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) ) )
V129
(
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) ) ) (
V115
(
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) ,
b
3
: ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) ) )
V129
(
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) ) )
Basis
of ) holds
(
A
: ( ( ) ( )
Subset
of )
meets
U
: ( ( ) ( )
Subset
of ) &
U
: ( ( ) ( )
Subset
of )
\
A
: ( ( ) ( )
Subset
of ) : ( ( ) ( )
Element
of
K10
( the
carrier
of
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( non
empty
)
set
) )
<>
{}
: ( ( ) ( )
set
) ) ) ;
theorem
:: TOPGEN_1:11
for
T
being ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
)
for
A
being ( ( ) ( )
Subset
of )
for
p
being ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) ) holds
(
p
: ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) )
in
Fr
A
: ( ( ) ( )
Subset
of ) : ( ( ) (
closed
)
Element
of
K10
( the
carrier
of
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( non
empty
)
set
) ) iff ex
B
being ( (
V115
(
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) ,
b
3
: ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) ) )
V129
(
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) ) ) (
V115
(
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) ,
b
3
: ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) ) )
V129
(
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) ) )
Basis
of ) st
for
U
being ( ( ) ( )
Subset
of ) st
U
: ( ( ) ( )
Subset
of )
in
B
: ( (
V115
(
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) ,
b
3
: ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) ) )
V129
(
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) ) ) (
V115
(
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) ,
b
3
: ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) ) )
V129
(
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) ) )
Basis
of ) holds
(
A
: ( ( ) ( )
Subset
of )
meets
U
: ( ( ) ( )
Subset
of ) &
U
: ( ( ) ( )
Subset
of )
\
A
: ( ( ) ( )
Subset
of ) : ( ( ) ( )
Element
of
K10
( the
carrier
of
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( non
empty
)
set
) )
<>
{}
: ( ( ) ( )
set
) ) ) ;
theorem
:: TOPGEN_1:12
for
T
being ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
)
for
A
,
B
being ( ( ) ( )
Subset
of ) holds
Fr
(
A
: ( ( ) ( )
Subset
of )
/\
B
: ( ( ) ( )
Subset
of )
)
: ( ( ) ( )
Element
of
K10
( the
carrier
of
b
1
: ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) : ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) : ( ( ) (
closed
)
Element
of
K10
( the
carrier
of
b
1
: ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) : ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) )
c=
(
(
Cl
A
: ( ( ) ( )
Subset
of )
)
: ( ( ) (
closed
)
Element
of
K10
( the
carrier
of
b
1
: ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) : ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) )
/\
(
Fr
B
: ( ( ) ( )
Subset
of )
)
: ( ( ) (
closed
)
Element
of
K10
( the
carrier
of
b
1
: ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) : ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) )
)
: ( ( ) ( )
Element
of
K10
( the
carrier
of
b
1
: ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) : ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) )
\/
(
(
Fr
A
: ( ( ) ( )
Subset
of )
)
: ( ( ) (
closed
)
Element
of
K10
( the
carrier
of
b
1
: ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) : ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) )
/\
(
Cl
B
: ( ( ) ( )
Subset
of )
)
: ( ( ) (
closed
)
Element
of
K10
( the
carrier
of
b
1
: ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) : ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) )
)
: ( ( ) ( )
Element
of
K10
( the
carrier
of
b
1
: ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) : ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Element
of
K10
( the
carrier
of
b
1
: ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) : ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) ;
theorem
:: TOPGEN_1:13
for
T
being ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
)
for
A
being ( ( ) ( )
Subset
of ) holds the
carrier
of
T
: ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) : ( ( ) ( )
set
)
=
(
(
Int
A
: ( ( ) ( )
Subset
of )
)
: ( ( ) (
open
)
Element
of
K10
( the
carrier
of
b
1
: ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) : ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) )
\/
(
Fr
A
: ( ( ) ( )
Subset
of )
)
: ( ( ) (
closed
)
Element
of
K10
( the
carrier
of
b
1
: ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) : ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) )
)
: ( ( ) ( )
Element
of
K10
( the
carrier
of
b
1
: ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) : ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) )
\/
(
Int
(
A
: ( ( ) ( )
Subset
of )
`
)
: ( ( ) ( )
Element
of
K10
( the
carrier
of
b
1
: ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) : ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) )
)
: ( ( ) (
open
)
Element
of
K10
( the
carrier
of
b
1
: ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) : ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Element
of
K10
( the
carrier
of
b
1
: ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) : ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) ;
theorem
:: TOPGEN_1:14
for
T
being ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
)
for
A
being ( ( ) ( )
Subset
of ) holds
( (
A
: ( ( ) ( )
Subset
of ) is
open
&
A
: ( ( ) ( )
Subset
of ) is
closed
) iff
Fr
A
: ( ( ) ( )
Subset
of ) : ( ( ) (
closed
)
Element
of
K10
( the
carrier
of
b
1
: ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) : ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) )
=
{}
: ( ( ) ( )
set
) ) ;
begin
definition
let
T
be ( ( ) ( )
TopStruct
) ;
let
A
be ( ( ) ( )
Subset
of ) ;
let
x
be ( ( ) ( )
set
) ;
pred
x
is_an_accumulation_point_of
A
means
:: TOPGEN_1:def 2
x
: ( ( ) ( )
Element
of
T
: ( ( non
empty
V105
()
V106
()
V107
()
V108
() ) ( non
empty
V105
()
V106
()
V107
()
V108
() )
L7
()) )
in
Cl
(
A
: ( ( ) ( )
Element
of
K10
(
K10
(
T
: ( ( non
empty
V105
()
V106
()
V107
()
V108
() ) ( non
empty
V105
()
V106
()
V107
()
V108
() )
L7
()) ) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( non
empty
)
set
) )
\
{
x
: ( ( ) ( )
Element
of
T
: ( ( non
empty
V105
()
V106
()
V107
()
V108
() ) ( non
empty
V105
()
V106
()
V107
()
V108
() )
L7
()) )
}
: ( ( ) ( non
empty
V2
() 1 : ( ( ) ( non
empty
)
set
)
-element
)
set
)
)
: ( ( ) ( )
Element
of
K10
( the
carrier
of
T
: ( ( non
empty
V105
()
V106
()
V107
()
V108
() ) ( non
empty
V105
()
V106
()
V107
()
V108
() )
L7
()) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Element
of
K10
( the
carrier
of
T
: ( ( non
empty
V105
()
V106
()
V107
()
V108
() ) ( non
empty
V105
()
V106
()
V107
()
V108
() )
L7
()) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( non
empty
)
set
) ) ;
end;
theorem
:: TOPGEN_1:15
for
T
being ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
)
for
A
being ( ( ) ( )
Subset
of )
for
x
being ( ( ) ( )
set
) st
x
: ( ( ) ( )
set
)
is_an_accumulation_point_of
A
: ( ( ) ( )
Subset
of ) holds
x
: ( ( ) ( )
set
) is ( ( ) ( )
Point
of ( ( ) ( )
set
) ) ;
definition
let
T
be ( ( ) ( )
TopStruct
) ;
let
A
be ( ( ) ( )
Subset
of ) ;
func
Der
A
->
( ( ) ( )
Subset
of )
means
:: TOPGEN_1:def 3
for
x
being ( ( ) ( )
set
) st
x
: ( ( ) ( )
set
)
in
the
carrier
of
T
: ( ( non
empty
V105
()
V106
()
V107
()
V108
() ) ( non
empty
V105
()
V106
()
V107
()
V108
() )
L7
()) : ( ( ) ( non
empty
)
set
) holds
(
x
: ( ( ) ( )
set
)
in
it
: ( ( ) ( )
Element
of
T
: ( ( non
empty
V105
()
V106
()
V107
()
V108
() ) ( non
empty
V105
()
V106
()
V107
()
V108
() )
L7
()) ) iff
x
: ( ( ) ( )
set
)
is_an_accumulation_point_of
A
: ( ( ) ( )
Element
of
K10
(
K10
(
T
: ( ( non
empty
V105
()
V106
()
V107
()
V108
() ) ( non
empty
V105
()
V106
()
V107
()
V108
() )
L7
()) ) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( non
empty
)
set
) ) );
end;
theorem
:: TOPGEN_1:16
for
T
being ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
)
for
A
being ( ( ) ( )
Subset
of )
for
x
being ( ( ) ( )
set
) holds
(
x
: ( ( ) ( )
set
)
in
Der
A
: ( ( ) ( )
Subset
of ) : ( ( ) ( )
Subset
of ) iff
x
: ( ( ) ( )
set
)
is_an_accumulation_point_of
A
: ( ( ) ( )
Subset
of ) ) ;
theorem
:: TOPGEN_1:17
for
T
being ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
)
for
A
being ( ( ) ( )
Subset
of )
for
x
being ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) ) holds
(
x
: ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) )
in
Der
A
: ( ( ) ( )
Subset
of ) : ( ( ) ( )
Subset
of ) iff for
U
being ( (
open
) (
open
)
Subset
of ) st
x
: ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) )
in
U
: ( (
open
) (
open
)
Subset
of ) holds
ex
y
being ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) ) st
(
y
: ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) )
in
A
: ( ( ) ( )
Subset
of )
/\
U
: ( (
open
) (
open
)
Subset
of ) : ( ( ) ( )
Element
of
K10
( the
carrier
of
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( non
empty
)
set
) ) &
x
: ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) )
<>
y
: ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) ) ) ) ;
theorem
:: TOPGEN_1:18
for
T
being ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
)
for
A
being ( ( ) ( )
Subset
of )
for
x
being ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) ) holds
(
x
: ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) )
in
Der
A
: ( ( ) ( )
Subset
of ) : ( ( ) ( )
Subset
of ) iff for
B
being ( (
V115
(
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) ,
b
3
: ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) ) )
V129
(
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) ) ) (
V115
(
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) ,
b
3
: ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) ) )
V129
(
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) ) )
Basis
of )
for
U
being ( ( ) ( )
Subset
of ) st
U
: ( ( ) ( )
Subset
of )
in
B
: ( (
V115
(
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) ,
b
3
: ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) ) )
V129
(
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) ) ) (
V115
(
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) ,
b
3
: ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) ) )
V129
(
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) ) )
Basis
of ) holds
ex
y
being ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) ) st
(
y
: ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) )
in
A
: ( ( ) ( )
Subset
of )
/\
U
: ( ( ) ( )
Subset
of ) : ( ( ) ( )
Element
of
K10
( the
carrier
of
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( non
empty
)
set
) ) &
x
: ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) )
<>
y
: ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) ) ) ) ;
theorem
:: TOPGEN_1:19
for
T
being ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
)
for
A
being ( ( ) ( )
Subset
of )
for
x
being ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) ) holds
(
x
: ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) )
in
Der
A
: ( ( ) ( )
Subset
of ) : ( ( ) ( )
Subset
of ) iff ex
B
being ( (
V115
(
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) ,
b
3
: ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) ) )
V129
(
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) ) ) (
V115
(
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) ,
b
3
: ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) ) )
V129
(
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) ) )
Basis
of ) st
for
U
being ( ( ) ( )
Subset
of ) st
U
: ( ( ) ( )
Subset
of )
in
B
: ( (
V115
(
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) ,
b
3
: ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) ) )
V129
(
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) ) ) (
V115
(
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) ,
b
3
: ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) ) )
V129
(
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) ) )
Basis
of ) holds
ex
y
being ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) ) st
(
y
: ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) )
in
A
: ( ( ) ( )
Subset
of )
/\
U
: ( ( ) ( )
Subset
of ) : ( ( ) ( )
Element
of
K10
( the
carrier
of
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( non
empty
)
set
) ) &
x
: ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) )
<>
y
: ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) ) ) ) ;
begin
definition
let
T
be ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) ;
let
A
be ( ( ) ( )
Subset
of ) ;
let
x
be ( ( ) ( )
set
) ;
pred
x
is_isolated_in
A
means
:: TOPGEN_1:def 4
(
x
: ( ( ) ( )
Element
of
T
: ( ( non
empty
V105
()
V106
()
V107
()
V108
() ) ( non
empty
V105
()
V106
()
V107
()
V108
() )
L7
()) )
in
A
: ( ( ) ( )
Element
of
K10
(
K10
(
T
: ( ( non
empty
V105
()
V106
()
V107
()
V108
() ) ( non
empty
V105
()
V106
()
V107
()
V108
() )
L7
()) ) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( non
empty
)
set
) ) & not
x
: ( ( ) ( )
Element
of
T
: ( ( non
empty
V105
()
V106
()
V107
()
V108
() ) ( non
empty
V105
()
V106
()
V107
()
V108
() )
L7
()) )
is_an_accumulation_point_of
A
: ( ( ) ( )
Element
of
K10
(
K10
(
T
: ( ( non
empty
V105
()
V106
()
V107
()
V108
() ) ( non
empty
V105
()
V106
()
V107
()
V108
() )
L7
()) ) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( non
empty
)
set
) ) );
end;
theorem
:: TOPGEN_1:20
for
T
being ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
)
for
A
being ( ( ) ( )
Subset
of )
for
p
being ( ( ) ( )
set
) holds
(
p
: ( ( ) ( )
set
)
in
A
: ( ( ) ( )
Subset
of )
\
(
Der
A
: ( ( ) ( )
Subset
of )
)
: ( ( ) ( )
Subset
of ) : ( ( ) ( )
Element
of
K10
( the
carrier
of
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( non
empty
)
set
) ) iff
p
: ( ( ) ( )
set
)
is_isolated_in
A
: ( ( ) ( )
Subset
of ) ) ;
theorem
:: TOPGEN_1:21
for
T
being ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
)
for
A
being ( ( ) ( )
Subset
of )
for
p
being ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) ) holds
(
p
: ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) )
is_an_accumulation_point_of
A
: ( ( ) ( )
Subset
of ) iff for
U
being ( (
open
) (
open
)
Subset
of ) st
p
: ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) )
in
U
: ( (
open
) (
open
)
Subset
of ) holds
ex
q
being ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) ) st
(
q
: ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) )
<>
p
: ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) ) &
q
: ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) )
in
A
: ( ( ) ( )
Subset
of ) &
q
: ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) )
in
U
: ( (
open
) (
open
)
Subset
of ) ) ) ;
theorem
:: TOPGEN_1:22
for
T
being ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
)
for
A
being ( ( ) ( )
Subset
of )
for
p
being ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) ) holds
(
p
: ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) )
is_isolated_in
A
: ( ( ) ( )
Subset
of ) iff ex
G
being ( (
open
) (
open
)
Subset
of ) st
G
: ( (
open
) (
open
)
Subset
of )
/\
A
: ( ( ) ( )
Subset
of ) : ( ( ) ( )
Element
of
K10
( the
carrier
of
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( non
empty
)
set
) )
=
{
p
: ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) )
}
: ( ( ) ( non
empty
V2
() 1 : ( ( ) ( non
empty
)
set
)
-element
)
set
) ) ;
definition
let
T
be ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) ;
let
p
be ( ( ) ( )
Point
of ( ( ) ( )
set
) ) ;
attr
p
is
isolated
means
:: TOPGEN_1:def 5
p
: ( ( ) ( )
Element
of
K10
(
K10
(
T
: ( ( non
empty
V105
()
V106
()
V107
()
V108
() ) ( non
empty
V105
()
V106
()
V107
()
V108
() )
L7
()) ) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( non
empty
)
set
) )
is_isolated_in
[#]
T
: ( ( non
empty
V105
()
V106
()
V107
()
V108
() ) ( non
empty
V105
()
V106
()
V107
()
V108
() )
L7
()) : ( ( ) ( non
empty
non
proper
)
Element
of
K10
( the
carrier
of
T
: ( ( non
empty
V105
()
V106
()
V107
()
V108
() ) ( non
empty
V105
()
V106
()
V107
()
V108
() )
L7
()) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( non
empty
)
set
) ) ;
end;
theorem
:: TOPGEN_1:23
errorfrm ;
begin
definition
let
T
be ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) ;
let
F
be ( ( ) ( )
Subset-Family
of ) ;
func
Der
F
->
( ( ) ( )
Subset-Family
of )
means
:: TOPGEN_1:def 6
for
A
being ( ( ) ( )
Subset
of ) holds
(
A
: ( ( ) ( )
Subset
of )
in
it
: ( ( ) ( )
Element
of
T
: ( ( non
empty
V105
()
V106
()
V107
()
V108
() ) ( non
empty
V105
()
V106
()
V107
()
V108
() )
L7
()) ) iff ex
B
being ( ( ) ( )
Subset
of ) st
(
A
: ( ( ) ( )
Subset
of )
=
Der
B
: ( ( ) ( )
Subset
of ) : ( ( ) ( )
Subset
of ) &
B
: ( ( ) ( )
Subset
of )
in
F
: ( ( ) ( )
Element
of
K10
(
K10
(
T
: ( ( non
empty
V105
()
V106
()
V107
()
V108
() ) ( non
empty
V105
()
V106
()
V107
()
V108
() )
L7
()) ) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( non
empty
)
set
) ) ) );
end;
theorem
:: TOPGEN_1:24
for
T
being ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
)
for
F
being ( ( ) ( )
Subset-Family
of ) st
F
: ( ( ) ( )
Subset-Family
of )
=
{}
: ( ( ) ( )
set
) holds
Der
F
: ( ( ) ( )
Subset-Family
of ) : ( ( ) ( )
Subset-Family
of )
=
{}
: ( ( ) ( )
set
) ;
theorem
:: TOPGEN_1:25
for
T
being ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
)
for
A
being ( ( ) ( )
Subset
of )
for
F
being ( ( ) ( )
Subset-Family
of ) st
F
: ( ( ) ( )
Subset-Family
of )
=
{
A
: ( ( ) ( )
Subset
of )
}
: ( ( ) ( non
empty
V2
() 1 : ( ( ) ( non
empty
)
set
)
-element
)
Element
of
K10
(
K10
( the
carrier
of
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( non
empty
)
set
) ) holds
Der
F
: ( ( ) ( )
Subset-Family
of ) : ( ( ) ( )
Subset-Family
of )
=
{
(
Der
A
: ( ( ) ( )
Subset
of )
)
: ( ( ) ( )
Subset
of )
}
: ( ( ) ( non
empty
V2
() 1 : ( ( ) ( non
empty
)
set
)
-element
)
Element
of
K10
(
K10
( the
carrier
of
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( non
empty
)
set
) ) ;
theorem
:: TOPGEN_1:26
for
T
being ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
)
for
F
,
G
being ( ( ) ( )
Subset-Family
of ) st
F
: ( ( ) ( )
Subset-Family
of )
c=
G
: ( ( ) ( )
Subset-Family
of ) holds
Der
F
: ( ( ) ( )
Subset-Family
of ) : ( ( ) ( )
Subset-Family
of )
c=
Der
G
: ( ( ) ( )
Subset-Family
of ) : ( ( ) ( )
Subset-Family
of ) ;
theorem
:: TOPGEN_1:27
for
T
being ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
)
for
F
,
G
being ( ( ) ( )
Subset-Family
of ) holds
Der
(
F
: ( ( ) ( )
Subset-Family
of )
\/
G
: ( ( ) ( )
Subset-Family
of )
)
: ( ( ) ( )
Element
of
K10
(
K10
( the
carrier
of
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Subset-Family
of )
=
(
Der
F
: ( ( ) ( )
Subset-Family
of )
)
: ( ( ) ( )
Subset-Family
of )
\/
(
Der
G
: ( ( ) ( )
Subset-Family
of )
)
: ( ( ) ( )
Subset-Family
of ) : ( ( ) ( )
Element
of
K10
(
K10
( the
carrier
of
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( non
empty
)
set
) ) ;
theorem
:: TOPGEN_1:28
for
T
being ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
)
for
A
being ( ( ) ( )
Subset
of ) holds
Der
A
: ( ( ) ( )
Subset
of ) : ( ( ) ( )
Subset
of )
c=
Cl
A
: ( ( ) ( )
Subset
of ) : ( ( ) (
closed
)
Element
of
K10
( the
carrier
of
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( non
empty
)
set
) ) ;
theorem
:: TOPGEN_1:29
for
T
being ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
)
for
A
being ( ( ) ( )
Subset
of ) holds
Cl
A
: ( ( ) ( )
Subset
of ) : ( ( ) (
closed
)
Element
of
K10
( the
carrier
of
b
1
: ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) : ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) )
=
A
: ( ( ) ( )
Subset
of )
\/
(
Der
A
: ( ( ) ( )
Subset
of )
)
: ( ( ) ( )
Subset
of ) : ( ( ) ( )
Element
of
K10
( the
carrier
of
b
1
: ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) : ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) ;
theorem
:: TOPGEN_1:30
for
T
being ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
)
for
A
,
B
being ( ( ) ( )
Subset
of ) st
A
: ( ( ) ( )
Subset
of )
c=
B
: ( ( ) ( )
Subset
of ) holds
Der
A
: ( ( ) ( )
Subset
of ) : ( ( ) ( )
Subset
of )
c=
Der
B
: ( ( ) ( )
Subset
of ) : ( ( ) ( )
Subset
of ) ;
theorem
:: TOPGEN_1:31
for
T
being ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
)
for
A
,
B
being ( ( ) ( )
Subset
of ) holds
Der
(
A
: ( ( ) ( )
Subset
of )
\/
B
: ( ( ) ( )
Subset
of )
)
: ( ( ) ( )
Element
of
K10
( the
carrier
of
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Subset
of )
=
(
Der
A
: ( ( ) ( )
Subset
of )
)
: ( ( ) ( )
Subset
of )
\/
(
Der
B
: ( ( ) ( )
Subset
of )
)
: ( ( ) ( )
Subset
of ) : ( ( ) ( )
Element
of
K10
( the
carrier
of
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( non
empty
)
set
) ) ;
theorem
:: TOPGEN_1:32
for
T
being ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
)
for
A
being ( ( ) ( )
Subset
of ) st
T
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) is
T_1
holds
Der
(
Der
A
: ( ( ) ( )
Subset
of )
)
: ( ( ) ( )
Subset
of ) : ( ( ) ( )
Subset
of )
c=
Der
A
: ( ( ) ( )
Subset
of ) : ( ( ) ( )
Subset
of ) ;
theorem
:: TOPGEN_1:33
for
T
being ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
)
for
A
being ( ( ) ( )
Subset
of ) st
T
: ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) is
T_1
holds
Cl
(
Der
A
: ( ( ) ( )
Subset
of )
)
: ( ( ) ( )
Subset
of ) : ( ( ) (
closed
)
Element
of
K10
( the
carrier
of
b
1
: ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) : ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) )
=
Der
A
: ( ( ) ( )
Subset
of ) : ( ( ) ( )
Subset
of ) ;
registration
let
T
be ( ( non
empty
TopSpace-like
T_1
) ( non
empty
TopSpace-like
T_1
)
TopSpace
) ;
let
A
be ( ( ) ( )
Subset
of ) ;
cluster
Der
A
: ( ( ) ( )
Element
of
K10
( the
carrier
of
T
: ( ( non
empty
TopSpace-like
T_1
) ( non
empty
TopSpace-like
T_1
)
TopStruct
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Subset
of )
->
closed
;
end;
theorem
:: TOPGEN_1:34
for
T
being ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
)
for
F
being ( ( ) ( )
Subset-Family
of ) holds
union
(
Der
F
: ( ( ) ( )
Subset-Family
of )
)
: ( ( ) ( )
Subset-Family
of ) : ( ( ) ( )
Element
of
K10
( the
carrier
of
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( non
empty
)
set
) )
c=
Der
(
union
F
: ( ( ) ( )
Subset-Family
of )
)
: ( ( ) ( )
Element
of
K10
( the
carrier
of
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Subset
of ) ;
theorem
:: TOPGEN_1:35
for
T
being ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
)
for
A
,
B
being ( ( ) ( )
Subset
of )
for
x
being ( ( ) ( )
set
) st
A
: ( ( ) ( )
Subset
of )
c=
B
: ( ( ) ( )
Subset
of ) &
x
: ( ( ) ( )
set
)
is_an_accumulation_point_of
A
: ( ( ) ( )
Subset
of ) holds
x
: ( ( ) ( )
set
)
is_an_accumulation_point_of
B
: ( ( ) ( )
Subset
of ) ;
begin
definition
let
T
be ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) ;
let
A
be ( ( ) ( )
Subset
of ) ;
attr
A
is
dense-in-itself
means
:: TOPGEN_1:def 7
A
: ( ( ) ( )
Element
of
K10
( the
carrier
of
T
: ( ( non
empty
V105
()
V106
()
V107
()
V108
() ) ( non
empty
V105
()
V106
()
V107
()
V108
() )
L7
()) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( non
empty
)
set
) )
c=
Der
A
: ( ( ) ( )
Element
of
K10
( the
carrier
of
T
: ( ( non
empty
V105
()
V106
()
V107
()
V108
() ) ( non
empty
V105
()
V106
()
V107
()
V108
() )
L7
()) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Subset
of ) ;
end;
definition
let
T
be ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) ;
attr
T
is
dense-in-itself
means
:: TOPGEN_1:def 8
[#]
T
: ( ( non
empty
V105
()
V106
()
V107
()
V108
() ) ( non
empty
V105
()
V106
()
V107
()
V108
() )
L7
()) : ( ( ) ( non
empty
non
proper
)
Element
of
K10
( the
carrier
of
T
: ( ( non
empty
V105
()
V106
()
V107
()
V108
() ) ( non
empty
V105
()
V106
()
V107
()
V108
() )
L7
()) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( non
empty
)
set
) ) is
dense-in-itself
;
end;
theorem
:: TOPGEN_1:36
for
T
being ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
)
for
A
being ( ( ) ( )
Subset
of ) st
T
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) is
T_1
&
A
: ( ( ) ( )
Subset
of ) is
dense-in-itself
holds
Cl
A
: ( ( ) ( )
Subset
of ) : ( ( ) (
closed
)
Element
of
K10
( the
carrier
of
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( non
empty
)
set
) ) is
dense-in-itself
;
definition
let
T
be ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) ;
let
F
be ( ( ) ( )
Subset-Family
of ) ;
attr
F
is
dense-in-itself
means
:: TOPGEN_1:def 9
for
A
being ( ( ) ( )
Subset
of ) st
A
: ( ( ) ( )
Subset
of )
in
F
: ( ( ) ( )
Element
of
K10
( the
carrier
of
T
: ( ( non
empty
V105
()
V106
()
V107
()
V108
() ) ( non
empty
V105
()
V106
()
V107
()
V108
() )
L7
()) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( non
empty
)
set
) ) holds
A
: ( ( ) ( )
Subset
of ) is
dense-in-itself
;
end;
theorem
:: TOPGEN_1:37
for
T
being ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
)
for
F
being ( ( ) ( )
Subset-Family
of ) st
F
: ( ( ) ( )
Subset-Family
of ) is
dense-in-itself
holds
union
F
: ( ( ) ( )
Subset-Family
of ) : ( ( ) ( )
Element
of
K10
( the
carrier
of
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( non
empty
)
set
) )
c=
union
(
Der
F
: ( ( ) ( )
Subset-Family
of )
)
: ( ( ) ( )
Subset-Family
of ) : ( ( ) ( )
Element
of
K10
( the
carrier
of
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( non
empty
)
set
) ) ;
theorem
:: TOPGEN_1:38
for
T
being ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
)
for
F
being ( ( ) ( )
Subset-Family
of ) st
F
: ( ( ) ( )
Subset-Family
of ) is
dense-in-itself
holds
union
F
: ( ( ) ( )
Subset-Family
of ) : ( ( ) ( )
Element
of
K10
( the
carrier
of
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( non
empty
)
set
) ) is
dense-in-itself
;
theorem
:: TOPGEN_1:39
for
T
being ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) holds
Fr
(
{}
T
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
)
)
: ( ( ) (
empty
proper
ordinal
cardinal
{}
: ( ( ) ( )
set
)
-element
open
boundary
nowhere_dense
)
Element
of
K10
( the
carrier
of
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( non
empty
)
set
) ) : ( ( ) (
closed
boundary
nowhere_dense
)
Element
of
K10
( the
carrier
of
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( non
empty
)
set
) )
=
{}
: ( ( ) ( )
set
) ;
registration
let
T
be ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) ;
let
A
be ( (
open
closed
) (
open
closed
)
Subset
of ) ;
cluster
Fr
A
: ( (
open
closed
) (
open
closed
)
Element
of
K10
( the
carrier
of
T
: ( (
TopSpace-like
) (
TopSpace-like
)
TopStruct
) : ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) : ( ( ) (
closed
boundary
nowhere_dense
)
Element
of
K10
( the
carrier
of
T
: ( (
TopSpace-like
) (
TopSpace-like
)
TopStruct
) : ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) )
->
empty
;
end;
registration
let
T
be ( ( non
empty
TopSpace-like
non
discrete
) ( non
empty
V47
()
TopSpace-like
non
discrete
)
TopSpace
) ;
cluster
non
open
for ( ( ) ( )
Element
of
K10
( the
carrier
of
T
: ( ( non
empty
TopSpace-like
non
discrete
) ( non
empty
V47
()
TopSpace-like
non
discrete
)
TopStruct
) : ( ( ) ( non
empty
V2
() )
set
) ) : ( ( ) ( non
empty
)
set
) ) ;
cluster
non
closed
for ( ( ) ( )
Element
of
K10
( the
carrier
of
T
: ( ( non
empty
TopSpace-like
non
discrete
) ( non
empty
V47
()
TopSpace-like
non
discrete
)
TopStruct
) : ( ( ) ( non
empty
V2
() )
set
) ) : ( ( ) ( non
empty
)
set
) ) ;
end;
registration
let
T
be ( ( non
empty
TopSpace-like
non
discrete
) ( non
empty
V47
()
TopSpace-like
non
discrete
)
TopSpace
) ;
let
A
be ( ( non
open
) ( non
open
)
Subset
of ) ;
cluster
Fr
A
: ( ( non
open
) ( non
open
)
Element
of
K10
( the
carrier
of
T
: ( ( non
empty
TopSpace-like
non
discrete
) ( non
empty
V47
()
TopSpace-like
non
discrete
)
TopStruct
) : ( ( ) ( non
empty
V2
() )
set
) ) : ( ( ) ( non
empty
)
set
) ) : ( ( ) (
closed
)
Element
of
K10
( the
carrier
of
T
: ( ( non
empty
TopSpace-like
non
discrete
) ( non
empty
V47
()
TopSpace-like
non
discrete
)
TopStruct
) : ( ( ) ( non
empty
V2
() )
set
) ) : ( ( ) ( non
empty
)
set
) )
->
non
empty
;
end;
registration
let
T
be ( ( non
empty
TopSpace-like
non
discrete
) ( non
empty
V47
()
TopSpace-like
non
discrete
)
TopSpace
) ;
let
A
be ( ( non
closed
) ( non
closed
)
Subset
of ) ;
cluster
Fr
A
: ( ( non
closed
) ( non
closed
)
Element
of
K10
( the
carrier
of
T
: ( ( non
empty
TopSpace-like
non
discrete
) ( non
empty
V47
()
TopSpace-like
non
discrete
)
TopStruct
) : ( ( ) ( non
empty
V2
() )
set
) ) : ( ( ) ( non
empty
)
set
) ) : ( ( ) (
closed
)
Element
of
K10
( the
carrier
of
T
: ( ( non
empty
TopSpace-like
non
discrete
) ( non
empty
V47
()
TopSpace-like
non
discrete
)
TopStruct
) : ( ( ) ( non
empty
V2
() )
set
) ) : ( ( ) ( non
empty
)
set
) )
->
non
empty
;
end;
begin
definition
let
T
be ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) ;
let
A
be ( ( ) ( )
Subset
of ) ;
attr
A
is
perfect
means
:: TOPGEN_1:def 10
(
A
: ( ( non
closed
) ( non
closed
)
Element
of
K10
( the
carrier
of
T
: ( ( non
empty
TopSpace-like
non
discrete
) ( non
empty
V47
()
TopSpace-like
non
discrete
)
TopStruct
) : ( ( ) ( non
empty
V2
() )
set
) ) : ( ( ) ( non
empty
)
set
) ) is
closed
&
A
: ( ( non
closed
) ( non
closed
)
Element
of
K10
( the
carrier
of
T
: ( ( non
empty
TopSpace-like
non
discrete
) ( non
empty
V47
()
TopSpace-like
non
discrete
)
TopStruct
) : ( ( ) ( non
empty
V2
() )
set
) ) : ( ( ) ( non
empty
)
set
) ) is
dense-in-itself
);
end;
registration
let
T
be ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) ;
cluster
perfect
->
closed
dense-in-itself
for ( ( ) ( )
Element
of
K10
( the
carrier
of
T
: ( ( non
empty
TopSpace-like
non
discrete
) ( non
empty
V47
()
TopSpace-like
non
discrete
)
TopStruct
) : ( ( ) ( non
empty
V2
() )
set
) ) : ( ( ) ( non
empty
)
set
) ) ;
cluster
closed
dense-in-itself
->
perfect
for ( ( ) ( )
Element
of
K10
( the
carrier
of
T
: ( ( non
empty
TopSpace-like
non
discrete
) ( non
empty
V47
()
TopSpace-like
non
discrete
)
TopStruct
) : ( ( ) ( non
empty
V2
() )
set
) ) : ( ( ) ( non
empty
)
set
) ) ;
end;
theorem
:: TOPGEN_1:40
for
T
being ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) holds
Der
(
{}
T
: ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
)
)
: ( ( ) (
empty
ordinal
cardinal
{}
: ( ( ) ( )
set
)
-element
open
boundary
nowhere_dense
)
Element
of
K10
( the
carrier
of
b
1
: ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) : ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Subset
of )
=
{}
T
: ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) : ( ( ) (
empty
ordinal
cardinal
{}
: ( ( ) ( )
set
)
-element
open
boundary
nowhere_dense
)
Element
of
K10
( the
carrier
of
b
1
: ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) : ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) ;
theorem
:: TOPGEN_1:41
for
T
being ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
)
for
A
being ( ( ) ( )
Subset
of ) holds
(
A
: ( ( ) ( )
Subset
of ) is
perfect
iff
Der
A
: ( ( ) ( )
Subset
of ) : ( ( ) ( )
Subset
of )
=
A
: ( ( ) ( )
Subset
of ) ) ;
theorem
:: TOPGEN_1:42
for
T
being ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) holds
{}
T
: ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) : ( ( ) (
empty
ordinal
cardinal
{}
: ( ( ) ( )
set
)
-element
open
boundary
nowhere_dense
)
Element
of
K10
( the
carrier
of
b
1
: ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) : ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) is
perfect
;
registration
let
T
be ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) ;
cluster
empty
->
perfect
for ( ( ) ( )
Element
of
K10
( the
carrier
of
T
: ( ( non
empty
TopSpace-like
non
discrete
) ( non
empty
V47
()
TopSpace-like
non
discrete
)
TopStruct
) : ( ( ) ( non
empty
V2
() )
set
) ) : ( ( ) ( non
empty
)
set
) ) ;
end;
registration
let
T
be ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) ;
cluster
perfect
for ( ( ) ( )
Element
of
K10
( the
carrier
of
T
: ( (
TopSpace-like
) (
TopSpace-like
)
TopStruct
) : ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) ;
end;
begin
definition
let
T
be ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) ;
let
A
be ( ( ) ( )
Subset
of ) ;
attr
A
is
scattered
means
:: TOPGEN_1:def 11
for
B
being ( ( ) ( )
Subset
of ) holds
(
B
: ( ( ) ( )
Subset
of ) is
empty
or not
B
: ( ( ) ( )
Subset
of )
c=
A
: ( ( non
closed
) ( non
closed
)
Element
of
K10
( the
carrier
of
T
: ( (
TopSpace-like
) (
TopSpace-like
)
TopStruct
) : ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) or not
B
: ( ( ) ( )
Subset
of ) is
dense-in-itself
);
end;
registration
let
T
be ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) ;
cluster
non
empty
scattered
->
non
dense-in-itself
for ( ( ) ( )
Element
of
K10
( the
carrier
of
T
: ( (
TopSpace-like
) (
TopSpace-like
)
TopStruct
) : ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) ;
cluster
non
empty
dense-in-itself
->
non
scattered
for ( ( ) ( )
Element
of
K10
( the
carrier
of
T
: ( (
TopSpace-like
) (
TopSpace-like
)
TopStruct
) : ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) ;
end;
theorem
:: TOPGEN_1:43
for
T
being ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) holds
{}
T
: ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) : ( ( ) (
empty
ordinal
cardinal
{}
: ( ( ) ( )
set
)
-element
open
closed
boundary
nowhere_dense
dense-in-itself
perfect
)
Element
of
K10
( the
carrier
of
b
1
: ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) : ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) is
scattered
;
registration
let
T
be ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) ;
cluster
empty
->
scattered
for ( ( ) ( )
Element
of
K10
( the
carrier
of
T
: ( (
TopSpace-like
) (
TopSpace-like
)
TopStruct
) : ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) ;
end;
theorem
:: TOPGEN_1:44
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
ex
A
,
B
being ( ( ) ( )
Subset
of ) st
(
A
: ( ( ) ( )
Subset
of )
\/
B
: ( ( ) ( )
Subset
of ) : ( ( ) ( )
Element
of
K10
( the
carrier
of
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( non
empty
)
set
) )
=
[#]
T
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) : ( ( ) ( non
empty
non
proper
open
dense
non
boundary
)
Element
of
K10
( the
carrier
of
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( non
empty
)
set
) ) &
A
: ( ( ) ( )
Subset
of )
misses
B
: ( ( ) ( )
Subset
of ) &
A
: ( ( ) ( )
Subset
of ) is
perfect
&
B
: ( ( ) ( )
Subset
of ) is
scattered
) ;
registration
let
T
be ( (
TopSpace-like
discrete
) (
TopSpace-like
discrete
)
TopSpace
) ;
let
A
be ( ( ) ( )
Subset
of ) ;
cluster
Fr
A
: ( ( ) ( )
Element
of
K10
( the
carrier
of
T
: ( (
TopSpace-like
discrete
) (
TopSpace-like
discrete
)
TopStruct
) : ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) : ( ( ) (
closed
)
Element
of
K10
( the
carrier
of
T
: ( (
TopSpace-like
discrete
) (
TopSpace-like
discrete
)
TopStruct
) : ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) )
->
empty
;
end;
registration
let
T
be ( (
TopSpace-like
discrete
) (
TopSpace-like
discrete
)
TopSpace
) ;
cluster
->
open
closed
for ( ( ) ( )
Element
of
K10
( the
carrier
of
T
: ( (
TopSpace-like
) (
TopSpace-like
)
TopStruct
) : ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) ;
end;
theorem
:: TOPGEN_1:45
for
T
being ( (
TopSpace-like
discrete
) (
TopSpace-like
discrete
)
TopSpace
)
for
A
being ( ( ) (
open
closed
)
Subset
of ) holds
Der
A
: ( ( ) (
open
closed
)
Subset
of ) : ( ( ) (
open
closed
)
Subset
of )
=
{}
: ( ( ) ( )
set
) ;
registration
let
T
be ( ( non
empty
TopSpace-like
discrete
) ( non
empty
TopSpace-like
T_1
T_2
V64
()
normal
discrete
)
TopSpace
) ;
let
A
be ( ( ) (
open
closed
)
Subset
of ) ;
cluster
Der
A
: ( ( ) (
open
closed
)
Element
of
K10
( the
carrier
of
T
: ( ( non
empty
TopSpace-like
discrete
) ( non
empty
TopSpace-like
T_1
T_2
V64
()
normal
discrete
)
TopStruct
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( non
empty
)
set
) ) : ( ( ) (
open
closed
)
Subset
of )
->
empty
;
end;
begin
definition
let
T
be ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) ;
func
density
T
->
( (
cardinal
) (
ordinal
cardinal
)
number
)
means
:: TOPGEN_1:def 12
( ex
A
being ( ( ) ( )
Subset
of ) st
(
A
: ( ( ) ( )
Subset
of ) is
dense
&
it
: ( ( ) (
open
closed
)
Element
of
K10
( the
carrier
of
T
: ( (
TopSpace-like
) (
TopSpace-like
)
TopStruct
) : ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) )
=
card
A
: ( ( ) ( )
Subset
of ) : ( (
cardinal
) (
ordinal
cardinal
)
set
) ) & ( for
B
being ( ( ) ( )
Subset
of ) st
B
: ( ( ) ( )
Subset
of ) is
dense
holds
it
: ( ( ) (
open
closed
)
Element
of
K10
( the
carrier
of
T
: ( (
TopSpace-like
) (
TopSpace-like
)
TopStruct
) : ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) )
c=
card
B
: ( ( ) ( )
Subset
of ) : ( (
cardinal
) (
ordinal
cardinal
)
set
) ) );
end;
definition
let
T
be ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) ;
attr
T
is
separable
means
:: TOPGEN_1:def 13
density
T
: ( (
TopSpace-like
) (
TopSpace-like
)
TopStruct
) : ( (
cardinal
) (
ordinal
cardinal
)
number
)
c=
omega
: ( ( ) (
ordinal
non
finite
cardinal
limit_cardinal
)
set
) ;
end;
theorem
:: TOPGEN_1:46
for
T
being ( (
TopSpace-like
countable
) (
TopSpace-like
countable
)
TopSpace
) holds
T
: ( (
TopSpace-like
countable
) (
TopSpace-like
countable
)
TopSpace
) is
separable
;
registration
cluster
TopSpace-like
countable
->
TopSpace-like
separable
for ( ( ) ( )
TopStruct
) ;
end;
begin
theorem
:: TOPGEN_1:47
for
A
being ( ( ) ( )
Subset
of ) st
A
: ( ( ) ( )
Subset
of )
=
RAT
: ( ( ) ( )
set
) holds
A
: ( ( ) ( )
Subset
of )
`
: ( ( ) ( )
Element
of
K10
( the
carrier
of
R^1
: ( (
TopSpace-like
) ( non
empty
strict
TopSpace-like
V114
() )
TopStruct
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( non
empty
)
set
) )
=
IRRAT
: ( ( ) ( )
Element
of
K10
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) ;
theorem
:: TOPGEN_1:48
for
A
being ( ( ) ( )
Subset
of ) st
A
: ( ( ) ( )
Subset
of )
=
IRRAT
: ( ( ) ( )
Element
of
K10
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) holds
A
: ( ( ) ( )
Subset
of )
`
: ( ( ) ( )
Element
of
K10
( the
carrier
of
R^1
: ( (
TopSpace-like
) ( non
empty
strict
TopSpace-like
V114
() )
TopStruct
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( non
empty
)
set
) )
=
RAT
: ( ( ) ( )
set
) ;
theorem
:: TOPGEN_1:49
for
A
being ( ( ) ( )
Subset
of ) st
A
: ( ( ) ( )
Subset
of )
=
RAT
: ( ( ) ( )
set
) holds
Int
A
: ( ( ) ( )
Subset
of ) : ( ( ) (
open
)
Element
of
K10
( the
carrier
of
R^1
: ( (
TopSpace-like
) ( non
empty
strict
TopSpace-like
V114
() )
TopStruct
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( non
empty
)
set
) )
=
{}
: ( ( ) ( )
set
) ;
theorem
:: TOPGEN_1:50
for
A
being ( ( ) ( )
Subset
of ) st
A
: ( ( ) ( )
Subset
of )
=
IRRAT
: ( ( ) ( )
Element
of
K10
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) holds
Int
A
: ( ( ) ( )
Subset
of ) : ( ( ) (
open
)
Element
of
K10
( the
carrier
of
R^1
: ( (
TopSpace-like
) ( non
empty
strict
TopSpace-like
V114
() )
TopStruct
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( non
empty
)
set
) )
=
{}
: ( ( ) ( )
set
) ;
theorem
:: TOPGEN_1:51
RAT
: ( ( ) ( )
set
) is ( (
dense
) (
dense
)
Subset
of ) ;
theorem
:: TOPGEN_1:52
IRRAT
: ( ( ) ( )
Element
of
K10
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) is ( (
dense
) (
dense
)
Subset
of ) ;
theorem
:: TOPGEN_1:53
RAT
: ( ( ) ( )
set
) is ( (
boundary
) (
boundary
)
Subset
of ) ;
theorem
:: TOPGEN_1:54
IRRAT
: ( ( ) ( )
Element
of
K10
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) is ( (
boundary
) (
boundary
)
Subset
of ) ;
theorem
:: TOPGEN_1:55
REAL
: ( ( ) ( )
set
) is ( ( non
boundary
) ( non
boundary
)
Subset
of ) ;
theorem
:: TOPGEN_1:56
ex
A
,
B
being ( ( ) ( )
Subset
of ) st
(
A
: ( ( ) ( )
Subset
of ) is
boundary
&
B
: ( ( ) ( )
Subset
of ) is
boundary
& not
A
: ( ( ) ( )
Subset
of )
\/
B
: ( ( ) ( )
Subset
of ) : ( ( ) ( )
Element
of
K10
( the
carrier
of
R^1
: ( (
TopSpace-like
) ( non
empty
strict
TopSpace-like
V114
() )
TopStruct
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( non
empty
)
set
) ) is
boundary
) ;