:: 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 b1 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 = b1 )
proofend;
uniqueness
 for b1, b2 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 = b1 ) & 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 = b2 ) holds
b1 = b2
proofend;
end;

:: deftheorem Def1 defines Component_of CONNSP_3:def_1_:_
 for GX being TopStruct
for V, b3 being Subset of GX holds
( b3 = 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 = b3 ) );

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
proofend;

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 = {}
proofend;

theorem Th3: :: CONNSP_3:3
for GX being non empty TopSpace holds Component_of ({} GX) = the carrier of GX
proofend;

theorem :: CONNSP_3:4
for GX being non empty TopSpace
for V being Subset of GX st V is connected holds
Component_of V <> {}
proofend;

theorem Th5: :: CONNSP_3:5
for GX being TopSpace
for V being Subset of GX st V is connected &amp; V <> {} holds
Component_of V is connected
proofend;

theorem Th6: :: CONNSP_3:6
for GX being non empty TopSpace
for V, C being Subset of GX st V is connected &amp; C is connected &amp; Component_of V c= C holds
C = Component_of V
proofend;

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
proofend;

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 &amp; V <> {} &amp; A = Component_of V ) )
proofend;

theorem :: CONNSP_3:9
for GX being non empty TopSpace
for V being Subset of GX st V is connected &amp; 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 &amp; V is connected &amp; V c= A &amp; V <> {} holds
A = Component_of V
proofend;

theorem Th11: :: CONNSP_3:11
for GX being non empty TopSpace
for V being Subset of GX st V is connected &amp; V <> {} holds
Component_of (Component_of V) = Component_of V
proofend;

theorem Th12: :: CONNSP_3:12
for GX being non empty TopSpace
for A, B being Subset of GX st A is connected &amp; B is connected &amp; A <> {} &amp; A c= B holds
Component_of A = Component_of B
proofend;

theorem Th13: :: CONNSP_3:13
for GX being non empty TopSpace
for A, B being Subset of GX st A is connected &amp; B is connected &amp; A <> {} &amp; A c= B holds
B c= Component_of A
proofend;

theorem Th14: :: CONNSP_3:14
for GX being non empty TopSpace
for A, B being Subset of GX st A is connected &amp; A \/ B is connected &amp; A <> {} holds
A \/ B c= Component_of A
proofend;

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 &amp; p in A holds
Component_of p = Component_of A
proofend;

theorem :: CONNSP_3:16
for GX being non empty TopSpace
for A, B being Subset of GX st A is connected &amp; B is connected &amp; A meets B holds
( A \/ B c= Component_of A &amp; A \/ B c= Component_of B &amp; A c= Component_of B &amp; B c= Component_of A )
proofend;

theorem :: CONNSP_3:17
for GX being non empty TopSpace
for A being Subset of GX st A is connected &amp; A <> {} holds
Cl A c= Component_of A
proofend;

theorem :: CONNSP_3:18
for GX being non empty TopSpace
for A, B being Subset of GX st A is a_component &amp; B is connected &amp; B <> {} &amp; A misses B holds
A misses Component_of B
proofend;

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_)_&amp;_{}_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 ) &amp; {} 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 ) &amp; {} 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 ) &amp; it = union F );
existence
 ex b1 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 ) &amp; b1 = union F )
proofend;
end;

:: deftheorem Def2 defines a_union_of_components CONNSP_3:def_2_:_
 for GX being TopStruct
for b2 being Subset of GX holds
( b2 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 ) &amp; b2 = union F ) );

theorem Th19: :: CONNSP_3:19
for GX being non empty TopSpace holds {} GX is a_union_of_components of GX
proofend;

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
proofend;

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 &amp; A is a_union_of_components of GX holds
Component_of p c= A
proofend;

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 &amp; B is a_union_of_components of GX holds
( A \/ B is a_union_of_components of GX &amp; A /\ B is a_union_of_components of GX )
proofend;

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
proofend;

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
proofend;

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 &amp; B is a_union_of_components of GX holds
A \ B is a_union_of_components of GX
proofend;

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)
proofend;
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
proofend;
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)
proofend;
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
proofend;
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 b1 being Subset of GX st
for q being Point of (GX | B) st q = p holds
b1 = Component_of q
proofend;
uniqueness
 for b1, b2 being Subset of GX st ( for q being Point of (GX | B) st q = p holds
b1 = Component_of q ) &amp; ( for q being Point of (GX | B) st q = p holds
b2 = Component_of q ) holds
b1 = b2
proofend;
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 b4 being Subset of GX holds
( b4 = Component_of (p,B) iff for q being Point of (GX | B) st q = p holds
b4 = 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)
proofend;

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))
proofend;

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
proofend;

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
proofend;

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
proofend;

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
proofend;

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
proofend;

:: 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 b1 being a_union_of_components of T holds b1 is empty
proofend;
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
proofend;