:: Connected Spaces
:: by Beata Padlewska
::
:: Received May 6, 1989
:: Copyright (c) 1990-2018 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
;