:: Connected Spaces :: by Beata Padlewska :: :: Received May 6, 1989 :: Copyright (c) 1990-2021 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 PRE_TOPC, SUBSET_1, XBOOLE_0, TARSKI, RCOMP_1, RELAT_2, FUNCT_1, ORDINAL2, RELAT_1, STRUCT_0, TOPS_1, SETFAM_1, CONNSP_1; notations TARSKI, XBOOLE_0, SUBSET_1, SETFAM_1, RELSET_1, DOMAIN_1, STRUCT_0, PRE_TOPC, TOPS_1; constructors SETFAM_1, DOMAIN_1, TOPS_1, RELSET_1; registrations XBOOLE_0, SUBSET_1, RELSET_1, STRUCT_0, PRE_TOPC, RELAT_1; requirements SUBSET, BOOLE; begin reserve GX for TopSpace; reserve A, B, C for Subset of GX; reserve TS for TopStruct; reserve K, K1, L, L1 for Subset of TS; :: :: Separated sets :: definition let GX be TopStruct, A,B be Subset of GX; pred A,B are_separated means :: CONNSP_1:def 1 Cl A misses B & A misses Cl B; symmetry; end; theorem :: CONNSP_1:1 K,L are_separated implies K misses L; theorem :: CONNSP_1:2 K is closed & L is closed & K misses L implies K,L are_separated; theorem :: CONNSP_1:3 [#]GX = A \/ B & A is open & B is open & A misses B implies A,B are_separated ; theorem :: CONNSP_1:4 [#]GX = A \/ B & A,B are_separated implies A is open closed & B is open closed; theorem :: CONNSP_1:5 for X9 being SubSpace of GX, P1,Q1 being Subset of GX, P,Q being Subset of X9 st P=P1 & Q=Q1 holds P,Q are_separated implies P1,Q1 are_separated ; theorem :: CONNSP_1:6 for X9 being SubSpace of GX, P,Q being Subset of GX, P1,Q1 being Subset of X9 st P=P1 & Q=Q1 & P \/ Q c= [#](X9) holds P,Q are_separated implies P1,Q1 are_separated; theorem :: CONNSP_1:7 K,L are_separated & K1 c= K & L1 c= L implies K1,L1 are_separated; theorem :: CONNSP_1:8 A,B are_separated & A,C are_separated implies A,B \/ C are_separated; theorem :: CONNSP_1:9 K is closed & L is closed or K is open & L is open implies K \ L, L \ K are_separated; :: :: Connected Spaces :: definition let GX be TopStruct; attr GX is connected means :: CONNSP_1:def 2 for A, B being Subset of GX st [#]GX = A \/ B & A,B are_separated holds A = {}GX or B = {}GX; end; theorem :: CONNSP_1:10 GX is connected iff for A, B being Subset of GX st [#]GX = A \/ B & A <> {}GX & B <> {}GX & A is closed & B is closed holds A meets B; theorem :: CONNSP_1:11 GX is connected iff for A,B being Subset of GX st [#]GX = A \/ B & A <> {}GX & B <> {}GX & A is open & B is open holds A meets B; theorem :: CONNSP_1:12 GX is connected iff for A being Subset of GX st A <> {}GX & A <> [#]GX holds Cl A meets Cl([#]GX \ A); theorem :: CONNSP_1:13 GX is connected iff for A being Subset of GX st A is open closed holds A = {}GX or A = [#]GX; theorem :: CONNSP_1:14 for GY being TopSpace for F being Function of GX,GY st F is continuous & F.:[#]GX = [#]GY & GX is connected holds GY is connected; :: :: Connected Sets :: definition let GX be TopStruct, A be Subset of GX; attr A is connected means :: CONNSP_1:def 3 GX|A is connected; end; theorem :: CONNSP_1:15 A is connected iff for P,Q being Subset of GX st A = P \/ Q & P, Q are_separated holds P = {}GX or Q = {}GX; theorem :: CONNSP_1:16 A is connected & A c= B \/ C & B,C are_separated implies A c= B or A c= C; theorem :: CONNSP_1:17 A is connected & B is connected & not A,B are_separated implies A \/ B is connected; theorem :: CONNSP_1:18 C is connected & C c= A & A c= Cl C implies A is connected; theorem :: CONNSP_1:19 A is connected implies Cl A is connected; theorem :: CONNSP_1:20 GX is connected & A is connected & [#]GX \ A = B \/ C & B,C are_separated implies A \/ B is connected & A \/ C is connected; theorem :: CONNSP_1:21 [#]GX \ A = B \/ C & B,C are_separated & A is closed implies A \/ B is closed & A \/ C is closed; theorem :: CONNSP_1:22 C is connected & C meets A & C \ A <> {}GX implies C meets Fr A; theorem :: CONNSP_1:23 for X9 being SubSpace of GX, A being Subset of GX, B being Subset of X9 st A = B holds A is connected iff B is connected; theorem :: CONNSP_1:24 A is closed & B is closed & A \/ B is connected & A /\ B is connected implies A is connected & B is connected; theorem :: CONNSP_1:25 for F being Subset-Family of GX st (for A being Subset of GX st A in F holds A is connected) & (ex A being Subset of GX st A <> {}GX & A in F & (for B being Subset of GX st B in F & B <> A holds not A,B are_separated)) holds union F is connected; theorem :: CONNSP_1:26 for F being Subset-Family of GX st (for A being Subset of GX st A in F holds A is connected) & meet F <> {}GX holds union F is connected; theorem :: CONNSP_1:27 [#]GX is connected iff GX is connected; registration let GX be non empty TopSpace, x be Point of GX; cluster {x} -> connected for Subset of GX; end; definition let GX be TopStruct, x,y be Point of GX; pred x, y are_joined means :: CONNSP_1:def 4 ex C being Subset of GX st C is connected & x in C & y in C; end; theorem :: CONNSP_1:28 for GX being non empty TopSpace st ex x being Point of GX st for y being Point of GX holds x,y are_joined holds GX is connected; theorem :: CONNSP_1:29 (ex x being Point of GX st for y being Point of GX holds x,y are_joined) iff for x,y being Point of GX holds x,y are_joined; theorem :: CONNSP_1:30 for GX being non empty TopSpace st for x, y being Point of GX holds x, y are_joined holds GX is connected; theorem :: CONNSP_1:31 for GX being non empty TopSpace for x being Point of GX, F being Subset-Family of GX st for A being Subset of GX holds A in F iff A is connected & x in A holds F <> {}; :: :: Components of Topological Spaces :: definition let GX be TopStruct, A be Subset of GX; attr A is a_component means :: CONNSP_1:def 5 A is connected & for B being Subset of GX st B is connected holds A c= B implies A = B; end; registration let GX be TopStruct; cluster a_component -> connected for Subset of GX; end; registration let GX be non empty TopSpace; cluster a_component -> non empty for Subset of GX; end; theorem :: CONNSP_1:32 for GX being non empty TopSpace, A being Subset of GX st A is a_component holds A <> {}GX; registration let GX; cluster a_component -> closed for Subset of GX; end; theorem :: CONNSP_1:33 A is a_component implies A is closed; theorem :: CONNSP_1:34 A is a_component & B is a_component implies A = B or A,B are_separated; theorem :: CONNSP_1:35 A is a_component & B is a_component implies A = B or A misses B; theorem :: CONNSP_1:36 C is connected implies for S being Subset of GX st S is a_component holds C misses S or C c= S; definition let GX be TopStruct, A, B be Subset of GX; pred B is_a_component_of A means :: CONNSP_1:def 6 ex B1 being Subset of GX|A st B1 = B & B1 is a_component; end; theorem :: CONNSP_1:37 GX is connected & A is connected & C is_a_component_of [#]GX \ A implies [#]GX \ C is connected; :: :: A Component of a Point :: definition let GX be TopStruct, x be Point of GX; func Component_of x -> Subset of GX means :: CONNSP_1:def 7 ex F being Subset-Family of GX st (for A being Subset of GX holds A in F iff A is connected & x in A) & union F = it; end; reserve GX for non empty TopSpace; reserve A, C for Subset of GX; reserve x for Point of GX; theorem :: CONNSP_1:38 x in Component_of x; registration let GX,x; cluster Component_of x -> non empty connected; end; theorem :: CONNSP_1:39 C is connected & Component_of x c= C implies C = Component_of x; theorem :: CONNSP_1:40 A is a_component iff ex x being Point of GX st A = Component_of x; theorem :: CONNSP_1:41 A is a_component & x in A implies A = Component_of x; theorem :: CONNSP_1:42 for p being Point of GX st p in Component_of x holds Component_of p = Component_of x; theorem :: CONNSP_1:43 for F being Subset-Family of GX st for A being Subset of GX holds A in F iff A is a_component holds F is Cover of GX; begin :: Addenda, the 2009.03 revision, A.T. registration let T be TopStruct; cluster empty for Subset of T; end; registration let T be TopStruct; cluster empty -> connected for Subset of T; end; theorem :: CONNSP_1:44 for T being TopSpace, X being set holds X is connected Subset of T iff X is connected Subset of the TopStruct of T; theorem :: CONNSP_1:45 for T being TopSpace, X being Subset of T, Y being Subset of the TopStruct of T st X=Y holds X is a_component iff Y is a_component; :: from JORDAN2C, 2011.07.03, A.T. theorem :: CONNSP_1:46 for G being non empty TopSpace, P being Subset of G,A being Subset of G, Q being Subset of G|A st P=Q & P is connected holds Q is connected ;