:: Components and Unions of Components
:: by Yatsuka Nakamura and Andrzej Trybulec
::
:: Received February 5, 1996
:: Copyright (c) 1996-2012 Association of Mizar Users
begin
definition
let
GX
be
TopStruct
;
let
V
be
Subset
of
GX
;
func
Component_of
V
->
Subset
of
GX
means
:
Def1
:
:: CONNSP_3:def 1
ex
F
being
Subset-Family
of
GX
st
( ( for
A
being
Subset
of
GX
holds
(
A
in
F
iff (
A
is
connected
&
V
c=
A
) ) ) &
union
F
=
it
);
existence
ex
b
1
being
Subset
of
GX
ex
F
being
Subset-Family
of
GX
st
( ( for
A
being
Subset
of
GX
holds
(
A
in
F
iff (
A
is
connected
&
V
c=
A
) ) ) &
union
F
=
b
1
)
proof
end;
uniqueness
for
b
1
,
b
2
being
Subset
of
GX
st ex
F
being
Subset-Family
of
GX
st
( ( for
A
being
Subset
of
GX
holds
(
A
in
F
iff (
A
is
connected
&
V
c=
A
) ) ) &
union
F
=
b
1
) & ex
F
being
Subset-Family
of
GX
st
( ( for
A
being
Subset
of
GX
holds
(
A
in
F
iff (
A
is
connected
&
V
c=
A
) ) ) &
union
F
=
b
2
) holds
b
1
=
b
2
proof
end;
end;
::
deftheorem
Def1
defines
Component_of
CONNSP_3:def 1 :
for
GX
being
TopStruct
for
V
,
b
3
being
Subset
of
GX
holds
(
b
3
=
Component_of
V
iff ex
F
being
Subset-Family
of
GX
st
( ( for
A
being
Subset
of
GX
holds
(
A
in
F
iff (
A
is
connected
&
V
c=
A
) ) ) &
union
F
=
b
3
) );
theorem
Th1
:
:: CONNSP_3:1
for
GX
being
TopSpace
for
V
being
Subset
of
GX
st ex
A
being
Subset
of
GX
st
(
A
is
connected
&
V
c=
A
) holds
V
c=
Component_of
V
proof
end;
theorem
:: CONNSP_3:2
for
GX
being
TopSpace
for
V
being
Subset
of
GX
st ( for
A
being
Subset
of
GX
holds
( not
A
is
connected
or not
V
c=
A
) ) holds
Component_of
V
=
{}
proof
end;
theorem
Th3
:
:: CONNSP_3:3
for
GX
being non
empty
TopSpace
holds
Component_of
(
{}
GX
)
=
the
carrier
of
GX
proof
end;
theorem
:: CONNSP_3:4
for
GX
being non
empty
TopSpace
for
V
being
Subset
of
GX
st
V
is
connected
holds
Component_of
V
<>
{}
proof
end;
theorem
Th5
:
:: CONNSP_3:5
for
GX
being
TopSpace
for
V
being
Subset
of
GX
st
V
is
connected
&
V
<>
{}
holds
Component_of
V
is
connected
proof
end;
theorem
Th6
:
:: CONNSP_3:6
for
GX
being non
empty
TopSpace
for
V
,
C
being
Subset
of
GX
st
V
is
connected
&
C
is
connected
&
Component_of
V
c=
C
holds
C
=
Component_of
V
proof
end;
theorem
Th7
:
:: CONNSP_3:7
for
GX
being non
empty
TopSpace
for
A
being
Subset
of
GX
st
A
is
a_component
holds
Component_of
A
=
A
proof
end;
theorem
Th8
:
:: CONNSP_3:8
for
GX
being non
empty
TopSpace
for
A
being
Subset
of
GX
holds
(
A
is
a_component
iff ex
V
being
Subset
of
GX
st
(
V
is
connected
&
V
<>
{}
&
A
=
Component_of
V
) )
proof
end;
theorem
:: CONNSP_3:9
for
GX
being non
empty
TopSpace
for
V
being
Subset
of
GX
st
V
is
connected
&
V
<>
{}
holds
Component_of
V
is
a_component
by
Th8
;
theorem
:: CONNSP_3:10
for
GX
being non
empty
TopSpace
for
A
,
V
being
Subset
of
GX
st
A
is
a_component
&
V
is
connected
&
V
c=
A
&
V
<>
{}
holds
A
=
Component_of
V
proof
end;
theorem
Th11
:
:: CONNSP_3:11
for
GX
being non
empty
TopSpace
for
V
being
Subset
of
GX
st
V
is
connected
&
V
<>
{}
holds
Component_of
(
Component_of
V
)
=
Component_of
V
proof
end;
theorem
Th12
:
:: CONNSP_3:12
for
GX
being non
empty
TopSpace
for
A
,
B
being
Subset
of
GX
st
A
is
connected
&
B
is
connected
&
A
<>
{}
&
A
c=
B
holds
Component_of
A
=
Component_of
B
proof
end;
theorem
Th13
:
:: CONNSP_3:13
for
GX
being non
empty
TopSpace
for
A
,
B
being
Subset
of
GX
st
A
is
connected
&
B
is
connected
&
A
<>
{}
&
A
c=
B
holds
B
c=
Component_of
A
proof
end;
theorem
Th14
:
:: CONNSP_3:14
for
GX
being non
empty
TopSpace
for
A
,
B
being
Subset
of
GX
st
A
is
connected
&
A
\/
B
is
connected
&
A
<>
{}
holds
A
\/
B
c=
Component_of
A
proof
end;
theorem
Th15
:
:: CONNSP_3:15
for
GX
being non
empty
TopSpace
for
A
being
Subset
of
GX
for
p
being
Point
of
GX
st
A
is
connected
&
p
in
A
holds
Component_of
p
=
Component_of
A
proof
end;
theorem
:: CONNSP_3:16
for
GX
being non
empty
TopSpace
for
A
,
B
being
Subset
of
GX
st
A
is
connected
&
B
is
connected
&
A
meets
B
holds
(
A
\/
B
c=
Component_of
A
&
A
\/
B
c=
Component_of
B
&
A
c=
Component_of
B
&
B
c=
Component_of
A
)
proof
end;
theorem
:: CONNSP_3:17
for
GX
being non
empty
TopSpace
for
A
being
Subset
of
GX
st
A
is
connected
&
A
<>
{}
holds
Cl
A
c=
Component_of
A
proof
end;
theorem
:: CONNSP_3:18
for
GX
being non
empty
TopSpace
for
A
,
B
being
Subset
of
GX
st
A
is
a_component
&
B
is
connected
&
B
<>
{}
&
A
misses
B
holds
A
misses
Component_of
B
proof
end;
begin
Lm1
:
now
:: thesis:
for
GX
being
TopStruct
ex
F
being
Subset-Family
of
GX
st
( ( for
B
being
Subset
of
GX
st
B
in
F
holds
B
is
a_component
) &
{}
GX
=
union
F
)
let
GX
be
TopStruct
;
:: thesis:
ex
F
being
Subset-Family
of
GX
st
( ( for
B
being
Subset
of
GX
st
B
in
F
holds
B
is
a_component
) &
{}
GX
=
union
F
)
reconsider
S
=
{}
as
Subset-Family
of
GX
by
XBOOLE_1:2
;
for
B
being
Subset
of
GX
st
B
in
S
holds
B
is
a_component
;
hence
ex
F
being
Subset-Family
of
GX
st
( ( for
B
being
Subset
of
GX
st
B
in
F
holds
B
is
a_component
) &
{}
GX
=
union
F
)
by
ZFMISC_1:2
;
:: thesis:
verum
end;
definition
let
GX
be
TopStruct
;
mode
a_union_of_components
of
GX
->
Subset
of
GX
means
:
Def2
:
:: CONNSP_3:def 2
ex
F
being
Subset-Family
of
GX
st
( ( for
B
being
Subset
of
GX
st
B
in
F
holds
B
is
a_component
) &
it
=
union
F
);
existence
ex
b
1
being
Subset
of
GX
ex
F
being
Subset-Family
of
GX
st
( ( for
B
being
Subset
of
GX
st
B
in
F
holds
B
is
a_component
) &
b
1
=
union
F
)
proof
end;
end;
::
deftheorem
Def2
defines
a_union_of_components
CONNSP_3:def 2 :
for
GX
being
TopStruct
for
b
2
being
Subset
of
GX
holds
(
b
2
is
a_union_of_components
of
GX
iff ex
F
being
Subset-Family
of
GX
st
( ( for
B
being
Subset
of
GX
st
B
in
F
holds
B
is
a_component
) &
b
2
=
union
F
) );
theorem
Th19
:
:: CONNSP_3:19
for
GX
being non
empty
TopSpace
holds
{}
GX
is
a_union_of_components
of
GX
proof
end;
theorem
Th20
:
:: CONNSP_3:20
for
GX
being non
empty
TopSpace
for
A
being
Subset
of
GX
st
A
=
the
carrier
of
GX
holds
A
is
a_union_of_components
of
GX
proof
end;
theorem
Th21
:
:: CONNSP_3:21
for
GX
being non
empty
TopSpace
for
A
being
Subset
of
GX
for
p
being
Point
of
GX
st
p
in
A
&
A
is
a_union_of_components
of
GX
holds
Component_of
p
c=
A
proof
end;
theorem
:: CONNSP_3:22
for
GX
being non
empty
TopSpace
for
A
,
B
being
Subset
of
GX
st
A
is
a_union_of_components
of
GX
&
B
is
a_union_of_components
of
GX
holds
(
A
\/
B
is
a_union_of_components
of
GX
&
A
/\
B
is
a_union_of_components
of
GX
)
proof
end;
theorem
:: CONNSP_3:23
for
GX
being non
empty
TopSpace
for
Fu
being
Subset-Family
of
GX
st ( for
A
being
Subset
of
GX
st
A
in
Fu
holds
A
is
a_union_of_components
of
GX
) holds
union
Fu
is
a_union_of_components
of
GX
proof
end;
theorem
:: CONNSP_3:24
for
GX
being non
empty
TopSpace
for
Fu
being
Subset-Family
of
GX
st ( for
A
being
Subset
of
GX
st
A
in
Fu
holds
A
is
a_union_of_components
of
GX
) holds
meet
Fu
is
a_union_of_components
of
GX
proof
end;
theorem
:: CONNSP_3:25
for
GX
being non
empty
TopSpace
for
A
,
B
being
Subset
of
GX
st
A
is
a_union_of_components
of
GX
&
B
is
a_union_of_components
of
GX
holds
A
\
B
is
a_union_of_components
of
GX
proof
end;
begin
definition
let
GX
be
TopStruct
;
let
B
be
Subset
of
GX
;
let
p
be
Point
of
GX
;
assume
A1
:
p
in
B
;
func
Down
(
p
,
B
)
->
Point
of
(
GX
|
B
)
equals
:
Def3
:
:: CONNSP_3:def 3
p
;
coherence
p
is
Point
of
(
GX
|
B
)
proof
end;
end;
::
deftheorem
Def3
defines
Down
CONNSP_3:def 3 :
for
GX
being
TopStruct
for
B
being
Subset
of
GX
for
p
being
Point
of
GX
st
p
in
B
holds
Down
(
p
,
B
)
=
p
;
definition
let
GX
be
TopStruct
;
let
B
be
Subset
of
GX
;
let
p
be
Point
of
(
GX
|
B
)
;
assume
A1
:
B
<>
{}
;
func
Up
p
->
Point
of
GX
equals
:: CONNSP_3:def 4
p
;
coherence
p
is
Point
of
GX
proof
end;
end;
::
deftheorem
defines
Up
CONNSP_3:def 4 :
for
GX
being
TopStruct
for
B
being
Subset
of
GX
for
p
being
Point
of
(
GX
|
B
)
st
B
<>
{}
holds
Up
p
=
p
;
definition
let
GX
be
TopStruct
;
let
V
,
B
be
Subset
of
GX
;
func
Down
(
V
,
B
)
->
Subset
of
(
GX
|
B
)
equals
:: CONNSP_3:def 5
V
/\
B
;
coherence
V
/\
B
is
Subset
of
(
GX
|
B
)
proof
end;
end;
::
deftheorem
defines
Down
CONNSP_3:def 5 :
for
GX
being
TopStruct
for
V
,
B
being
Subset
of
GX
holds
Down
(
V
,
B
)
=
V
/\
B
;
definition
let
GX
be
TopStruct
;
let
B
be
Subset
of
GX
;
let
V
be
Subset
of
(
GX
|
B
)
;
func
Up
V
->
Subset
of
GX
equals
:: CONNSP_3:def 6
V
;
coherence
V
is
Subset
of
GX
proof
end;
end;
::
deftheorem
defines
Up
CONNSP_3:def 6 :
for
GX
being
TopStruct
for
B
being
Subset
of
GX
for
V
being
Subset
of
(
GX
|
B
)
holds
Up
V
=
V
;
definition
let
GX
be
TopStruct
;
let
B
be
Subset
of
GX
;
let
p
be
Point
of
GX
;
assume
A1
:
p
in
B
;
func
Component_of
(
p
,
B
)
->
Subset
of
GX
means
:
Def7
:
:: CONNSP_3:def 7
for
q
being
Point
of
(
GX
|
B
)
st
q
=
p
holds
it
=
Component_of
q
;
existence
ex
b
1
being
Subset
of
GX
st
for
q
being
Point
of
(
GX
|
B
)
st
q
=
p
holds
b
1
=
Component_of
q
proof
end;
uniqueness
for
b
1
,
b
2
being
Subset
of
GX
st ( for
q
being
Point
of
(
GX
|
B
)
st
q
=
p
holds
b
1
=
Component_of
q
) & ( for
q
being
Point
of
(
GX
|
B
)
st
q
=
p
holds
b
2
=
Component_of
q
) holds
b
1
=
b
2
proof
end;
end;
::
deftheorem
Def7
defines
Component_of
CONNSP_3:def 7 :
for
GX
being
TopStruct
for
B
being
Subset
of
GX
for
p
being
Point
of
GX
st
p
in
B
holds
for
b
4
being
Subset
of
GX
holds
(
b
4
=
Component_of
(
p
,
B
) iff for
q
being
Point
of
(
GX
|
B
)
st
q
=
p
holds
b
4
=
Component_of
q
);
theorem
:: CONNSP_3:26
for
GX
being non
empty
TopSpace
for
B
being
Subset
of
GX
for
p
being
Point
of
GX
st
p
in
B
holds
p
in
Component_of
(
p
,
B
)
proof
end;
theorem
Th27
:
:: CONNSP_3:27
for
GX
being non
empty
TopSpace
for
B
being
Subset
of
GX
for
p
being
Point
of
GX
st
p
in
B
holds
Component_of
(
p
,
B
)
=
Component_of
(
Down
(
p
,
B
)
)
proof
end;
theorem
:: CONNSP_3:28
for
GX
being
TopSpace
for
V
,
B
being
Subset
of
GX
st
V
is
open
holds
Down
(
V
,
B
) is
open
proof
end;
theorem
Th29
:
:: CONNSP_3:29
for
GX
being non
empty
TopSpace
for
V
,
B
being
Subset
of
GX
st
V
c=
B
holds
Cl
(
Down
(
V
,
B
)
)
=
(
Cl
V
)
/\
B
proof
end;
theorem
:: CONNSP_3:30
for
GX
being non
empty
TopSpace
for
B
being
Subset
of
GX
for
V
being
Subset
of
(
GX
|
B
)
holds
Cl
V
=
(
Cl
(
Up
V
)
)
/\
B
proof
end;
theorem
:: CONNSP_3:31
for
GX
being non
empty
TopSpace
for
V
,
B
being
Subset
of
GX
st
V
c=
B
holds
Cl
(
Down
(
V
,
B
)
)
c=
Cl
V
proof
end;
theorem
:: CONNSP_3:32
for
GX
being non
empty
TopSpace
for
B
being
Subset
of
GX
for
V
being
Subset
of
(
GX
|
B
)
st
V
c=
B
holds
Down
(
(
Up
V
)
,
B
)
=
V
by
XBOOLE_1:28
;
theorem
:: CONNSP_3:33
for
GX
being non
empty
TopSpace
for
B
being
Subset
of
GX
for
p
being
Point
of
GX
st
p
in
B
holds
Component_of
(
p
,
B
) is
connected
proof
end;
:: Moved from JORDAN1B, AK, 22.02.2006
registration
let
T
be non
empty
TopSpace
;
cluster
non
empty
for
a_union_of_components
of
T
;
existence
not for
b
1
being
a_union_of_components
of
T
holds
b
1
is
empty
proof
end;
end;
theorem
:: CONNSP_3:34
for
T
being non
empty
TopSpace
for
A
being non
empty
a_union_of_components
of
T
st
A
is
connected
holds
A
is
a_component
proof
end;