:: Components and Unions of Components
:: by Yatsuka Nakamura and Andrzej Trybulec
::
:: Received February 5, 1996
:: Copyright (c) 1996-2021 Association of Mizar Users


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 )
proof end;
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
proof end;
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
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;

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 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 ) & b1 = union F )
proof end;
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 ) & b2 = 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;

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 b1 being Subset of GX st
for q being Point of (GX | B) st q = p holds
b1 = Component_of q
proof end;
uniqueness
for b1, b2 being Subset of GX st ( for q being Point of (GX | B) st q = p holds
b1 = Component_of q ) & ( for q being Point of (GX | B) st q = p holds
b2 = Component_of q ) holds
b1 = b2
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 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)
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 b1 being a_union_of_components of T holds b1 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;