:: Connected Spaces
:: by Beata Padlewska
::
:: Received May 6, 1989
:: Copyright (c) 1990-2026 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;
definitions XBOOLE_0;
equalities SUBSET_1, STRUCT_0;
expansions XBOOLE_0;
theorems TARSKI, FUNCT_1, FUNCT_2, ZFMISC_1, SETFAM_1, PRE_TOPC, TOPS_1,
SUBSET_1, RELAT_1, XBOOLE_0, XBOOLE_1, RELSET_1;
schemes SUBSET_1;
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
Cl A misses B & A misses Cl B;
symmetry;
end;
theorem Th1:
K,L are_separated implies K misses L
proof
assume that
A1: (Cl K) /\ L = {} and
K /\ Cl L = {};
K c= Cl K by PRE_TOPC:18;
hence K /\ L = {} by A1,XBOOLE_1:3,27;
end;
theorem Th2:
K is closed & L is closed & K misses L implies K,L are_separated
by PRE_TOPC:22;
theorem Th3:
[#]GX = A \/ B & A is open & B is open & A misses B implies A,B are_separated
proof
assume that
A1: [#]GX = A \/ B and
A2: A is open and
A3: B is open and
A4: A misses B;
A5: Cl([#]GX \ B) = [#]GX \ B by A3,PRE_TOPC:23;
A = [#]GX \ B by A1,A4,PRE_TOPC:5;
then
A6: A is closed by A5,PRE_TOPC:22;
A7: Cl([#]GX \ A) = [#]GX \ A by A2,PRE_TOPC:23;
B = [#]GX \ A by A1,A4,PRE_TOPC:5;
then B is closed by A7,PRE_TOPC:22;
hence thesis by A4,A6,Th2;
end;
theorem Th4:
[#]GX = A \/ B & A,B are_separated implies
A is open closed & B is open closed
proof
assume that
A1: [#]GX = A \/ B and
A2: A,B are_separated;
A3: [#]GX \ B = A by A1,A2,Th1,PRE_TOPC:5;
B c= Cl B by PRE_TOPC:18;
then
A4: A misses Cl B implies Cl B = B by A1,XBOOLE_1:73;
A c= Cl A by PRE_TOPC:18;
then
A5: Cl A misses B implies Cl A = A by A1,XBOOLE_1:73;
B = [#]GX \ A by A1,A2,Th1,PRE_TOPC:5;
hence thesis by A2,A5,A4,A3,PRE_TOPC:22,23;
end;
theorem Th5:
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
proof
let X9 be SubSpace of GX, P1,Q1 be Subset of GX, P,Q be Subset of X9 such
that
A1: P = P1 and
A2: Q = Q1;
reconsider P2 = P, Q2 = Q as Subset of GX by PRE_TOPC:11;
assume that
A3: (Cl P) /\ Q = {} and
A4: P /\ Cl Q = {};
P /\ Cl Q = P /\ (([#] X9) /\ Cl Q2) by PRE_TOPC:17
.= P /\ [#] X9 /\ Cl Q2 by XBOOLE_1:16
.= P2 /\ Cl Q2 by XBOOLE_1:28;
then
A5: P2 misses Cl Q2 by A4;
(Cl P) /\ Q = ((Cl P2) /\ ([#](X9))) /\ Q by PRE_TOPC:17
.= (Cl P2) /\ (Q /\ [#] X9) by XBOOLE_1:16
.= (Cl P2) /\ Q2 by XBOOLE_1:28;
then (Cl P2) misses Q2 by A3;
hence thesis by A1,A2,A5;
end;
theorem Th6:
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
proof
let X9 be SubSpace of GX, P,Q be Subset of GX, P1,Q1 be Subset of X9 such
that
A1: P = P1 and
A2: Q = Q1 and
A3: P \/ Q c= [#](X9);
A4: Q c= P \/ Q by XBOOLE_1:7;
P c= P \/ Q by XBOOLE_1:7;
then reconsider P2 = P, Q2 = Q as Subset of X9 by A3,A4,XBOOLE_1:1;
assume that
A5: (Cl P) /\ Q = {} and
A6: P /\ Cl Q = {};
P2 /\ Cl Q2 = P2 /\ (([#] X9) /\ Cl Q) by PRE_TOPC:17
.= (P2 /\ [#] X9) /\ Cl Q by XBOOLE_1:16
.= P /\ Cl Q by XBOOLE_1:28;
then
A7: P2 misses Cl Q2 by A6;
Cl P2 = (Cl P) /\ [#] X9 by PRE_TOPC:17;
then (Cl P2) /\ Q2 = (Cl P) /\ (Q2 /\ [#] X9) by XBOOLE_1:16
.= (Cl P) /\ Q by XBOOLE_1:28;
then (Cl P2) misses Q2 by A5;
hence thesis by A1,A2,A7;
end;
theorem Th7:
K,L are_separated & K1 c= K & L1 c= L implies K1,L1 are_separated
proof
assume that
A1: (Cl K) /\ L = {} and
A2: K /\ Cl L = {} and
A3: K1 c= K and
A4: L1 c= L;
Cl L1 c= Cl L by A4,PRE_TOPC:19;
then K1 /\ Cl L1 = {}TS by A2,A3,XBOOLE_1:3,27;
then
A5: K1 misses Cl L1;
Cl K1 c= Cl K by A3,PRE_TOPC:19;
then (Cl K1) /\ L1 = {}TS by A1,A4,XBOOLE_1:3,27;
then (Cl K1) misses L1;
hence thesis by A5;
end;
theorem Th8:
A,B are_separated & A,C are_separated implies A,B \/ C are_separated
proof
assume that
A1: (Cl A) misses B and
A2: A misses Cl B and
A3: (Cl A) misses C and
A4: A misses Cl C;
A5: A /\ Cl B = {} by A2;
A /\ Cl (B \/ C) = A /\ ((Cl B) \/ Cl C) by PRE_TOPC:20
.= (A /\ Cl B) \/ (A /\ Cl C) by XBOOLE_1:23
.= {}GX by A4,A5;
then
A6: A misses Cl (B \/ C);
A7: (Cl A) /\ B = {} by A1;
(Cl A) /\ (B \/ C) = ((Cl A) /\ B) \/ ((Cl A) /\ C) by XBOOLE_1:23
.= {}GX by A3,A7;
then (Cl A) misses (B \/ C);
hence thesis by A6;
end;
theorem Th9:
K is closed & L is closed or K is open & L is open implies
K \ L, L \ K are_separated
proof
A1: now
let K,L be Subset of TS such that
A2: K is open and
A3: L is open;
A4: K /\ L` c= K by XBOOLE_1:17;
A5: (Cl L) /\ K` c= K` by XBOOLE_1:17;
Cl([#]TS \ K) = [#]TS \ K by A2,PRE_TOPC:23;
then
A6: (K /\ (L`)) /\ ((Cl L) /\ Cl(K`)) c= K /\ (K`) by A4,A5,XBOOLE_1:27;
A7: K \ L = K /\ (L`) by SUBSET_1:13;
A8: L /\ K` c= L by XBOOLE_1:17;
(Cl K) /\ (L`) c= L` by XBOOLE_1:17;
then
A9: ((Cl K) /\ L`) /\ (L /\ K`) c= L /\ (L`) by A8,XBOOLE_1:27;
L misses L` by XBOOLE_1:79;
then
A10: L /\ L` = {};
K misses K` by XBOOLE_1:79;
then
A11: K /\ K` = {};
[#]TS \ K = K`;
then
A12: ((Cl K) /\ Cl(L`)) /\ (L /\ (K`)) = ((Cl K) /\ (L`)) /\ (L /\ (K`))
by A3,PRE_TOPC:23;
A13: L \ K = L /\ (K`) by SUBSET_1:13;
Cl(L /\ (K`)) c= (Cl L) /\ Cl(K`) by PRE_TOPC:21;
then (K \ L) /\ Cl(L \ K) c= (K /\ (L`)) /\ ((Cl L) /\ Cl(K`)) by A7,A13,
XBOOLE_1:27;
then (K \ L) /\ Cl(L \ K) = {}TS by A11,A6;
then
A14: (K \ L) misses Cl(L \ K);
Cl(K /\ (L`)) c= (Cl K) /\ Cl (L`) by PRE_TOPC:21;
then
(Cl(K \ L)) /\ (L \ K) c= ((Cl K) /\ Cl(L`)) /\ (L /\ (K`)) by A7,A13,
XBOOLE_1:27;
then (Cl(K \ L)) /\ (L \ K) = {}TS by A12,A10,A9;
then (Cl(K \ L)) misses (L \ K);
hence K \ L,L \ K are_separated by A14;
end;
A15: now
let K,L be Subset of TS;
assume that
A16: K is closed and
A17: L is closed;
A18: [#]TS \ L is open by A17,PRE_TOPC:def 3;
A19: ([#]TS \ K) \ ([#]TS \ L) = (K`) /\ (([#]TS \ L)`) by SUBSET_1:13
.= (K`) /\ L by PRE_TOPC:3
.= L \ K by SUBSET_1:13;
A20: ([#]TS \ L) \ ([#]TS \ K) = (L`) /\ (([#]TS \ K)`) by SUBSET_1:13
.= (L`) /\ K by PRE_TOPC:3
.= K \ L by SUBSET_1:13;
[#]TS \ K is open by A16,PRE_TOPC:def 3;
hence K \ L,L \ K are_separated by A1,A18,A20,A19;
end;
assume K is closed & L is closed or K is open & L is open;
hence thesis by A1,A15;
end;
::
:: Connected Spaces
::
definition
let GX be TopStruct;
attr GX is connected means
for A, B being Subset of GX st [#]GX = A \/ B & A,B are_separated holds
A = {}GX or B = {}GX;
end;
theorem Th10:
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
proof
A1: now
assume not GX is connected;
then consider P, Q being Subset of GX such that
A2: [#]GX = P \/ Q and
A3: P,Q are_separated and
A4: P <> {}GX and
A5: Q <> {}GX;
A6: Q is closed by A2,A3,Th4;
P is closed by A2,A3,Th4;
hence
ex A,B being Subset of GX st [#]GX = A \/ B & A <> {}GX & B <> {}GX &
A is closed & B is closed & A misses B by A2,A3,A4,A5,A6,Th1;
end;
(ex A,B being Subset of GX st [#]GX = A \/ B & A <> {}GX & B <> {}GX &
A is closed & B is closed & A misses B)
implies not GX is connected by Th2;
hence thesis by A1;
end;
theorem
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
proof
A1: now
assume not GX is connected;
then consider P,Q being Subset of GX such that
A2: [#]GX = P \/ Q and
A3: P,Q are_separated and
A4: P <> {}GX and
A5: Q <> {}GX;
reconsider P, Q as Subset of GX;
A6: Q is open by A2,A3,Th4;
P is open by A2,A3,Th4;
hence
ex A,B being Subset of GX st [#]GX = A \/ B & A <> {}GX & B <> {}GX &
A is open & B is open & A misses B by A2,A3,A4,A5,A6,Th1;
end;
(ex A,B being Subset of GX st [#]GX = A \/ B & A <> {}GX &
B <> {}GX & A is open & B is open & A misses B)
implies not GX is connected by Th3;
hence thesis by A1;
end;
theorem Th12:
GX is connected iff for A being Subset of GX st A <> {}GX & A <>
[#]GX holds Cl A meets Cl([#]GX \ A)
proof
A1: now
given A being Subset of GX such that
A2: A <> {}GX and
A3: A <> [#]GX and
A4: (Cl A) misses Cl([#]GX \ A);
A5: (Cl A) /\ Cl([#]GX \ A) = {} by A4;
A c= Cl A by PRE_TOPC:18;
then A /\ Cl([#]GX \ A) = {}GX by A5,XBOOLE_1:3,27;
then
A6: A misses Cl([#]GX \ A);
A7: [#]GX = A \/ (A`) by PRE_TOPC:2;
A8: [#]GX \ A <> {}GX by A3,PRE_TOPC:4;
[#]GX \ A c= Cl([#]GX \ A) by PRE_TOPC:18;
then (Cl A) /\ ([#]GX \ A) = {} by A5,XBOOLE_1:3,27;
then (Cl A) misses ([#]GX \ A);
then A,[#]GX \ A are_separated by A6;
hence not GX is connected by A2,A8,A7;
end;
now
assume not GX is connected;
then consider A, B being Subset of GX such that
A9: [#]GX = A \/ B and
A10: A <> {}GX and
A11: B <> {}GX and
A12: A is closed and
A13: B is closed and
A14: A misses B by Th10;
A15: Cl A = A by A12,PRE_TOPC:22;
A16: Cl B = B by A13,PRE_TOPC:22;
A17: B = [#]GX \ A by A9,A14,PRE_TOPC:5;
then A <> [#]GX by A11,PRE_TOPC:4;
hence
ex A being Subset of GX st A <> {}GX & A <> [#]GX & (Cl A) misses Cl(
[#]GX \ A) by A10,A14,A17,A15,A16;
end;
hence thesis by A1;
end;
theorem
GX is connected iff for A being Subset of GX st A is open closed holds
A = {}GX or A = [#]GX
proof
A1: now
assume not GX is connected;
then consider P,Q being Subset of GX such that
A2: [#]GX = P \/ Q and
A3: P,Q are_separated and
A4: P <> {}GX and
A5: Q <> {}GX;
reconsider P, Q as Subset of GX;
Q = [#]GX \ P by A2,A3,Th1,PRE_TOPC:5;
then
A6: P <> [#]GX by A5,PRE_TOPC:4;
P is open closed by A2,A3,Th4;
hence ex P being Subset of GX st P is open closed & P <> {}GX & P <> [#]GX
by A4,A6;
end;
now
given A1 being Subset of GX such that
A7: A1 is open closed and
A8: A1 <> {}GX and
A9: A1 <> [#]GX;
A10: Cl ([#]GX \ A1) = [#]GX \ A1 by A7,PRE_TOPC:23;
A11: A1 misses A1` by XBOOLE_1:79;
Cl A1 = A1 by A7,PRE_TOPC:22;
hence not GX is connected by A8,A9,A10,A11,Th12;
end;
hence thesis by A1;
end;
theorem
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
proof
let GY be TopSpace;
let F be Function of GX,GY such that
A1: F is continuous and
A2: F.:[#]GX = [#]GY and
A3: GX is connected;
assume not GY is connected;
then consider A, B being Subset of GY such that
A4: [#]GY = A \/ B and
A5: A <> {}GY and
A6: B <> {}GY and
A7: A is closed and
A8: B is closed and
A9: A misses B by Th10;
A10: F" A is closed by A1,A7,PRE_TOPC:def 6;
A11: F" B is closed by A1,A8,PRE_TOPC:def 6;
A12: A /\ B = {} by A9;
F" A /\ F" B = F"(A /\ B) by FUNCT_1:68
.= {} by A12;
then
A13: F" A misses F" B;
the carrier of GY is non empty by A5;
then
A14: [#]GX = F"the carrier of GY by FUNCT_2:40
.= F" A \/ F" B by A4,RELAT_1:140;
A15: rng F = F.:(the carrier of GX) by RELSET_1:22;
then
A16: F"B <> {}GX by A2,A6,RELAT_1:139;
F"A <> {}GX by A2,A5,A15,RELAT_1:139;
hence contradiction by A3,A14,A13,A10,A11,A16,Th10;
end;
::
:: Connected Sets
::
definition
let GX be TopStruct, A be Subset of GX;
attr A is connected means
:Def3:
GX|A is connected;
end;
theorem Th15:
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
proof
A1: [#](GX|A) = A by PRE_TOPC:def 5;
A2: now
assume not A is connected;
then not GX|A is connected;
then consider P,Q being Subset of GX|A such that
A3: [#](GX|A) = P \/ Q and
A4: P,Q are_separated and
A5: P <> {}(GX|A) and
A6: Q <> {}(GX|A);
reconsider Q1 = Q as Subset of GX by PRE_TOPC:11;
reconsider P1 = P as Subset of GX by PRE_TOPC:11;
P1,Q1 are_separated by A4,Th5;
hence ex P1,Q1 being Subset of GX st A = P1 \/ Q1 & P1,Q1 are_separated &
P1 <> {}GX & Q1 <> {}GX by A1,A3,A5,A6;
end;
now
given P,Q being Subset of GX such that
A7: A = P \/ Q and
A8: P,Q are_separated and
A9: P <> {}GX and
A10: Q <> {}GX;
reconsider Q1 = Q as Subset of GX|A by A1,A7,XBOOLE_1:7;
reconsider P1 = P as Subset of GX|A by A1,A7,XBOOLE_1:7;
P1,Q1 are_separated by A1,A7,A8,Th6;
then not GX|A is connected by A1,A7,A9,A10;
hence not A is connected;
end;
hence thesis by A2;
end;
theorem Th16:
A is connected & A c= B \/ C & B,C are_separated implies A c= B or A c= C
proof
assume that
A1: A is connected and
A2: A c= B \/ C and
A3: B,C are_separated;
A4: A /\ C c= C by XBOOLE_1:17;
A /\ B c= B by XBOOLE_1:17;
then
A5: A /\ B,A /\ C are_separated by A3,A4,Th7;
A6: (A /\ B) \/ (A /\ C) = A /\ (B \/ C) by XBOOLE_1:23
.= A by A2,XBOOLE_1:28;
assume that
A7: not A c= B and
A8: not A c= C;
A meets C by A2,A7,XBOOLE_1:73;
then
A9: A /\ C <> {};
A meets B by A2,A8,XBOOLE_1:73;
then
A10: A /\ B <> {};
then A <> {}GX;
hence contradiction by A1,A10,A9,A5,A6,Th15;
end;
theorem Th17:
A is connected & B is connected & not A,B are_separated implies
A \/ B is connected
proof
assume that
A1: A is connected and
A2: B is connected and
A3: not A,B are_separated;
assume not A \/ B is connected;
then consider P,Q being Subset of GX such that
A4: A \/ B = P \/ Q and
A5: P,Q are_separated and
A6: P <> {}GX and
A7: Q <> {}GX by Th15;
A8: not(A c= Q & B c= P) by A3,A5,Th7;
P misses Q by A5,Th1;
then
A9: P /\ Q = {};
A10: now
A11: P c= P \/ Q by XBOOLE_1:7;
assume that
A12: A c= P and
A13: B c= P;
A \/ B c= P by A12,A13,XBOOLE_1:8;
then P \/ Q = P by A4,A11;
hence contradiction by A7,A9,XBOOLE_1:7,28;
end;
A14: now
A15: Q c= Q \/ P by XBOOLE_1:7;
assume that
A16: A c= Q and
A17: B c= Q;
A \/ B c= Q by A16,A17,XBOOLE_1:8;
then Q \/ P = Q by A4,A15;
hence contradiction by A6,A9,XBOOLE_1:7,28;
end;
not(A c= P & B c= Q) by A3,A5,Th7;
hence contradiction by A1,A2,A4,A5,A10,A8,A14,Th16,XBOOLE_1:7;
end;
theorem Th18:
C is connected & C c= A & A c= Cl C implies A is connected
proof
assume that
A1: C is connected and
A2: C c= A and
A3: A c= Cl C;
assume not A is connected;
then consider P,Q being Subset of GX such that
A4: A = P \/ Q and
A5: P,Q are_separated and
A6: P <> {}GX and
A7: Q <> {}GX by Th15;
P misses Cl Q by A5;
then
A8: P /\ Cl Q = {};
A9: now
assume C c= Q;
then Cl C c= Cl Q by PRE_TOPC:19;
then P /\ Cl C = {} by A8,XBOOLE_1:3,27;
then P /\ A = {} by A3,XBOOLE_1:3,27;
hence contradiction by A4,A6,XBOOLE_1:21;
end;
(Cl P) misses Q by A5;
then
A10: (Cl P) /\ Q = {};
now
assume C c= P;
then Cl C c= Cl P by PRE_TOPC:19;
then (Cl C) /\ Q = {} by A10,XBOOLE_1:3,27;
then A /\ Q = {} by A3,XBOOLE_1:3,27;
hence contradiction by A4,A7,XBOOLE_1:21;
end;
hence contradiction by A1,A2,A4,A5,A9,Th16;
end;
theorem Th19:
A is connected implies Cl A is connected
proof
A1: A c= Cl A by PRE_TOPC:18;
assume A is connected;
hence thesis by A1,Th18;
end;
theorem Th20:
GX is connected & A is connected & [#]GX \ A = B \/ C & B,C
are_separated implies A \/ B is connected & A \/ C is connected
proof
assume that
A1: GX is connected and
A2: A is connected and
A3: [#]GX \ A = B \/ C and
A4: B,C are_separated;
now
let A,B,C be Subset of GX such that
A5: GX is connected and
A6: A is connected and
A7: [#]GX \ A = B \/ C and
A8: B,C are_separated;
now
let P,Q be Subset of GX such that
A9: A \/ B = P \/ Q and
A10: P,Q are_separated;
A11: [#]GX = A \/ (B \/ C) by A7,XBOOLE_1:45
.= P \/ Q \/ C by A9,XBOOLE_1:4;
A12: now
assume A c= Q;
then P misses A by A10,Th1,Th7;
then P c= B by A9,XBOOLE_1:7,73;
then P,C are_separated by A8,Th7;
then
A13: P,Q \/ C are_separated by A10,Th8;
[#]GX = P \/ (Q \/ C) by A11,XBOOLE_1:4;
hence P = {}GX or Q = {}GX by A5,A13;
end;
now
assume A c= P;
then Q misses A by A10,Th1,Th7;
then Q c= B by A9,XBOOLE_1:7,73;
then Q,C are_separated by A8,Th7;
then
A14: Q,P \/ C are_separated by A10,Th8;
[#]GX = Q \/ (P \/ C) by A11,XBOOLE_1:4;
hence P = {}GX or Q = {}GX by A5,A14;
end;
hence P = {}GX or Q = {}GX by A6,A9,A10,A12,Th16,XBOOLE_1:7;
end;
hence A \/ B is connected by Th15;
end;
hence thesis by A1,A2,A3,A4;
end;
theorem
[#]GX \ A = B \/ C & B,C are_separated & A is closed implies A \/ B is
closed & A \/ C is closed
proof
assume that
A1: [#]GX \ A = B \/ C and
A2: B,C are_separated and
A3: A is closed;
now
let A,B,C be Subset of GX;
assume that
A4: [#]GX \ A = B \/ C and
A5: B,C are_separated and
A6: A is closed;
A7: Cl A = A by A6,PRE_TOPC:22;
(Cl B) misses C by A5;
then
A8: (Cl B) /\ C = {};
A9: [#]GX = A \/ (B \/ C) by A4,XBOOLE_1:45;
Cl(A \/ B) = (Cl A) \/ Cl B by PRE_TOPC:20
.= A \/ ((Cl B) /\ (A \/ (B \/ C))) by A7,A9,XBOOLE_1:28
.= (A \/ Cl B) /\ (A \/ (A \/ (B \/ C))) by XBOOLE_1:24
.= (A \/ Cl B) /\ ((A \/ A) \/ (B \/ C)) by XBOOLE_1:4
.= A \/ ((Cl B) /\ (B \/ C)) by XBOOLE_1:24
.= A \/ (((Cl B) /\ B) \/ ((Cl B) /\ C)) by XBOOLE_1:23
.= A \/ B by A8,PRE_TOPC:18,XBOOLE_1:28;
hence A \/ B is closed by PRE_TOPC:22;
end;
hence thesis by A1,A2,A3;
end;
theorem
C is connected & C meets A & C \ A <> {}GX implies C meets Fr A
proof
assume that
A1: C is connected and
A2: C meets A and
A3: C \ A <> {}GX;
A4: A` c= Cl(A`) by PRE_TOPC:18;
Cl (C /\ A) c= Cl A by PRE_TOPC:19,XBOOLE_1:17;
then
A5: (Cl(C /\ A)) /\ (A`) c= (Cl A) /\ Cl(A`) by A4,XBOOLE_1:27;
A6: A c= Cl A by PRE_TOPC:18;
A7: C \ A = C /\ A` by SUBSET_1:13;
then Cl (C \ A) c= Cl(A`) by PRE_TOPC:19,XBOOLE_1:17;
then A /\ Cl(C /\ (A`)) c= (Cl A) /\ Cl(A`) by A7,A6,XBOOLE_1:27;
then ((Cl(C /\ A)) /\ (A`)) \/ (A /\ Cl(C /\ (A`))) c= (Cl A) /\ Cl(A`) by A5
,XBOOLE_1:8;
then
A8: C /\ (((Cl(C /\ A)) /\ (A`)) \/ (A /\ Cl(C /\ (A`)))) c= C /\ ((Cl A)
/\ Cl(A`)) by XBOOLE_1:27;
A9: C = C /\ [#]GX by XBOOLE_1:28
.= C /\ ( A \/ A`) by PRE_TOPC:2
.= (C /\ A) \/ (C \ A) by A7,XBOOLE_1:23;
C /\ A <> {} by A2;
then not C /\ A,C \ A are_separated by A1,A3,A9,Th15;
then (Cl(C /\ A)) meets (C \ A) or (C /\ A) meets Cl(C \ A);
then
A10: (Cl(C /\ A)) /\ (C \ A) <> {} or (C /\ A) /\ Cl(C \ A) <> {};
((Cl(C /\ A)) /\ (C \ A)) \/ ((C /\ A) /\ Cl(C \ A)) = (((Cl(C /\ A))
/\ C) /\ (A`)) \/ ((C /\ A) /\ Cl(C /\ (A`))) by A7,XBOOLE_1:16
.= ((C /\ Cl(C /\ A)) /\ (A`)) \/ (C /\ (A /\ Cl(C /\ (A`)))) by
XBOOLE_1:16
.= (C /\ ((Cl(C /\ A)) /\ (A`))) \/ (C /\ (A /\ Cl(C /\ (A`)))) by
XBOOLE_1:16
.= C /\ ((Cl(C /\ A) /\ (A`)) \/ (A /\ Cl(C /\ A`))) by XBOOLE_1:23;
then ((Cl(C /\ A)) /\ (C \ A)) \/ ((C /\ A) /\ Cl(C \ A)) c= C /\ Fr A by A8,
TOPS_1:def 2;
hence C /\ Fr A <> {} by A10;
end;
theorem Th23:
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
proof
let X9 be SubSpace of GX, A be Subset of GX, B be Subset of X9;
assume
A1: A = B;
reconsider GX9 = GX, X = X9 as TopSpace;
A2: [#](GX|A) = A by PRE_TOPC:def 5;
reconsider B9 = B as Subset of X;
reconsider A9 = A as Subset of GX9;
A3: [#](X9|B) = B by PRE_TOPC:def 5;
A4: now
assume not A is connected;
then not GX9|A9 is connected;
then consider P,Q being Subset of GX|A such that
A5: [#](GX|A) = P \/ Q and
A6: P <> {}(GX|A) and
A7: Q <> {}(GX|A) and
A8: P is closed and
A9: Q is closed and
A10: P misses Q by Th10;
consider P1 being Subset of GX such that
A11: P1 is closed and
A12: P1 /\ ([#](GX|A)) = P by A8,PRE_TOPC:13;
reconsider P11 = P1 /\ ([#](X9)) as Subset of X9;
A13: P11 is closed by A11,PRE_TOPC:13;
reconsider PP = P, QQ=Q as Subset of X9|B by A1,A2,A3;
A14: P c= [#](X9) by A1,A2,XBOOLE_1:1;
P1 /\ A c= P1 by XBOOLE_1:17;
then P c= P1 /\ ([#](X9)) by A2,A12,A14,XBOOLE_1:19;
then
A15: P c= P1 /\ [#](X9) /\ A by A2,XBOOLE_1:19;
P1 /\ ([#](X9)) c= P1 by XBOOLE_1:17;
then P1 /\ [#](X9) /\ A c= P by A2,A12,XBOOLE_1:27;
then P11 /\ [#](X9|B) = PP by A1,A3,A15;
then
A16: PP is closed by A13,PRE_TOPC:13;
consider Q1 being Subset of GX such that
A17: Q1 is closed and
A18: Q1 /\ ([#](GX|A)) = Q by A9,PRE_TOPC:13;
reconsider Q11 = Q1 /\ ([#](X9)) as Subset of X9;
A19: Q c= [#](X9) by A1,A2,XBOOLE_1:1;
Q1 /\ A c= Q1 by XBOOLE_1:17;
then Q c= Q1 /\ ([#](X9)) by A2,A18,A19,XBOOLE_1:19;
then
A20: Q c= (Q1 /\ ([#](X9))) /\ A by A2,XBOOLE_1:19;
Q1 /\ ([#](X9)) c= Q1 by XBOOLE_1:17;
then (Q1 /\ ([#](X9))) /\ A c= Q by A2,A18,XBOOLE_1:27;
then
A21: (Q1 /\ ([#](X9))) /\ A = Q by A20;
Q11 is closed by A17,PRE_TOPC:13;
then QQ is closed by A1,A3,A21,PRE_TOPC:13;
then not X|B9 is connected by A1,A2,A3,A5,A6,A7,A10,A16,Th10;
hence not B is connected;
end;
now
assume not B is connected;
then not X9|B is connected;
then consider P,Q being Subset of X9|B such that
A22: [#](X9|B) = P \/ Q and
A23: P <> {}(X9|B) and
A24: Q <> {}(X9|B) and
A25: P is closed and
A26: Q is closed and
A27: P misses Q by Th10;
reconsider QQ = Q as Subset of GX|A by A1,A2,A3;
reconsider PP = P as Subset of GX|A by A1,A2,A3;
consider P1 being Subset of X9 such that
A28: P1 is closed and
A29: P1 /\ ([#](X9|B)) = P by A25,PRE_TOPC:13;
consider Q1 being Subset of X9 such that
A30: Q1 is closed and
A31: Q1 /\ ([#](X9|B)) = Q by A26,PRE_TOPC:13;
consider Q2 being Subset of GX such that
A32: Q2 is closed and
A33: Q2 /\ ([#](X9)) = Q1 by A30,PRE_TOPC:13;
Q2 /\ ([#](GX|A)) = Q2 /\ (([#](X9)) /\ B) by A1,A2,XBOOLE_1:28
.= QQ by A3,A31,A33,XBOOLE_1:16;
then
A34: QQ is closed by A32,PRE_TOPC:13;
consider P2 being Subset of GX such that
A35: P2 is closed and
A36: P2 /\ ([#](X9)) = P1 by A28,PRE_TOPC:13;
P2 /\ ([#](GX|A)) = P2 /\ (([#](X9)) /\ B) by A1,A2,XBOOLE_1:28
.= PP by A3,A29,A36,XBOOLE_1:16;
then PP is closed by A35,PRE_TOPC:13;
then not GX9|A9 is connected by A1,A2,A3,A22,A23,A24,A27,A34,Th10;
hence not A is connected;
end;
hence thesis by A4;
end;
theorem
A is closed & B is closed & A \/ B is connected & A /\ B is connected
implies A is connected & B is connected
proof
assume that
A1: A is closed and
A2: B is closed;
set AB = A \/ B;
A3: A \/ B = [#](GX|(A \/ B)) by PRE_TOPC:def 5;
then reconsider B1 = B as Subset of GX|AB by XBOOLE_1:7;
reconsider A1 = A as Subset of GX|AB by A3,XBOOLE_1:7;
A4: [#](GX|(A \/ B)) \ (A1 /\ B1) = (A1 \ B1) \/ (B1 \ A1) by A3,XBOOLE_1:55;
B /\ ([#](GX|(A \/ B))) = B by A3,XBOOLE_1:7,28;
then
A5: B1 is closed by A2,PRE_TOPC:13;
A /\ ([#](GX|(A \/ B))) = A by A3,XBOOLE_1:7,28;
then A1 is closed by A1,PRE_TOPC:13;
then
A6: A1 \ B1,B1 \ A1 are_separated by A5,Th9;
assume that
A7: A \/ B is connected and
A8: A /\ B is connected;
A9: GX|(A \/ B) is connected by A7;
A10: A1 /\ B1 is connected by A8,Th23;
(A1 /\ B1) \/ (B1 \ A1) = B1 by XBOOLE_1:51;
then
A11: B1 is connected by A9,A4,A6,A10,Th20;
(A1 /\ B1) \/ (A1 \ B1) = A1 by XBOOLE_1:51;
then A1 is connected by A9,A4,A6,A10,Th20;
hence thesis by A11,Th23;
end;
theorem Th25:
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
proof
let F be Subset-Family of GX;
assume that
A1: for A being Subset of GX st A in F holds A is connected and
A2: 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;
consider A1 being Subset of GX such that
A1 <> {}GX and
A3: A1 in F and
A4: for B being Subset of GX st B in F & B <> A1 holds not A1,B
are_separated by A2;
reconsider A1 as Subset of GX;
now
let P,Q be Subset of GX;
assume that
A5: union F = P \/ Q and
A6: P,Q are_separated;
P misses Q by A6,Th1;
then
A7: P /\ Q = {};
A8: now
assume
A9: A1 c= Q;
now
let B be Subset of GX;
assume that
A10: B in F and
B <> A1 and
A11: not B c= Q;
B is connected by A1,A10;
then B c= P or B c= Q by A5,A6,A10,Th16,ZFMISC_1:74;
hence contradiction by A4,A6,A9,A10,A11,Th7;
end;
then for A being set st A in F holds A c= Q by A9;
then
A12: union F c= Q by ZFMISC_1:76;
Q c= P \/ Q by XBOOLE_1:7;
then Q = P \/ Q by A5,A12;
hence P = {}GX by A7,XBOOLE_1:7,28;
end;
A13: now
assume
A14: A1 c= P;
now
let B be Subset of GX;
assume that
A15: B in F and
B <> A1;
B is connected by A1,A15;
then
A16: B c= P or B c= Q by A5,A6,A15,Th16,ZFMISC_1:74;
assume not B c= P;
hence contradiction by A4,A6,A14,A15,A16,Th7;
end;
then for A being set st A in F holds A c= P by A14;
then
A17: union F c= P by ZFMISC_1:76;
P c= P \/ Q by XBOOLE_1:7;
then P = P \/ Q by A5,A17;
hence Q = {}GX by A7,XBOOLE_1:7,28;
end;
A1 c= P \/ Q by A3,A5,ZFMISC_1:74;
hence P = {}GX or Q = {}GX by A1,A3,A6,A13,A8,Th16;
end;
hence thesis by Th15;
end;
theorem Th26:
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
proof
let F be Subset-Family of GX;
assume that
A1: for A being Subset of GX st A in F holds A is connected and
A2: meet F <> {}GX;
consider x being Point of GX such that
A3: x in meet F by A2,PRE_TOPC:12;
meet F c= union F by SETFAM_1:2;
then consider A2 being set such that
A4: x in A2 and
A5: A2 in F by A3,TARSKI:def 4;
reconsider A2 as Subset of GX by A5;
A6: now
let B be Subset of GX such that
A7: B in F and
B <> A2;
A2 c= Cl A2 by PRE_TOPC:18;
then x in Cl A2 & x in B or x in A2 & x in Cl B by A3,A4,A7,SETFAM_1:def 1;
then Cl A2 /\ B <> {} or A2 /\ Cl B <> {} by XBOOLE_0:def 4;
then Cl A2 meets B or A2 meets Cl B;
hence not A2,B are_separated;
end;
A2 <> {}GX by A4;
hence thesis by A1,A5,A6,Th25;
end;
theorem Th27:
[#]GX is connected iff GX is connected
proof
A1: [#]GX = [#](GX|[#]GX) by PRE_TOPC:def 5;
A2: now
assume
A3: GX is connected;
now
let P1,Q1 be Subset of GX|([#]GX) such that
A4: [#](GX|[#]GX) = P1 \/ Q1 and
A5: P1,Q1 are_separated;
reconsider Q = Q1 as Subset of GX by PRE_TOPC:11;
reconsider P = P1 as Subset of GX by PRE_TOPC:11;
P,Q are_separated by A5,Th5;
hence P1 = {}(GX|([#]GX)) or Q1 = {}(GX|([#]GX)) by A1,A3,A4;
end;
then GX|([#]GX) is connected;
hence [#]GX is connected;
end;
now
assume [#]GX is connected;
then
A6: GX|[#]GX is connected;
now
let P1,Q1 be Subset of GX such that
A7: [#]GX = P1 \/ Q1 and
A8: P1,Q1 are_separated;
reconsider Q = Q1 as Subset of GX|([#]GX) by A1;
reconsider P = P1 as Subset of (GX|([#]GX)) by A1;
P,Q are_separated by A1,A7,A8,Th6;
hence P1 = {}GX or Q1 = {}GX by A1,A6,A7;
end;
hence GX is connected;
end;
hence thesis by A2;
end;
registration
let GX be non empty TopSpace, x be Point of GX;
cluster {x} -> connected for Subset of GX;
coherence
proof
now
assume not {x} is connected;
then consider P,Q being Subset of GX such that
A1: {x} = P \/ Q and
A2: P,Q are_separated and
A3: P <> {}GX and
A4: Q <> {}GX by Th15;
P <> Q
proof
assume not thesis;
then
A5: P /\ Q = P;
P misses Q by A2,Th1;
hence contradiction by A3,A5;
end;
hence contradiction by A1,A3,A4,ZFMISC_1:38;
end;
hence thesis;
end;
end;
definition
let GX be TopStruct, x,y be Point of GX;
pred x, y are_joined means
:Def4:
ex C being Subset of GX st C is connected & x in C & y in C;
end;
theorem Th28:
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
proof
let GX be non empty TopSpace;
given a being Point of GX such that
A1: for x being Point of GX holds a,x are_joined;
now
let x be Point of GX;
defpred P[set] means ex C1 being Subset of GX st C1 = $1 & C1 is connected
& x in $1;
consider F being Subset-Family of GX such that
A2: for C being Subset of GX holds C in F iff P[C] from SUBSET_1:sch 3;
take F;
let C be Subset of GX;
thus C in F implies C is connected & x in C
proof
assume C in F;
then
ex C1 being Subset of GX st C1 = C & C1 is connected & x in C by A2;
hence thesis;
end;
thus C is connected & x in C implies C in F by A2;
end;
then consider F being Subset-Family of GX such that
A3: for C being Subset of GX holds C in F iff C is connected & a in C;
A4: for x being Point of GX
ex C being Subset of GX st C is connected & a in C & x in C by A1,Def4;
now
let x be object;
assume x in [#]GX;
then consider C being Subset of GX such that
A5: C is connected and
A6: a in C and
A7: x in C by A4;
C in F by A3,A5,A6;
hence x in union F by A7,TARSKI:def 4;
end;
then [#]GX c= union F by TARSKI:def 3;
then
A8: union F = [#]GX;
A9: for A being set st A in F holds a in A by A3;
a in {a} by TARSKI:def 1;
then F <> {} by A3;
then
A10: meet F <> {}GX by A9,SETFAM_1:def 1;
for A being Subset of GX st A in F holds A is connected by A3;
then [#]GX is connected by A8,A10,Th26;
hence thesis by Th27;
end;
theorem Th29:
(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
proof
A1: now
given a being Point of GX such that
A2: for x being Point of GX holds a,x are_joined;
let x,y be Point of GX;
a,x are_joined by A2;
then consider C1 being Subset of GX such that
A3: C1 is connected and
A4: a in C1 and
A5: x in C1;
a,y are_joined by A2;
then consider C2 being Subset of GX such that
A6: C2 is connected and
A7: a in C2 and
A8: y in C2;
C1 /\ C2 <> {}GX by A4,A7,XBOOLE_0:def 4;
then C1 meets C2;
then
A9: C1 \/ C2 is connected by A3,A6,Th1,Th17;
A10: y in C1 \/ C2 by A8,XBOOLE_0:def 3;
x in C1 \/ C2 by A5,XBOOLE_0:def 3;
hence x,y are_joined by A9,A10;
end;
now
set a = the Point of GX;
assume for x,y being Point of GX holds x,y are_joined;
then for y being Point of GX holds a,y are_joined;
hence ex x being Point of GX st for y being Point of GX holds x,y
are_joined;
end;
hence thesis by A1;
end;
theorem
for GX being non empty TopSpace st for x, y being Point of GX holds x,
y are_joined holds GX is connected
proof
let GX be non empty TopSpace;
assume for x,y being Point of GX holds x,y are_joined;
then ex x being Point of GX st for y being Point of GX holds x,y are_joined
by Th29;
hence thesis by Th28;
end;
theorem Th31:
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 <> {}
proof
let GX be non empty TopSpace;
let x be Point of GX, F be Subset-Family of GX such that
A1: for A being Subset of GX holds A in F iff A is connected & x in A;
x in {x} by TARSKI:def 1;
hence thesis by A1;
end;
::
:: Components of Topological Spaces
::
definition
let GX be TopStruct, A be Subset of GX;
attr A is a_component means
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;
coherence;
end;
registration
let GX be non empty TopSpace;
cluster a_component -> non empty for Subset of GX;
coherence
proof
{} c= {the Point of GX} by XBOOLE_1:2;
hence thesis;
end;
end;
theorem
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;
coherence
proof
let A;
A1: A c= Cl A by PRE_TOPC:18;
assume
A2: A is a_component;
then Cl A is connected by Th19;
then A = Cl A by A2,A1;
hence thesis by PRE_TOPC:22;
end;
end;
theorem
A is a_component implies A is closed;
theorem Th34:
A is a_component & B is a_component implies
A = B or A,B are_separated
proof
assume that
A1: A is a_component and
A2: B is a_component;
A <> B implies A,B are_separated
proof
A3: B c= A \/ B by XBOOLE_1:7;
A4: A c= A \/ B by XBOOLE_1:7;
assume
A5: A <> B;
assume not A,B are_separated;
then A \/ B is connected by A1,A2,Th17;
then A = A \/ B by A1,A4;
hence contradiction by A1,A2,A5,A3;
end;
hence thesis;
end;
theorem
A is a_component & B is a_component implies A = B or A misses B by Th1,Th34;
theorem
C is connected implies for S being Subset of GX st S is a_component holds
C misses S or C c= S
proof
assume
A1: C is connected;
let S be Subset of GX;
assume
A2: S is a_component;
A3: S c= C \/ S by XBOOLE_1:7;
assume C meets S;
then C \/ S is connected by A1,A2,Th1,Th17;
then S = C \/ S by A2,A3;
hence thesis by XBOOLE_1:7;
end;
definition
let GX be TopStruct, A, B be Subset of GX;
pred B is_a_component_of A means
ex B1 being Subset of GX|A st B1 = B & B1 is a_component;
end;
theorem
GX is connected & A is connected & C is_a_component_of [#]GX \ A
implies [#]GX \ C is connected
proof
assume that
A1: GX is connected and
A2: A is connected and
A3: C is_a_component_of [#]GX \ A;
consider C1 being Subset of GX|([#]GX \ A) such that
A4: C1 = C and
A5: C1 is a_component by A3;
reconsider C2 = C1 as Subset of GX by A4;
C1 c= [#](GX|([#]GX \ A));
then C1 c= [#]GX \ A by PRE_TOPC:def 5;
then ([#]GX \ A)` c= C2` by SUBSET_1:12;
then
A6: A c= C2` by PRE_TOPC:3;
now
A misses C1 by A6,SUBSET_1:23;
then
A7: A /\ C1 = {};
A8: C is connected by A4,A5,Th23;
let P,Q be Subset of GX such that
A9: [#]GX \ C = P \/ Q and
A10: P,Q are_separated;
A11: P misses P` by XBOOLE_1:79;
A12: P misses Q by A10,Th1;
A13: now
A14: Q misses Q` by XBOOLE_1:79;
assume
A15: A c= Q;
P c= Q` by A12,SUBSET_1:23;
then A /\ P c= Q /\ Q` by A15,XBOOLE_1:27;
then
A16: A /\ P c= {} by A14;
(C \/ P ) /\ A = (A /\ C) \/ (A /\ P) by XBOOLE_1:23
.= {} by A4,A7,A16;
then C \/ P misses A;
then C \/ P c= A` by SUBSET_1:23;
then C \/ P c= [#](GX|([#]GX \ A)) by PRE_TOPC:def 5;
then reconsider C1P1 = C \/ P as Subset of GX|([#]GX \ A);
A17: C misses C` by XBOOLE_1:79;
C \/ P is connected by A1,A9,A10,A8,Th20;
then
A18: C1P1 is connected by Th23;
C c= C1 \/ P by A4,XBOOLE_1:7;
then C1P1 = C1 by A4,A5,A18;
then
A19: P c= C by A4,XBOOLE_1:7;
P c= [#]GX \ C by A9,XBOOLE_1:7;
then P c= C /\ ([#]GX \ C) by A19,XBOOLE_1:19;
then P c= {} by A17;
hence P = {}GX;
end;
A20: Q c= [#]GX \ C by A9,XBOOLE_1:7;
now
assume
A21: A c= P;
Q c= P` by A12,SUBSET_1:23;
then A /\ Q c= P /\ P` by A21,XBOOLE_1:27;
then
A22: A /\ Q c= {} by A11;
(C \/ Q) /\ A = (A /\ C) \/ (A /\ Q) by XBOOLE_1:23
.= {} by A4,A7,A22;
then (C \/ Q) misses A;
then C \/ Q c= A` by SUBSET_1:23;
then C \/ Q c= [#](GX|([#]GX \ A)) by PRE_TOPC:def 5;
then reconsider C1Q1 = C \/ Q as Subset of GX|([#]GX \ A);
C \/ Q is connected by A1,A9,A10,A8,Th20;
then
A23: C1Q1 is connected by Th23;
C1 c= C1 \/ Q by XBOOLE_1:7;
then C1Q1 = C1 by A4,A5,A23;
then Q c= C by A4,XBOOLE_1:7;
then
A24: Q c= C /\ ([#]GX \ C) by A20,XBOOLE_1:19;
C misses C` by XBOOLE_1:79;
then Q c= {} by A24;
hence Q = {}GX;
end;
hence P = {}GX or Q = {}GX by A2,A4,A6,A9,A10,A13,Th16;
end;
hence thesis by Th15;
end;
::
:: A Component of a Point
::
definition
let GX be TopStruct, x be Point of GX;
func Component_of x -> Subset of GX means
:Def7:
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;
existence
proof
defpred P[set] means ex A1 being Subset of GX st A1 = $1 & A1 is connected
& x in $1;
consider F being Subset-Family of GX such that
A1: for A being Subset of GX holds A in F iff P[A] from SUBSET_1:sch 3;
take union F, F;
thus for A being Subset of GX holds A in F iff A is connected & x in A
proof
let A be Subset of GX;
thus A in F implies A is connected & x in A
proof
assume A in F;
then ex A1 being Subset of GX st A1 = A & A1 is connected & x in A by
A1;
hence thesis;
end;
thus thesis by A1;
end;
thus thesis;
end;
uniqueness
proof
let S,S9 be Subset of GX;
assume that
A2: 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 = S and
A3: ex F9 being Subset-Family of GX st (for A being Subset of GX holds
A in F9 iff A is connected & x in A) & union F9 = S9;
consider F being Subset-Family of GX such that
A4: for A being Subset of GX holds A in F iff A is connected & x in A and
A5: union F = S by A2;
consider F9 being Subset-Family of GX such that
A6: for A being Subset of GX holds A in F9 iff A is connected & x in A and
A7: union F9 = S9 by A3;
now
let y be object;
A8: now
assume y in S9;
then consider B being set such that
A9: y in B and
A10: B in F9 by A7,TARSKI:def 4;
reconsider B as Subset of GX by A10;
A11: x in B by A6,A10;
B is connected by A6,A10;
then B in F by A4,A11;
hence y in S by A5,A9,TARSKI:def 4;
end;
now
assume y in S;
then consider B being set such that
A12: y in B and
A13: B in F by A5,TARSKI:def 4;
reconsider B as Subset of GX by A13;
A14: x in B by A4,A13;
B is connected by A4,A13;
then B in F9 by A6,A14;
hence y in S9 by A7,A12,TARSKI:def 4;
end;
hence y in S iff y in S9 by A8;
end;
hence thesis by TARSKI:2;
end;
end;
reserve GX for non empty TopSpace;
reserve A, C for Subset of GX;
reserve x for Point of GX;
theorem Th38:
x in Component_of x
proof
consider F being Subset-Family of GX such that
A1: for A being Subset of GX holds A in F iff A is connected & x in A and
A2: Component_of x = union F by Def7;
A3: for A being set holds A in F implies x in A by A1;
F <> {} by A1,Th31;
then
A4: x in meet F by A3,SETFAM_1:def 1;
meet F c= union F by SETFAM_1:2;
hence thesis by A2,A4;
end;
registration
let GX,x;
cluster Component_of x -> non empty connected;
coherence
proof
consider F being Subset-Family of GX such that
A1: for A being Subset of GX holds A in F iff A is connected & x in A and
A2: Component_of x = union F by Def7;
A3: for A being set holds A in F implies x in A by A1;
F <> {} by A1,Th31;
then
A4: meet F <> {}GX by A3,SETFAM_1:def 1;
for A being Subset of GX st A in F holds A is connected by A1;
hence thesis by A2,A4,Th26,Th38;
end;
end;
theorem Th39:
C is connected & Component_of x c= C implies C = Component_of x
proof
assume
A1: C is connected;
consider F being Subset-Family of GX such that
A2: for A being Subset of GX holds (A in F iff A is connected & x in A) and
A3: Component_of x = union F by Def7;
assume
A4: Component_of x c= C;
x in Component_of x by Th38;
then C in F by A1,A4,A2;
then C c= Component_of x by A3,ZFMISC_1:74;
hence thesis by A4;
end;
theorem Th40:
A is a_component iff ex x being Point of GX st A = Component_of x
proof
hereby
assume
A1: A is a_component;
then A <> {}GX;
then consider y being Point of GX such that
A2: y in A by PRE_TOPC:12;
take x = y;
consider F being Subset-Family of GX such that
A3: for B being Subset of GX holds B in F iff B is connected & x in B and
A4: union F = Component_of x by Def7;
A in F by A1,A2,A3;
then A c= union F by ZFMISC_1:74;
hence A = Component_of x by A1,A4;
end;
given x being Point of GX such that
A5: A = Component_of x;
for B being Subset of GX st B is connected holds A c= B implies A = B
by A5,Th39;
hence A is a_component by A5;
end;
theorem
A is a_component & x in A implies A = Component_of x
proof
assume that
A1: A is a_component and
A2: x in A;
x in Component_of x by Th38;
then A /\ (Component_of x) <> {} by A2,XBOOLE_0:def 4;
then
A3: A meets (Component_of x);
A4: Component_of x is a_component by Th40;
assume A <> Component_of x;
hence contradiction by A1,A3,A4,Th1,Th34;
end;
theorem
for p being Point of GX st p in Component_of x holds
Component_of p = Component_of x
proof
set A = Component_of x;
A1: A is a_component by Th40;
given p being Point of GX such that
A2: p in A and
A3: Component_of p <> A;
Component_of p is a_component by Th40;
then (Component_of p) misses A by A3,A1,Th1,Th34;
then
A4: (Component_of p) /\ A = {}GX;
p in Component_of p by Th38;
hence contradiction by A2,A4,XBOOLE_0:def 4;
end;
theorem
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
proof
let F be Subset-Family of GX such that
A1: for A being Subset of GX holds A in F iff A is a_component;
now
let x be object;
assume x in [#]GX;
then reconsider y = x as Point of GX;
Component_of y is a_component by Th40;
then Component_of y in F by A1;
then
A2: Component_of y c= union F by ZFMISC_1:74;
y in Component_of y by Th38;
hence x in union F by A2;
end;
then [#]GX c= union F by TARSKI:def 3;
hence thesis by SETFAM_1:def 11;
end;
begin :: Addenda, the 2009.03 revision, A.T.
registration
let T be TopStruct;
cluster empty for Subset of T;
existence
proof
take {}T;
thus thesis;
end;
end;
registration
let T be TopStruct;
cluster empty -> connected for Subset of T;
coherence
proof
let C be Subset of T;
assume C is empty;
then reconsider D = C as empty Subset of T;
let A, B be Subset of T|C such that
[#](T|C) = A \/ B and
A,B are_separated;
[#](T|D) = {};
hence thesis;
end;
end;
theorem Th44:
for T being TopSpace, X being set holds
X is connected Subset of T iff X is connected Subset of the TopStruct of T
proof
let T be TopSpace, X be set;
thus X is connected Subset of T implies X is connected Subset of the
TopStruct of T
proof
assume
A1: X is connected Subset of T;
then reconsider X as Subset of T;
reconsider Y=X as Subset of the TopStruct of T;
the TopStruct of T|X = (the TopStruct of T)|Y by PRE_TOPC:36;
then (the TopStruct of T)|Y is connected by A1,Def3;
hence thesis by Def3;
end;
assume
A2: X is connected Subset of the TopStruct of T;
then reconsider X as Subset of the TopStruct of T;
reconsider Y=X as Subset of T;
the TopStruct of T|Y = (the TopStruct of T)|X by PRE_TOPC:36;
then T|Y is connected by A2,Def3;
hence thesis by Def3;
end;
theorem
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
by Th44;
:: from JORDAN2C, 2011.07.03, A.T.
theorem
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
proof
let G be non empty TopSpace,P be Subset of G, A be Subset of G, Q be Subset
of G|A;
assume that
A1: P=Q and
A2: P is connected;
A3: G|P is connected by A2;
Q c= the carrier of G|A;
then Q c= A by PRE_TOPC:8;
then G|P=(G|A) |Q by A1,PRE_TOPC:7;
hence thesis by A3;
end;