:: CONNSP_2 semantic presentation
begin
definition
let
X
be ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) ;
let
x
be ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) ) ;
mode
a_neighborhood
of
x
->
( ( ) ( )
Subset
of )
means
:: CONNSP_2:def 1
x
: ( ( ) ( )
Element
of
K10
(
K10
(
X
: ( ( ) ( )
TopStruct
) ) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( non
empty
)
set
) )
in
Int
it
: ( ( ) ( )
Element
of
X
: ( ( ) ( )
TopStruct
) ) : ( ( ) ( )
Element
of
K10
( the
U1
of
X
: ( ( ) ( )
TopStruct
) : ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) ;
end;
definition
let
X
be ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) ;
let
A
be ( ( ) ( )
Subset
of ) ;
mode
a_neighborhood
of
A
->
( ( ) ( )
Subset
of )
means
:: CONNSP_2:def 2
A
: ( ( ) ( )
Element
of
K10
(
K10
(
X
: ( ( ) ( )
TopStruct
) ) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( non
empty
)
set
) )
c=
Int
it
: ( ( ) ( )
Element
of
X
: ( ( ) ( )
TopStruct
) ) : ( ( ) ( )
Element
of
K10
( the
U1
of
X
: ( ( ) ( )
TopStruct
) : ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) ;
end;
theorem
:: CONNSP_2:1
for
X
being ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
)
for
x
being ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) )
for
A
,
B
being ( ( ) ( )
Subset
of ) st
A
: ( ( ) ( )
Subset
of ) is ( ( ) ( )
a_neighborhood
of
x
: ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) ) ) &
B
: ( ( ) ( )
Subset
of ) is ( ( ) ( )
a_neighborhood
of
x
: ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) ) ) holds
A
: ( ( ) ( )
Subset
of )
\/
B
: ( ( ) ( )
Subset
of ) : ( ( ) ( )
Element
of
K10
( the
U1
of
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( non
empty
)
set
) ) is ( ( ) ( )
a_neighborhood
of
x
: ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) ) ) ;
theorem
:: CONNSP_2:2
for
X
being ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
)
for
x
being ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) )
for
A
,
B
being ( ( ) ( )
Subset
of ) holds
( (
A
: ( ( ) ( )
Subset
of ) is ( ( ) ( )
a_neighborhood
of
x
: ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) ) ) &
B
: ( ( ) ( )
Subset
of ) is ( ( ) ( )
a_neighborhood
of
x
: ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) ) ) ) iff
A
: ( ( ) ( )
Subset
of )
/\
B
: ( ( ) ( )
Subset
of ) : ( ( ) ( )
Element
of
K10
( the
U1
of
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( non
empty
)
set
) ) is ( ( ) ( )
a_neighborhood
of
x
: ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) ) ) ) ;
theorem
:: CONNSP_2:3
for
X
being ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
)
for
U1
being ( ( ) ( )
Subset
of )
for
x
being ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) ) st
U1
: ( ( ) ( )
Subset
of ) is
open
&
x
: ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) )
in
U1
: ( ( ) ( )
Subset
of ) holds
U1
: ( ( ) ( )
Subset
of ) is ( ( ) ( )
a_neighborhood
of
x
: ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) ) ) ;
theorem
:: CONNSP_2:4
for
X
being ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
)
for
U1
being ( ( ) ( )
Subset
of )
for
x
being ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) ) st
U1
: ( ( ) ( )
Subset
of ) is ( ( ) ( )
a_neighborhood
of
x
: ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) ) ) holds
x
: ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) )
in
U1
: ( ( ) ( )
Subset
of ) ;
theorem
:: CONNSP_2:5
for
X
being ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
)
for
x
being ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) )
for
U1
being ( ( ) ( )
Subset
of ) st
U1
: ( ( ) ( )
Subset
of ) is ( ( ) ( )
a_neighborhood
of
x
: ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) ) ) holds
ex
V
being ( ( non
empty
) ( non
empty
)
Subset
of ) st
(
V
: ( ( non
empty
) ( non
empty
)
Subset
of ) is ( ( ) ( )
a_neighborhood
of
x
: ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) ) ) &
V
: ( ( non
empty
) ( non
empty
)
Subset
of ) is
open
&
V
: ( ( non
empty
) ( non
empty
)
Subset
of )
c=
U1
: ( ( ) ( )
Subset
of ) ) ;
theorem
:: CONNSP_2:6
for
X
being ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
)
for
x
being ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) )
for
U1
being ( ( ) ( )
Subset
of ) holds
(
U1
: ( ( ) ( )
Subset
of ) is ( ( ) ( )
a_neighborhood
of
x
: ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) ) ) iff ex
V
being ( ( ) ( )
Subset
of ) st
(
V
: ( ( ) ( )
Subset
of ) is
open
&
V
: ( ( ) ( )
Subset
of )
c=
U1
: ( ( ) ( )
Subset
of ) &
x
: ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) )
in
V
: ( ( ) ( )
Subset
of ) ) ) ;
theorem
:: CONNSP_2:7
for
X
being ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
)
for
U1
being ( ( ) ( )
Subset
of ) holds
(
U1
: ( ( ) ( )
Subset
of ) is
open
iff for
x
being ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) ) st
x
: ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) )
in
U1
: ( ( ) ( )
Subset
of ) holds
ex
A
being ( ( ) ( )
Subset
of ) st
(
A
: ( ( ) ( )
Subset
of ) is ( ( ) ( )
a_neighborhood
of
x
: ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) ) ) &
A
: ( ( ) ( )
Subset
of )
c=
U1
: ( ( ) ( )
Subset
of ) ) ) ;
theorem
:: CONNSP_2:8
for
X
being ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
)
for
x
being ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) )
for
V
being ( ( ) ( )
Subset
of ) holds
(
V
: ( ( ) ( )
Subset
of ) is ( ( ) ( )
a_neighborhood
of
{
x
: ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) )
}
: ( ( ) ( non
empty
connected
)
Element
of
K10
( the
U1
of
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( non
empty
)
set
) ) ) iff
V
: ( ( ) ( )
Subset
of ) is ( ( ) ( )
a_neighborhood
of
x
: ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) ) ) ) ;
theorem
:: CONNSP_2:9
for
X
being ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
)
for
B
being ( ( non
empty
) ( non
empty
)
Subset
of )
for
x
being ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) )
for
A
being ( ( ) ( )
Subset
of )
for
A1
being ( ( ) ( )
Subset
of )
for
x1
being ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) ) st
B
: ( ( non
empty
) ( non
empty
)
Subset
of ) is
open
&
A
: ( ( ) ( )
Subset
of ) is ( ( ) ( )
a_neighborhood
of
x
: ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) ) ) &
A
: ( ( ) ( )
Subset
of )
=
A1
: ( ( ) ( )
Subset
of ) &
x
: ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) )
=
x1
: ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) ) holds
A1
: ( ( ) ( )
Subset
of ) is ( ( ) ( )
a_neighborhood
of
x1
: ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) ) ) ;
theorem
:: CONNSP_2:10
for
X
being ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
)
for
B
being ( ( non
empty
) ( non
empty
)
Subset
of )
for
x
being ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) )
for
A
being ( ( ) ( )
Subset
of )
for
A1
being ( ( ) ( )
Subset
of )
for
x1
being ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) ) st
A1
: ( ( ) ( )
Subset
of ) is ( ( ) ( )
a_neighborhood
of
x1
: ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) ) ) &
A
: ( ( ) ( )
Subset
of )
=
A1
: ( ( ) ( )
Subset
of ) &
x
: ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) )
=
x1
: ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) ) holds
A
: ( ( ) ( )
Subset
of ) is ( ( ) ( )
a_neighborhood
of
x
: ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) ) ) ;
theorem
:: CONNSP_2:11
for
X
being ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
)
for
A
,
B
being ( ( ) ( )
Subset
of ) st
A
: ( ( ) ( )
Subset
of ) is
a_component
&
A
: ( ( ) ( )
Subset
of )
c=
B
: ( ( ) ( )
Subset
of ) holds
A
: ( ( ) ( )
Subset
of )
is_a_component_of
B
: ( ( ) ( )
Subset
of ) ;
theorem
:: CONNSP_2:12
for
X
being ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
)
for
X1
being ( ( non
empty
) ( non
empty
TopSpace-like
)
SubSpace
of
X
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) )
for
x
being ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) )
for
x1
being ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) ) st
x
: ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) )
=
x1
: ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) ) holds
Component_of
x1
: ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) ) : ( ( ) ( non
empty
connected
)
Element
of
K10
( the
U1
of
b
2
: ( ( non
empty
) ( non
empty
TopSpace-like
)
SubSpace
of
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) ) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( non
empty
)
set
) )
c=
Component_of
x
: ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) ) : ( ( ) ( non
empty
connected
)
Element
of
K10
( the
U1
of
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( non
empty
)
set
) ) ;
definition
let
X
be ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) ;
let
x
be ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) ) ;
pred
X
is_locally_connected_in
x
means
:: CONNSP_2:def 3
for
U1
being ( ( ) ( )
Subset
of ) st
U1
: ( ( ) ( )
Subset
of ) is ( ( ) ( )
a_neighborhood
of
x
: ( ( ) ( )
Element
of
K10
(
K10
(
X
: ( ( ) ( )
TopStruct
) ) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( non
empty
)
set
) ) ) holds
ex
V
being ( ( ) ( )
Subset
of ) st
(
V
: ( ( ) ( )
Subset
of ) is ( ( ) ( )
a_neighborhood
of
x
: ( ( ) ( )
Element
of
K10
(
K10
(
X
: ( ( ) ( )
TopStruct
) ) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( non
empty
)
set
) ) ) &
V
: ( ( ) ( )
Subset
of ) is
connected
&
V
: ( ( ) ( )
Subset
of )
c=
U1
: ( ( ) ( )
Subset
of ) );
end;
definition
let
X
be ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) ;
attr
X
is
locally_connected
means
:: CONNSP_2:def 4
for
x
being ( ( ) ( )
Point
of ( ( ) ( )
set
) ) holds
X
: ( ( ) ( )
TopStruct
)
is_locally_connected_in
x
: ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) ) ;
end;
definition
let
X
be ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) ;
let
A
be ( ( ) ( )
Subset
of ) ;
let
x
be ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) ) ;
pred
A
is_locally_connected_in
x
means
:: CONNSP_2:def 5
for
B
being ( ( non
empty
) ( non
empty
)
Subset
of ) st
A
: ( ( ) ( )
Element
of
K10
(
K10
(
X
: ( ( ) ( )
TopStruct
) ) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( non
empty
)
set
) )
=
B
: ( ( non
empty
) ( non
empty
)
Subset
of ) holds
ex
x1
being ( ( ) ( )
Point
of ( ( ) ( )
set
) ) st
(
x1
: ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) )
=
x
: ( ( ) ( )
Element
of
X
: ( ( ) ( )
TopStruct
) ) &
X
: ( ( ) ( )
TopStruct
)
|
B
: ( ( non
empty
) ( non
empty
)
Subset
of ) : ( (
strict
) (
strict
)
SubSpace
of
X
: ( ( ) ( )
TopStruct
) )
is_locally_connected_in
x1
: ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) ) );
end;
definition
let
X
be ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) ;
let
A
be ( ( non
empty
) ( non
empty
)
Subset
of ) ;
attr
A
is
locally_connected
means
:: CONNSP_2:def 6
X
: ( ( ) ( )
TopStruct
)
|
A
: ( ( ) ( )
Element
of
K10
(
K10
(
X
: ( ( ) ( )
TopStruct
) ) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( non
empty
)
set
) ) : ( (
strict
) (
strict
)
SubSpace
of
X
: ( ( ) ( )
TopStruct
) ) is
locally_connected
;
end;
theorem
:: CONNSP_2:13
for
X
being ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
)
for
x
being ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) ) holds
(
X
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
)
is_locally_connected_in
x
: ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) ) iff for
V
,
S
being ( ( ) ( )
Subset
of ) st
V
: ( ( ) ( )
Subset
of ) is ( ( ) ( )
a_neighborhood
of
x
: ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) ) ) &
S
: ( ( ) ( )
Subset
of )
is_a_component_of
V
: ( ( ) ( )
Subset
of ) &
x
: ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) )
in
S
: ( ( ) ( )
Subset
of ) holds
S
: ( ( ) ( )
Subset
of ) is ( ( ) ( )
a_neighborhood
of
x
: ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) ) ) ) ;
theorem
:: CONNSP_2:14
for
X
being ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
)
for
x
being ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) ) holds
(
X
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
)
is_locally_connected_in
x
: ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) ) iff for
U1
being ( ( non
empty
) ( non
empty
)
Subset
of ) st
U1
: ( ( non
empty
) ( non
empty
)
Subset
of ) is
open
&
x
: ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) )
in
U1
: ( ( non
empty
) ( non
empty
)
Subset
of ) holds
ex
x1
being ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) ) st
(
x1
: ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) )
=
x
: ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) ) &
x
: ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) )
in
Int
(
Component_of
x1
: ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) )
)
: ( ( ) ( non
empty
connected
)
Element
of
K10
( the
U1
of
(
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
)
|
b
3
: ( ( non
empty
) ( non
empty
)
Subset
of )
)
: ( (
strict
) ( non
empty
strict
TopSpace-like
)
SubSpace
of
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) ) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( non
empty
)
set
) ) : ( ( ) (
open
)
Element
of
K10
( the
U1
of
(
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
)
|
b
3
: ( ( non
empty
) ( non
empty
)
Subset
of )
)
: ( (
strict
) ( non
empty
strict
TopSpace-like
)
SubSpace
of
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) ) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( non
empty
)
set
) ) ) ) ;
theorem
:: CONNSP_2:15
for
X
being ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) st
X
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) is
locally_connected
holds
for
S
being ( ( ) ( )
Subset
of ) st
S
: ( ( ) ( )
Subset
of ) is
a_component
holds
S
: ( ( ) ( )
Subset
of ) is
open
;
theorem
:: CONNSP_2:16
for
X
being ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
)
for
x
being ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) ) st
X
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
)
is_locally_connected_in
x
: ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) ) holds
for
A
being ( ( non
empty
) ( non
empty
)
Subset
of ) st
A
: ( ( non
empty
) ( non
empty
)
Subset
of ) is
open
&
x
: ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) )
in
A
: ( ( non
empty
) ( non
empty
)
Subset
of ) holds
A
: ( ( non
empty
) ( non
empty
)
Subset
of )
is_locally_connected_in
x
: ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) ) ;
theorem
:: CONNSP_2:17
for
X
being ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) st
X
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) is
locally_connected
holds
for
A
being ( ( non
empty
) ( non
empty
)
Subset
of ) st
A
: ( ( non
empty
) ( non
empty
)
Subset
of ) is
open
holds
A
: ( ( non
empty
) ( non
empty
)
Subset
of ) is
locally_connected
;
theorem
:: CONNSP_2:18
for
X
being ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) holds
(
X
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) is
locally_connected
iff for
A
being ( ( non
empty
) ( non
empty
)
Subset
of )
for
B
being ( ( ) ( )
Subset
of ) st
A
: ( ( non
empty
) ( non
empty
)
Subset
of ) is
open
&
B
: ( ( ) ( )
Subset
of )
is_a_component_of
A
: ( ( non
empty
) ( non
empty
)
Subset
of ) holds
B
: ( ( ) ( )
Subset
of ) is
open
) ;
theorem
:: CONNSP_2:19
for
X
being ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) st
X
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) is
locally_connected
holds
for
E
being ( ( non
empty
) ( non
empty
)
Subset
of )
for
C
being ( ( non
empty
) ( non
empty
)
Subset
of ) st
C
: ( ( non
empty
) ( non
empty
)
Subset
of ) is
connected
&
C
: ( ( non
empty
) ( non
empty
)
Subset
of ) is
open
holds
ex
H
being ( ( ) ( )
Subset
of ) st
(
H
: ( ( ) ( )
Subset
of ) is
open
&
H
: ( ( ) ( )
Subset
of ) is
connected
&
C
: ( ( non
empty
) ( non
empty
)
Subset
of )
=
E
: ( ( non
empty
) ( non
empty
)
Subset
of )
/\
H
: ( ( ) ( )
Subset
of ) : ( ( ) ( )
Element
of
K10
( the
U1
of
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( non
empty
)
set
) ) ) ;
theorem
:: CONNSP_2:20
for
X
being ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) holds
(
X
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) is
normal
iff for
A
,
C
being ( ( ) ( )
Subset
of ) st
A
: ( ( ) ( )
Subset
of )
<>
{}
: ( ( ) (
empty
)
set
) &
C
: ( ( ) ( )
Subset
of )
<>
[#]
X
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) : ( ( ) ( non
empty
non
proper
open
closed
dense
non
boundary
)
Element
of
K10
( the
U1
of
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( non
empty
)
set
) ) &
A
: ( ( ) ( )
Subset
of )
c=
C
: ( ( ) ( )
Subset
of ) &
A
: ( ( ) ( )
Subset
of ) is
closed
&
C
: ( ( ) ( )
Subset
of ) is
open
holds
ex
G
being ( ( ) ( )
Subset
of ) st
(
G
: ( ( ) ( )
Subset
of ) is
open
&
A
: ( ( ) ( )
Subset
of )
c=
G
: ( ( ) ( )
Subset
of ) &
Cl
G
: ( ( ) ( )
Subset
of ) : ( ( ) (
closed
)
Element
of
K10
( the
U1
of
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( non
empty
)
set
) )
c=
C
: ( ( ) ( )
Subset
of ) ) ) ;
theorem
:: CONNSP_2:21
for
X
being ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) st
X
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) is
locally_connected
&
X
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) is
normal
holds
for
A
,
B
being ( ( ) ( )
Subset
of ) st
A
: ( ( ) ( )
Subset
of )
<>
{}
: ( ( ) (
empty
)
set
) &
B
: ( ( ) ( )
Subset
of )
<>
{}
: ( ( ) (
empty
)
set
) &
A
: ( ( ) ( )
Subset
of ) is
closed
&
B
: ( ( ) ( )
Subset
of ) is
closed
&
A
: ( ( ) ( )
Subset
of )
misses
B
: ( ( ) ( )
Subset
of ) &
A
: ( ( ) ( )
Subset
of ) is
connected
&
B
: ( ( ) ( )
Subset
of ) is
connected
holds
ex
R
,
S
being ( ( ) ( )
Subset
of ) st
(
R
: ( ( ) ( )
Subset
of ) is
connected
&
S
: ( ( ) ( )
Subset
of ) is
connected
&
R
: ( ( ) ( )
Subset
of ) is
open
&
S
: ( ( ) ( )
Subset
of ) is
open
&
A
: ( ( ) ( )
Subset
of )
c=
R
: ( ( ) ( )
Subset
of ) &
B
: ( ( ) ( )
Subset
of )
c=
S
: ( ( ) ( )
Subset
of ) &
R
: ( ( ) ( )
Subset
of )
misses
S
: ( ( ) ( )
Subset
of ) ) ;
theorem
:: CONNSP_2:22
for
X
being ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
)
for
x
being ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) )
for
F
being ( ( ) ( )
Subset-Family
of ) st ( for
A
being ( ( ) ( )
Subset
of ) holds
(
A
: ( ( ) ( )
Subset
of )
in
F
: ( ( ) ( )
Subset-Family
of ) iff (
A
: ( ( ) ( )
Subset
of ) is
open
&
A
: ( ( ) ( )
Subset
of ) is
closed
&
x
: ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) )
in
A
: ( ( ) ( )
Subset
of ) ) ) ) holds
F
: ( ( ) ( )
Subset-Family
of )
<>
{}
: ( ( ) (
empty
)
set
) ;
definition
let
X
be ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) ;
let
x
be ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) ) ;
func
qComponent_of
x
->
( ( ) ( )
Subset
of )
means
:: CONNSP_2:def 7
ex
F
being ( ( ) ( )
Subset-Family
of ) st
( ( for
A
being ( ( ) ( )
Subset
of ) holds
(
A
: ( ( ) ( )
Subset
of )
in
F
: ( ( ) ( )
Subset-Family
of ) iff (
A
: ( ( ) ( )
Subset
of ) is
open
&
A
: ( ( ) ( )
Subset
of ) is
closed
&
x
: ( ( ) ( )
Element
of
K10
(
K10
(
X
: ( ( ) ( )
TopStruct
) ) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( non
empty
)
set
) )
in
A
: ( ( ) ( )
Subset
of ) ) ) ) &
meet
F
: ( ( ) ( )
Subset-Family
of ) : ( ( ) ( )
Element
of
K10
( the
U1
of
X
: ( ( ) ( )
TopStruct
) : ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) )
=
it
: ( ( ) ( )
Element
of
X
: ( ( ) ( )
TopStruct
) ) );
end;
theorem
:: CONNSP_2:23
for
X
being ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
)
for
x
being ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) ) holds
x
: ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) )
in
qComponent_of
x
: ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Subset
of ) ;
theorem
:: CONNSP_2:24
for
X
being ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
)
for
x
being ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) )
for
A
being ( ( ) ( )
Subset
of ) st
A
: ( ( ) ( )
Subset
of ) is
open
&
A
: ( ( ) ( )
Subset
of ) is
closed
&
x
: ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) )
in
A
: ( ( ) ( )
Subset
of ) &
A
: ( ( ) ( )
Subset
of )
c=
qComponent_of
x
: ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Subset
of ) holds
A
: ( ( ) ( )
Subset
of )
=
qComponent_of
x
: ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Subset
of ) ;
theorem
:: CONNSP_2:25
for
X
being ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
)
for
x
being ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) ) holds
qComponent_of
x
: ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Subset
of ) is
closed
;
theorem
:: CONNSP_2:26
for
X
being ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
)
for
x
being ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) ) holds
Component_of
x
: ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) ) : ( ( ) ( non
empty
connected
)
Element
of
K10
( the
U1
of
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( non
empty
)
set
) )
c=
qComponent_of
x
: ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Subset
of ) ;
theorem
:: CONNSP_2:27
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
Cl
A
: ( ( ) ( )
Subset
of ) : ( ( ) (
closed
)
Element
of
K10
( the
U1
of
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( non
empty
)
set
) ) iff for
G
being ( ( ) ( )
a_neighborhood
of
p
: ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) ) ) holds
G
: ( ( ) ( )
a_neighborhood
of
b
3
: ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) ) )
meets
A
: ( ( ) ( )
Subset
of ) ) ;
theorem
:: CONNSP_2:28
for
X
being ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
)
for
A
being ( ( ) ( )
Subset
of ) holds
[#]
X
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) : ( ( ) ( non
empty
non
proper
open
closed
dense
non
boundary
)
Element
of
K10
( the
U1
of
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( non
empty
)
set
) ) is ( ( ) ( )
a_neighborhood
of
A
: ( ( ) ( )
Subset
of ) ) ;
theorem
:: CONNSP_2:29
for
X
being ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
)
for
A
being ( ( ) ( )
Subset
of )
for
Y
being ( ( ) ( )
a_neighborhood
of
A
: ( ( ) ( )
Subset
of ) ) holds
A
: ( ( ) ( )
Subset
of )
c=
Y
: ( ( ) ( )
a_neighborhood
of
b
2
: ( ( ) ( )
Subset
of ) ) ;