:: Components and Unions of Components :: by Yatsuka Nakamura and Andrzej Trybulec :: :: Received February 5, 1996 :: Copyright (c) 1996-2019 Association of Mizar Users :: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland). :: This code can be distributed under the GNU General Public Licence :: version 3.0 or later, or the Creative Commons Attribution-ShareAlike :: License version 3.0 or later, subject to the binding interpretation :: detailed in file COPYING.interpretation. :: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these :: licenses, or see http://www.gnu.org/licenses/gpl.html and :: http://creativecommons.org/licenses/by-sa/3.0/. environ vocabularies XBOOLE_0, PRE_TOPC, SUBSET_1, CONNSP_1, SETFAM_1, RELAT_2, TARSKI, STRUCT_0, ZFMISC_1, RELAT_1, RUSUB_4, RCOMP_1, CONNSP_3; notations TARSKI, XBOOLE_0, SUBSET_1, SETFAM_1, STRUCT_0, PRE_TOPC, CONNSP_1; constructors SETFAM_1, CONNSP_1; registrations SUBSET_1, STRUCT_0, PRE_TOPC, CONNSP_1; requirements SUBSET, BOOLE; begin :: The component of a subset in a topological space reserve x,X,X2,Y,Y2 for set; reserve GX for non empty TopSpace; reserve A2,B2 for Subset of GX; reserve B for Subset of GX; definition let GX be TopStruct, V be Subset of GX; func Component_of V -> Subset of GX means :: 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; end; theorem :: CONNSP_3:1 for GX being TopSpace, 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; theorem :: CONNSP_3:2 for GX being TopSpace, V being Subset of GX st (not ex A being Subset of GX st A is connected & V c= A) holds Component_of V = {}; theorem :: CONNSP_3:3 Component_of {}GX = the carrier of GX; theorem :: CONNSP_3:4 for V being Subset of GX st V is connected holds Component_of V <>{}; theorem :: CONNSP_3:5 for GX being TopSpace, V being Subset of GX st V is connected & V <> {} holds Component_of V is connected; theorem :: CONNSP_3:6 for V,C being Subset of GX st V is connected & C is connected holds Component_of V c= C implies C = Component_of V; theorem :: CONNSP_3:7 for A being Subset of GX st A is a_component holds Component_of A=A; theorem :: CONNSP_3:8 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; theorem :: CONNSP_3:9 for V being Subset of GX st V is connected & V<>{} holds Component_of V is a_component; theorem :: CONNSP_3:10 for A, V be Subset of GX st A is a_component & V is connected & V c= A & V<>{} holds A = Component_of V; theorem :: CONNSP_3:11 for V being Subset of GX st V is connected & V<>{} holds Component_of (Component_of V)=Component_of V; theorem :: CONNSP_3:12 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; theorem :: CONNSP_3:13 for A,B being Subset of GX st A is connected & B is connected & A<>{} & A c= B holds B c= Component_of A; theorem :: CONNSP_3:14 for A being Subset of GX,B being Subset of GX st A is connected & A \/ B is connected & A<>{} holds A \/ B c= Component_of A; theorem :: CONNSP_3:15 for A being Subset of GX, p being Point of GX st A is connected & p in A holds Component_of p=Component_of A; theorem :: CONNSP_3:16 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; theorem :: CONNSP_3:17 for A being Subset of GX st A is connected & A<>{} holds Cl A c= Component_of A; theorem :: CONNSP_3:18 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; begin definition let GX be TopStruct; mode a_union_of_components of GX -> Subset of GX means :: 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; end; theorem :: CONNSP_3:19 {}(GX) is a_union_of_components of GX; theorem :: CONNSP_3:20 for A being Subset of GX st A=(the carrier of GX) holds A is a_union_of_components of GX; theorem :: CONNSP_3:21 for A being Subset of GX,p being Point of GX st p in A & A is a_union_of_components of GX holds Component_of p c= A; theorem :: CONNSP_3:22 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; theorem :: CONNSP_3:23 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; theorem :: CONNSP_3:24 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; theorem :: CONNSP_3:25 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; begin :: Operations Down and Up definition let GX be TopStruct, B be Subset of GX, p be Point of GX; assume p in B; func Down(p,B) -> Point of GX|B equals :: CONNSP_3:def 3 p; end; definition let GX be TopStruct, B be Subset of GX, p be Point of GX|B; assume B<>{}; func Up(p) -> Point of GX equals :: CONNSP_3:def 4 p; end; definition let GX be TopStruct, V,B be Subset of GX; func Down(V,B) -> Subset of GX|B equals :: CONNSP_3:def 5 V /\ B; end; definition let GX be TopStruct, B be Subset of GX; let V be Subset of GX|B; func Up(V) -> Subset of GX equals :: CONNSP_3:def 6 V; end; definition let GX be TopStruct, B be Subset of GX, p be Point of GX; assume p in B; func Component_of(p,B) -> Subset of GX means :: CONNSP_3:def 7 for q being Point of GX| B st q=p holds it=Component_of q; end; theorem :: CONNSP_3:26 for B being Subset of GX, p be Point of GX st p in B holds p in Component_of(p,B); theorem :: CONNSP_3:27 for B being Subset of GX, p be Point of GX st p in B holds Component_of(p,B)=Component_of Down(p,B); 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; theorem :: CONNSP_3:29 for V,B being Subset of GX st V c= B holds Cl Down(V,B) =(Cl V) /\ B; theorem :: CONNSP_3:30 for B being Subset of GX,V being Subset of GX| B holds Cl V =(Cl Up(V) ) /\ B ; theorem :: CONNSP_3:31 for V,B being Subset of GX st V c= B holds Cl Down(V,B) c= Cl V; theorem :: CONNSP_3:32 for B being Subset of GX, V being Subset of GX|B st V c= B holds Down( Up(V),B)=V; theorem :: CONNSP_3:33 for B being Subset of GX, p be Point of GX st p in B holds Component_of(p,B) is connected; :: Moved from JORDAN1B, AK, 22.02.2006 registration let T be non empty TopSpace; cluster non empty for a_union_of_components of T; 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;