Volume 1, 1989

University of Bialystok

Copyright (c) 1989 Association of Mizar Users

### The abstract of the Mizar article:

### Connected Spaces

**by****Beata Padlewska**- Received May 6, 1989
- MML identifier: CONNSP_1

- [ Mizar article, MML identifier index ]

environ vocabulary PRE_TOPC, BOOLE, SUBSET_1, RELAT_2, ORDINAL2, RELAT_1, TOPS_1, SETFAM_1, TARSKI, CONNSP_1; notation TARSKI, XBOOLE_0, SUBSET_1, FUNCT_1, STRUCT_0, PRE_TOPC, TOPS_1; constructors TOPS_1, MEMBERED; clusters PRE_TOPC, RELSET_1, SUBSET_1, MEMBERED, ZFMISC_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; canceled; theorem :: CONNSP_1:2 K,L are_separated implies K misses L; theorem :: CONNSP_1:3 [#]TS = K \/ L & K is closed & L is closed & K misses L implies K,L are_separated; theorem :: CONNSP_1:4 [#]GX = A \/ B & A is open & B is open & A misses B implies A,B are_separated; theorem :: CONNSP_1:5 [#]GX = A \/ B & A,B are_separated implies A is open closed & B is open closed; theorem :: CONNSP_1:6 for X' being SubSpace of GX, P1,Q1 being Subset of GX, P,Q being Subset of X' st P=P1 & Q=Q1 holds P,Q are_separated implies P1,Q1 are_separated; theorem :: CONNSP_1:7 for X' being SubSpace of GX, P,Q being Subset of GX, P1,Q1 being Subset of X' st P=P1 & Q=Q1 & P \/ Q c= [#](X') holds P,Q are_separated implies P1,Q1 are_separated; theorem :: CONNSP_1:8 K,L are_separated & K1 c= K & L1 c= L implies K1,L1 are_separated; theorem :: CONNSP_1:9 A,B are_separated & A,C are_separated implies A,B \/ C are_separated; theorem :: CONNSP_1:10 (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:11 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:12 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:13 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:14 GX is connected iff for A being Subset of GX st A is open closed holds A = {}GX or A = [#]GX; theorem :: CONNSP_1:15 for GY being TopSpace for F being map 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:16 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:17 A is connected & A c= B \/ C & B,C are_separated implies A c= B or A c= C; theorem :: CONNSP_1:18 A is connected & B is connected & not A,B are_separated implies A \/ B is connected; theorem :: CONNSP_1:19 C is connected & C c= A & A c= Cl C implies A is connected; theorem :: CONNSP_1:20 A is connected implies Cl A is connected; theorem :: CONNSP_1:21 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:22 [#]GX \ A = B \/ C & B,C are_separated & A is closed implies A \/ B is closed & A \/ C is closed; theorem :: CONNSP_1:23 C is connected & C meets A & C \ A <> {}GX implies C meets Fr A; theorem :: CONNSP_1:24 for X' being SubSpace of GX, A being Subset of GX, B being Subset of X' st A = B holds A is connected iff B is connected; theorem :: CONNSP_1:25 A is closed & B is closed & A \/ B is connected & A /\ B is connected implies A is connected & B 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) & (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:27 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:28 :: do poprawienia, przy poprawnej definicji "connected" !!! [#]GX is connected iff GX is connected; theorem :: CONNSP_1:29 for GX being non empty TopSpace for x being Point of GX holds {x} is connected; 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:30 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:31 (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:32 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:33 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; pred A is_a_component_of GX 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; theorem :: CONNSP_1:34 for GX being non empty TopSpace, A being Subset of GX st A is_a_component_of GX holds A <> {}GX; theorem :: CONNSP_1:35 A is_a_component_of GX implies A is closed; theorem :: CONNSP_1:36 A is_a_component_of GX & B is_a_component_of GX implies A = B or A,B are_separated; theorem :: CONNSP_1:37 A is_a_component_of GX & B is_a_component_of GX implies A = B or A misses B; theorem :: CONNSP_1:38 C is connected implies for S being Subset of GX st S is_a_component_of GX 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_of GX|A; end; theorem :: CONNSP_1:39 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 skl 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:40 x in skl x; theorem :: CONNSP_1:41 skl x is connected; theorem :: CONNSP_1:42 C is connected & skl x c= C implies C = skl x; theorem :: CONNSP_1:43 A is_a_component_of GX iff ex x being Point of GX st A = skl x; theorem :: CONNSP_1:44 A is_a_component_of GX & x in A implies A = skl x; theorem :: CONNSP_1:45 A = skl x implies for p being Point of GX st p in A holds skl p = A; theorem :: CONNSP_1:46 for F being Subset-Family of GX st for A being Subset of GX holds A in F iff A is_a_component_of GX holds F is_a_cover_of GX;

Back to top