:: Locally Connected Spaces
:: by Beata Padlewska
::
:: Received September 5, 1990
:: Copyright (c) 1990-2017 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, TOPS_1, TARSKI, RCOMP_1, RELAT_1,
CONNSP_1, RELAT_2, SETFAM_1, CONNSP_2;
notations TARSKI, XBOOLE_0, SUBSET_1, SETFAM_1, DOMAIN_1, STRUCT_0, PRE_TOPC,
TOPS_1, CONNSP_1;
constructors SETFAM_1, DOMAIN_1, TOPS_1, CONNSP_1, COMPTS_1;
registrations XBOOLE_0, SUBSET_1, STRUCT_0, PRE_TOPC, TOPS_1, CONNSP_1;
requirements SUBSET, BOOLE;
definitions TARSKI, COMPTS_1;
equalities SUBSET_1, STRUCT_0;
expansions TARSKI, COMPTS_1;
theorems TARSKI, ZFMISC_1, SETFAM_1, PRE_TOPC, TOPS_1, CONNSP_1, XBOOLE_0,
XBOOLE_1, SUBSET_1;
schemes SUBSET_1;
begin
::
:: A NEIGHBORHOOD OF A POINT
::
definition
let X be non empty TopSpace, x be Point of X;
mode a_neighborhood of x -> Subset of X means
:Def1:
x in Int(it);
existence
proof
take [#] X;
Int([#] X) = [#] X by TOPS_1:15;
hence thesis;
end;
end;
::
:: A NEIGHBORHOOD OF A SET
::
definition
let X be TopSpace,A be Subset of X;
mode a_neighborhood of A -> Subset of X means
:Def2:
A c= Int(it);
existence
proof
take [#] X;
Int([#] X) = [#] X by TOPS_1:15;
hence thesis;
end;
end;
reserve X for non empty TopSpace;
reserve x for Point of X;
reserve U1 for Subset of X;
theorem
for A,B being Subset of X holds A is a_neighborhood of x & B is
a_neighborhood of x implies A \/ B is a_neighborhood of x
proof
let A,B be Subset of X;
reconsider A1 = A, B1 = B as Subset of X;
A1 is a_neighborhood of x & B1 is a_neighborhood of x implies A1 \/ B1
is a_neighborhood of x
proof
assume that
A1: x in Int A1 and
x in Int B1;
A2: Int A1 \/ Int B1 c= Int (A1 \/ B1) by TOPS_1:20;
x in Int A1 \/ Int B1 by A1,XBOOLE_0:def 3;
hence thesis by A2,Def1;
end;
hence thesis;
end;
theorem
for A,B being Subset of X holds A is a_neighborhood of x & B is
a_neighborhood of x iff A /\ B is a_neighborhood of x
proof
let A,B be Subset of X;
A is a_neighborhood of x & B is a_neighborhood of x iff x in Int A & x
in Int B by Def1;
then A is a_neighborhood of x & B is a_neighborhood of x iff x in Int A /\
Int B by XBOOLE_0:def 4;
then
A is a_neighborhood of x & B is a_neighborhood of x iff x in Int (A /\ B
) by TOPS_1:17;
hence thesis by Def1;
end;
theorem Th3:
for U1 being Subset of X, x being Point of X st U1 is open & x in
U1 holds U1 is a_neighborhood of x
proof
let U1 be Subset of X, x be Point of X;
assume U1 is open & x in U1;
then x in Int U1 by TOPS_1:23;
hence thesis by Def1;
end;
theorem Th4:
for U1 being Subset of X, x being Point of X st U1 is
a_neighborhood of x holds x in U1
proof
let U1 be Subset of X, x be Point of X;
assume U1 is a_neighborhood of x;
then
A1: x in Int (U1) by Def1;
Int(U1) c= U1 by TOPS_1:16;
hence thesis by A1;
end;
theorem Th5:
U1 is a_neighborhood of x implies ex V being non empty Subset of
X st V is a_neighborhood of x & V is open & V c= U1
proof
assume U1 is a_neighborhood of x;
then x in Int(U1) by Def1;
then consider V being Subset of X such that
A1: V is open & V c= U1 and
A2: x in V by TOPS_1:22;
reconsider V as non empty Subset of X by A2;
take V;
thus thesis by A1,A2,Th3;
end;
theorem Th6:
U1 is a_neighborhood of x iff ex V being Subset of X st V is open
& V c= U1 & x in V
proof
A1: now
assume U1 is a_neighborhood of x;
then consider V being non empty Subset of X such that
A2: V is a_neighborhood of x & V is open & V c= U1 by Th5;
take V;
thus ex V being Subset of X st V is open & V c= U1 & x in V by A2,Th4;
end;
now
given V being Subset of X such that
A3: V is open & V c= U1 & x in V;
x in Int U1 by A3,TOPS_1:22;
hence U1 is a_neighborhood of x by Def1;
end;
hence thesis by A1;
end;
theorem
for U1 being Subset of X holds U1 is open iff for x st x in U1 ex A
being Subset of X st A is a_neighborhood of x & A c= U1
proof
let U1 be Subset of X;
now
assume
A1: for x st x in U1 ex A being Subset of X st A is a_neighborhood of
x & A c= U1;
for x being set holds x in U1 iff ex V being Subset of X st V is open
& V c= U1 & x in V
proof
let x be set;
thus x in U1 implies ex V being Subset of X st V is open & V c= U1 & x
in V
proof
assume
A2: x in U1;
then reconsider x as Point of X;
consider S being Subset of X such that
A3: S is a_neighborhood of x and
A4: S c= U1 by A1,A2;
consider V being Subset of X such that
A5: V is open & V c= S & x in V by A3,Th6;
take V;
thus thesis by A4,A5;
end;
given V being Subset of X such that
V is open and
A6: V c= U1 & x in V;
thus thesis by A6;
end;
hence U1 is open by TOPS_1:25;
end;
hence thesis by Th3;
end;
theorem
for V being Subset of X holds V is a_neighborhood of {x} iff V is
a_neighborhood of x
proof
let V be Subset of X;
thus V is a_neighborhood of {x} implies V is a_neighborhood of x
proof
assume V is a_neighborhood of {x};
then
A1: {x} c= Int(V) by Def2;
x in {x} by TARSKI:def 1;
hence thesis by A1,Def1;
end;
assume V is a_neighborhood of x;
then x in Int (V) by Def1;
then for p being object holds p in {x} implies p in Int V by TARSKI:def 1;
then {x} c= Int V;
hence thesis by Def2;
end;
theorem Th9:
for B being non empty Subset of X, x being Point of X|B, A being
Subset of X|B, A1 being Subset of X, x1 being Point of X st B is open & A is
a_neighborhood of x & A = A1 & x = x1 holds A1 is a_neighborhood of x1
proof
let B be non empty Subset of X, x be Point of X|B, A be Subset of X|B, A1 be
Subset of X, x1 be Point of X such that
A1: B is open and
A2: A is a_neighborhood of x and
A3: A=A1 & x=x1;
x in Int A by A2,Def1;
then consider Q1 being Subset of X|B such that
A4: Q1 is open and
A5: Q1 c= A & x in Q1 by TOPS_1:22;
Q1 in the topology of X|B by A4,PRE_TOPC:def 2;
then consider Q being Subset of X such that
A6: Q in the topology of X and
A7: Q1 = Q /\ [#](X|B) by PRE_TOPC:def 4;
reconsider Q2 = Q as Subset of X;
Q2 is open by A6,PRE_TOPC:def 2;
then
A8: Q /\ B is open by A1;
Q1 = Q /\ B by A7,PRE_TOPC:def 5;
then x1 in Int A1 by A3,A5,A8,TOPS_1:22;
hence thesis by Def1;
end;
Lm1: for X1 being SubSpace of X, A being Subset of X, A1 being Subset of X1 st
A = A1 holds Int (A) /\ [#](X1) c= Int A1
proof
let X1 be SubSpace of X, A be Subset of X, A1 be Subset of X1;
assume
A1: A = A1;
let p be object;
assume
A2: p in Int (A) /\ [#](X1);
then p in Int (A) by XBOOLE_0:def 4;
then consider Q being Subset of X such that
A3: Q is open and
A4: Q c= A & p in Q by TOPS_1:22;
ex Q1 being Subset of X1 st Q1 is open & Q1 c= A1 & p in Q1
proof
reconsider Q1=Q /\ [#] X1 as Subset of X1;
take Q1;
Q in the topology of X by A3,PRE_TOPC:def 2;
then Q1 c= Q & Q1 in the topology of X1 by PRE_TOPC:def 4,XBOOLE_1:17;
hence thesis by A1,A2,A4,PRE_TOPC:def 2,XBOOLE_0:def 4;
end;
hence thesis by TOPS_1:22;
end;
theorem Th10:
for B being non empty Subset of X, x being Point of X|B, A being
Subset of X|B, A1 being Subset of X, x1 being Point of X st A1 is
a_neighborhood of x1 & A=A1 & x=x1 holds A is a_neighborhood of x
proof
let B be non empty Subset of X, x be Point of X|B, A be Subset of X|B, A1 be
Subset of X, x1 be Point of X such that
A1: A1 is a_neighborhood of x1 and
A2: A=A1 and
A3: x=x1;
x1 in Int A1 by A1,Def1;
then
A4: x1 in Int (A1) /\ [#](X|B) by A3,XBOOLE_0:def 4;
Int (A1) /\ [#](X|B) c= Int A by A2,Lm1;
hence thesis by A3,A4,Def1;
end;
theorem Th11:
for A being Subset of X, B being Subset of X st A is a_component & A c= B
holds A is_a_component_of B
proof
let A be Subset of X,B be Subset of X such that
A1: A is a_component and
A2: A c= B;
A3: A is connected by A1;
ex A1 being Subset of X|B st A=A1 & A1 is a_component
proof
B = [#](X|B) by PRE_TOPC:def 5;
then reconsider C = A as Subset of X|B by A2;
take A1=C;
A4: for D being Subset of X|B st D is connected holds A1 c= D implies A1 = D
proof
let D be Subset of X|B such that
A5: D is connected;
reconsider D1=D as Subset of X by PRE_TOPC:11;
assume
A6: A1 c= D;
D1 is connected by A5,CONNSP_1:23;
hence thesis by A1,A6,CONNSP_1:def 5;
end;
A1 is connected by A3,CONNSP_1:23;
hence thesis by A4,CONNSP_1:def 5;
end;
hence thesis by CONNSP_1:def 6;
end;
theorem
for X1 being non empty SubSpace of X, x being Point of X, x1 being
Point of X1 st x = x1 holds Component_of x1 c= Component_of x
proof
let X1 be non empty SubSpace of X, x be Point of X, x1 be Point of X1;
consider F being Subset-Family of X such that
A1: for A being Subset of X holds A in F iff A is connected & x in A and
A2: union F = Component_of x by CONNSP_1:def 7;
reconsider Z = Component_of x1 as Subset of X by PRE_TOPC:11;
A3: x1 in Z & Z is connected by CONNSP_1:23,38;
assume x = x1;
then Z in F by A1,A3;
hence thesis by A2,ZFMISC_1:74;
end;
::
:: LOCALLY CONNECTED TOPOLOGICAL SPACES
::
definition
let X be non empty TopSpace, x be Point of X;
pred X is_locally_connected_in x means
for U1 being Subset of X st U1
is a_neighborhood of x ex V being Subset of X st V is a_neighborhood of x & V
is connected & V c= U1;
end;
definition
let X be non empty TopSpace;
attr X is locally_connected means
for x being Point of X holds X is_locally_connected_in x;
end;
definition
let X be non empty TopSpace, A be Subset of X, x be Point of X;
pred A is_locally_connected_in x means
for B being non empty Subset
of X st A = B ex x1 being Point of X|B st x1=x & X|B is_locally_connected_in x1
;
end;
definition
let X be non empty TopSpace, A be non empty Subset of X;
attr A is locally_connected means
X|A is locally_connected;
end;
theorem Th13:
for x holds X is_locally_connected_in x iff for V,S being Subset
of X st V is a_neighborhood of x & S is_a_component_of V & x in S holds S is
a_neighborhood of x
proof
let x;
thus X is_locally_connected_in x implies for V,S being Subset of X st V is
a_neighborhood of x & S is_a_component_of V & x in S holds S is a_neighborhood
of x
proof
assume
A1: X is_locally_connected_in x;
let V,S be Subset of X such that
A2: V is a_neighborhood of x and
A3: S is_a_component_of V and
A4: x in S;
reconsider V9 = V as non empty Subset of X by A2,Th4;
consider S1 being Subset of X|V such that
A5: S1=S and
A6: S1 is a_component by A3,CONNSP_1:def 6;
consider V1 being Subset of X such that
A7: V1 is a_neighborhood of x and
A8: V1 is connected and
A9: V1 c= V by A1,A2;
V1 c= [#](X|V) by A9,PRE_TOPC:def 5;
then reconsider V2=V1 as Subset of X|V;
A10: x in Int V1 by A7,Def1;
V2 is connected by A8,CONNSP_1:23;
then V2 misses S1 or V2 c= S1 by A6,CONNSP_1:36;
then
A11: V2 /\ S1 = {}(X|V9) or V2 c= S1 by XBOOLE_0:def 7;
x in V2 by A7,Th4;
then Int V1 c= Int S by A4,A5,A11,TOPS_1:19,XBOOLE_0:def 4;
hence thesis by A10,Def1;
end;
assume
A12: for V,S being Subset of X st V is a_neighborhood of x & S
is_a_component_of V & x in S holds S is a_neighborhood of x;
for U1 being Subset of X st U1 is a_neighborhood of x ex V being Subset
of X st V is a_neighborhood of x & V is connected & V c= U1
proof
let U1 be Subset of X;
A13: [#](X|U1) = U1 by PRE_TOPC:def 5;
assume
A14: U1 is a_neighborhood of x;
then
A15: x in U1 by Th4;
reconsider U1 as non empty Subset of X by A14,Th4;
x in [#](X|U1) by A15,PRE_TOPC:def 5;
then reconsider x1=x as Point of X|U1;
set S1 = Component_of x1;
reconsider S=S1 as Subset of X by PRE_TOPC:11;
take S;
S1 is a_component by CONNSP_1:40;
then
A16: S is_a_component_of U1 by CONNSP_1:def 6;
x in S & S1 is connected by CONNSP_1:38;
hence thesis by A12,A14,A13,A16,CONNSP_1:23;
end;
hence thesis;
end;
theorem Th14:
for x holds X is_locally_connected_in x iff for U1 being non
empty Subset of X st U1 is open & x in U1 ex x1 being Point of X|U1 st x1=x & x
in Int(Component_of x1)
proof
let x;
A1: X is_locally_connected_in x implies for U1 being non empty Subset of X
st U1 is open & x in U1 ex x1 being Point of X|U1 st x1=x & x in Int(
Component_of x1)
proof
assume
A2: X is_locally_connected_in x;
let U1 be non empty Subset of X such that
A3: U1 is open and
A4: x in U1;
x in [#](X|U1) by A4,PRE_TOPC:def 5;
then reconsider x1=x as Point of X|U1;
reconsider S1=Component_of x1 as Subset of X|U1;
take x1;
reconsider S=S1 as Subset of X by PRE_TOPC:11;
A5: x in S by CONNSP_1:38;
S1 is a_component by CONNSP_1:40;
then
A6: S is_a_component_of U1 by CONNSP_1:def 6;
U1 is a_neighborhood of x by A3,A4,Th3;
then S is a_neighborhood of x by A2,A6,A5,Th13;
then S1 is a_neighborhood of x1 by Th10;
hence thesis by Def1;
end;
(for U1 being non empty Subset of X st U1 is open & x in U1 ex x1 being
Point of X|U1 st x1=x & x in Int(Component_of x1)) implies X
is_locally_connected_in x
proof
assume
A7: for U1 being non empty Subset of X st U1 is open & x in U1 ex x1
being Point of X|U1 st x1=x & x in Int(Component_of x1);
for U1 being Subset of X st U1 is a_neighborhood of x ex V1 being
Subset of X st V1 is a_neighborhood of x & V1 is connected & V1 c= U1
proof
let U1 be Subset of X;
assume U1 is a_neighborhood of x;
then consider V being non empty Subset of X such that
A8: V is a_neighborhood of x and
A9: V is open and
A10: V c= U1 by Th5;
consider x1 being Point of X|V such that
A11: x1=x and
A12: x in Int(Component_of x1) by A7,A8,A9,Th4;
set S1=Component_of x1;
reconsider S=S1 as Subset of X by PRE_TOPC:11;
take S;
S1 c= [#](X|V);
then
A13: S1 is connected & S c= V by PRE_TOPC:def 5;
S1 is a_neighborhood of x1 by A11,A12,Def1;
hence thesis by A9,A10,A11,A13,Th9,CONNSP_1:23;
end;
hence thesis;
end;
hence thesis by A1;
end;
theorem Th15:
X is locally_connected implies
for S being Subset of X st S is a_component holds S is open
proof
assume
A1: X is locally_connected;
let S be Subset of X such that
A2: S is a_component;
now
let p be object;
assume
A3: p in S;
then reconsider x=p as Point of X;
A4: [#] X is a_neighborhood of x by Th3;
X is_locally_connected_in x & S is_a_component_of [#] X by A1,A2,Th11;
then S is a_neighborhood of x by A3,A4,Th13;
hence p in Int S by Def1;
end;
then Int(S) c= S & S c= Int S by TOPS_1:16;
then Int S = S by XBOOLE_0:def 10;
hence thesis;
end;
theorem Th16:
X is_locally_connected_in x implies for A being non empty Subset
of X st A is open & x in A holds A is_locally_connected_in x
proof
assume
A1: X is_locally_connected_in x;
let A be non empty Subset of X such that
A2: A is open and
A3: x in A;
reconsider B = A as non empty Subset of X;
A4: [#](X|A) = A by PRE_TOPC:def 5;
for C being non empty Subset of X st B = C ex x1 being Point of X|C st
x1=x & X|C is_locally_connected_in x1
proof
let C be non empty Subset of X;
assume
A5: B = C;
then reconsider y=x as Point of X|C by A3,A4;
take x1=y;
for U1 being Subset of X|B st U1 is a_neighborhood of x1 ex V being
Subset of X|B st V is a_neighborhood of x1 & V is connected & V c= U1
proof
let U1 be Subset of X|B such that
A6: U1 is a_neighborhood of x1;
reconsider U2=U1 as Subset of X by PRE_TOPC:11;
U2 is a_neighborhood of x by A2,A5,A6,Th9;
then consider V being Subset of X such that
A7: V is a_neighborhood of x & V is connected and
A8: V c= U2 by A1;
reconsider V1= V as Subset of X|B by A8,XBOOLE_1:1;
take V1;
thus thesis by A5,A7,A8,Th10,CONNSP_1:23;
end;
hence thesis by A5;
end;
hence thesis;
end;
theorem Th17:
X is locally_connected implies for A being non empty Subset of X
st A is open holds A is locally_connected
proof
assume
A1: X is locally_connected;
let A be non empty Subset of X such that
A2: A is open;
for x being Point of X|A holds X|A is_locally_connected_in x
proof
let x be Point of X|A;
x in [#](X|A);
then
A3: x in A by PRE_TOPC:def 5;
then reconsider x1=x as Point of X;
X is_locally_connected_in x1 by A1;
then A is_locally_connected_in x1 by A2,A3,Th16;
then
ex x2 being Point of X|A st x2=x1 & X|A is_locally_connected_in x2;
hence thesis;
end;
then X|A is locally_connected;
hence thesis;
end;
theorem Th18:
X is locally_connected iff for A being non empty Subset of X, B
being Subset of X st A is open & B is_a_component_of A holds B is open
proof
thus X is locally_connected implies for A being non empty Subset of X, B
being Subset of X st A is open & B is_a_component_of A holds B is open
proof
assume
A1: X is locally_connected;
let A be non empty Subset of X, B be Subset of X such that
A2: A is open and
A3: B is_a_component_of A;
consider B1 being Subset of X|A such that
A4: B1=B and
A5: B1 is a_component by A3,CONNSP_1:def 6;
reconsider B1 as Subset of X|A;
A is locally_connected by A1,A2,Th17;
then X|A is locally_connected;
then B1 is open by A5,Th15;
then B1 in the topology of X|A by PRE_TOPC:def 2;
then consider B2 being Subset of X such that
A6: B2 in the topology of X and
A7: B1 = B2 /\ [#](X|A) by PRE_TOPC:def 4;
A8: B = B2 /\ A by A4,A7,PRE_TOPC:def 5;
reconsider B2 as Subset of X;
B2 is open by A6,PRE_TOPC:def 2;
hence thesis by A2,A8;
end;
assume
A9: for A being non empty Subset of X, B being Subset of X st A is open
& B is_a_component_of A holds B is open;
let x;
for U1 being non empty Subset of X st U1 is open & x in U1 ex x1 being
Point of X|U1 st x1=x & x in Int(Component_of x1)
proof
let U1 be non empty Subset of X such that
A10: U1 is open and
A11: x in U1;
x in [#](X|U1) by A11,PRE_TOPC:def 5;
then reconsider x1=x as Point of X|U1;
set S1=Component_of x1;
reconsider S=S1 as Subset of X by PRE_TOPC:11;
S1 is a_component by CONNSP_1:40;
then S is_a_component_of U1 by CONNSP_1:def 6;
then
A12: S is open by A9,A10;
take x1;
x in S by CONNSP_1:38;
then S1 is a_neighborhood of x1 by A12,Th3,Th10;
hence thesis by Def1;
end;
hence thesis by Th14;
end;
theorem
X is locally_connected implies for E being non empty Subset of X, C
being non empty Subset of X|E st C is connected & C is open ex H being Subset
of X st H is open & H is connected & C = E /\ H
proof
assume
A1: X is locally_connected;
let E be non empty Subset of X, C be non empty Subset of X|E such that
A2: C is connected and
A3: C is open;
C in the topology of X|E by A3,PRE_TOPC:def 2;
then consider G being Subset of X such that
A4: G in the topology of X and
A5: C = G /\ [#](X|E) by PRE_TOPC:def 4;
A6: C = G /\ E by A5,PRE_TOPC:def 5;
reconsider G as non empty Subset of X by A5;
A7: G is open by A4,PRE_TOPC:def 2;
reconsider C1=C as Subset of X by PRE_TOPC:11;
C <> {} (X|E);
then consider x being Point of X|E such that
A8: x in C by PRE_TOPC:12;
x in G by A5,A8,XBOOLE_0:def 4;
then x in [#](X|G) by PRE_TOPC:def 5;
then reconsider y=x as Point of X|G;
set H1 = Component_of y;
reconsider H=H1 as Subset of X by PRE_TOPC:11;
take H;
A9: H1 is a_component by CONNSP_1:40;
then H is_a_component_of G by CONNSP_1:def 6;
hence H is open by A1,A7,Th18;
C c= G by A5,XBOOLE_1:17;
then C c= [#](X|G) by PRE_TOPC:def 5;
then reconsider C2=C1 as Subset of X|G;
H1 c= [#](X|G);
then
A10: H c= G by PRE_TOPC:def 5;
C1 is connected by A2,CONNSP_1:23;
then C2 is connected by CONNSP_1:23;
then C2 misses H or C2 c= H by A9,CONNSP_1:36;
then
A11: C2 /\ H = {}(X|G) or C2 c= H by XBOOLE_0:def 7;
A12: x in H1 by CONNSP_1:38;
H /\ (G /\ E) c= C by A6,XBOOLE_0:def 4;
then (H /\ G) /\ E c= C by XBOOLE_1:16;
then
A13: E /\ H c= C by A10,XBOOLE_1:28;
thus H is connected by CONNSP_1:23;
C c= E by A6,XBOOLE_1:17;
then C c= E /\ H by A8,A11,A12,XBOOLE_0:def 4;
hence thesis by A13,XBOOLE_0:def 10;
end;
theorem Th20:
X is normal iff for A,C being Subset of X st A <> {} & C <> [#]
X & A c= C & A is closed & C is open ex G being Subset of X st G is open & A c=
G & Cl G c= C
proof
thus X is normal implies for A,C being Subset of X st A <> {} & C <> [#] X &
A c= C & A is closed & C is open ex G being Subset of X st G is open & A c= G &
Cl G c= C
proof
assume
A1: for A,B being Subset of X st A <> {} & B <> {} & A is closed & B
is closed & A misses B ex G,H being Subset of X st G is open & H is open & A c=
G & B c= H & G misses H;
let A,C be Subset of X such that
A2: A <> {} and
A3: C <> [#] X and
A4: A c= C and
A5: A is closed and
A6: C is open;
set B=[#](X) \ C;
B c= A` by A4,XBOOLE_1:34;
then
A7: A misses B by SUBSET_1:23;
B <> {} & C` is closed by A3,A6,PRE_TOPC:4;
then consider G,H being Subset of X such that
A8: G is open and
A9: H is open and
A10: A c= G and
A11: B c= H and
A12: G misses H by A1,A2,A5,A7;
take G;
for p being object holds p in Cl G implies p in C
proof
let p be object;
assume
A13: p in Cl G;
then reconsider y=p as Point of X;
H` is closed & G c= H` by A9,A12,SUBSET_1:23;
then
A14: y in H` by A13,PRE_TOPC:15;
H` c= B` by A11,SUBSET_1:12;
then y in B` by A14;
hence thesis by PRE_TOPC:3;
end;
hence thesis by A8,A10;
end;
assume
A15: for A,C being Subset of X st A <> {} & C <> [#] X & A c= C & A is
closed & C is open ex G being Subset of X st G is open & A c= G & Cl G c= C;
for A,B being Subset of X st A <> {} & B <> {} & A is closed & B is
closed & A misses B ex G,H being Subset of X st G is open & H is open & A c= G
& B c= H & G misses H
proof
let A,B be Subset of X such that
A16: A <> {} and
A17: B <> {} and
A18: A is closed and
A19: B is closed & A misses B;
set C = [#] X \ B;
[#] X \ C = B by PRE_TOPC:3;
then
A20: C <> [#] X by A17,PRE_TOPC:4;
A c= B` & C is open by A19,PRE_TOPC:def 3,SUBSET_1:23;
then consider G being Subset of X such that
A21: G is open and
A22: A c= G and
A23: Cl G c= C by A15,A16,A18,A20;
take G;
take H = [#] X \ Cl G;
thus G is open & H is open by A21,PRE_TOPC:def 3;
C` c= (Cl G)` by A23,SUBSET_1:12;
hence A c= G & B c= H by A22,PRE_TOPC:3;
H c= G` by PRE_TOPC:18,XBOOLE_1:34;
hence thesis by SUBSET_1:23;
end;
hence thesis;
end;
theorem
X is locally_connected & X is normal implies for A,B being Subset of X
st A <> {} & B <> {} & A is closed & B is closed & A misses B holds (A is
connected & B is connected implies ex R,S being Subset of X st R is connected &
S is connected & R is open & S is open & A c= R & B c= S & R misses S)
proof
assume that
A1: X is locally_connected and
A2: X is normal;
let A,B be Subset of X such that
A3: A <> {} and
A4: B <> {} and
A5: A is closed and
A6: B is closed & A misses B;
B = [#] X \ ([#] X \ B) by PRE_TOPC:3;
then
A7: [#] X \ B <> [#] X by A4,PRE_TOPC:4;
A <> {} X by A3;
then consider x being Point of X such that
A8: x in A by PRE_TOPC:12;
A c= B` & B` is open by A6,SUBSET_1:23;
then consider G being Subset of X such that
A9: G is open and
A10: A c= G and
A11: Cl G c= B` by A2,A3,A5,A7,Th20;
A12: Cl G misses B by A11,SUBSET_1:23;
A13: x in G by A10,A8;
reconsider G as non empty Subset of X by A3,A10;
x in [#](X|G) by A13,PRE_TOPC:def 5;
then reconsider y=x as Point of X|G;
A14: Cl G misses (Cl G)` by XBOOLE_1:79;
assume that
A15: A is connected and
A16: B is connected;
set H=Component_of y;
reconsider H1=H as Subset of X by PRE_TOPC:11;
take R=H1;
A17: H is a_component by CONNSP_1:40;
then
A18: H1 is_a_component_of G by CONNSP_1:def 6;
A c= [#](X|G) by A10,PRE_TOPC:def 5;
then reconsider A1=A as Subset of X|G;
A19: H is connected & y in H by CONNSP_1:38;
A1 is connected by A15,CONNSP_1:23;
then A1 misses H or A1 c= H by A17,CONNSP_1:36;
then
A20: A1 /\ H = {} or A1 c= H by XBOOLE_0:def 7;
H c= [#](X|G);
then
A21: R c= G by PRE_TOPC:def 5;
G c= Cl G by PRE_TOPC:18;
then
A22: R c= Cl G by A21;
B <> {} X by A4;
then consider z being Point of X such that
A23: z in B by PRE_TOPC:12;
A24: B c= (Cl G)` by A12,SUBSET_1:23;
then reconsider C = (Cl G)` as non empty Subset of X by A23;
z in (Cl G)` by A23,A24;
then z in [#](X|C) by PRE_TOPC:def 5;
then reconsider z1=z as Point of X|C;
set V=Component_of z1;
reconsider V1=V as Subset of X by PRE_TOPC:11;
take S=V1;
A25: V is a_component by CONNSP_1:40;
B c= [#](X|(Cl G)`) by A24,PRE_TOPC:def 5;
then reconsider B1=B as Subset of X|(Cl G)`;
A26: V is connected & z1 in V by CONNSP_1:38;
B1 is connected by A16,CONNSP_1:23;
then B1 misses V or B1 c= V by A25,CONNSP_1:36;
then
A27: B1 /\ V = {} or B1 c= V by XBOOLE_0:def 7;
V c= [#](X|(Cl G)`);
then S c= (Cl G)` by PRE_TOPC:def 5;
then R /\ S c= Cl G /\ (Cl G)` by A22,XBOOLE_1:27;
then R /\ S c= {} X by A14,XBOOLE_0:def 7;
then
A28: R /\ S = {};
V1 is_a_component_of (Cl G)` by A25,CONNSP_1:def 6;
hence thesis by A1,A9,A8,A18,A20,A19,A23,A27,A26,A28,Th18,CONNSP_1:23
,XBOOLE_0:def 4,def 7;
end;
theorem Th22:
for x being Point of X, F being Subset-Family of X st for A
being Subset of X holds A in F iff A is open closed & x in A holds F <> {}
proof
A1: [#] X is open closed;
let x be Point of X, F be Subset-Family of X;
assume for A being Subset of X holds A in F iff A is open closed & x in A;
hence thesis by A1;
end;
::
:: A QUASICOMPONENT OF A POINT
::
definition
let X be non empty TopSpace, x be Point of X;
func qComponent_of x -> Subset of X means
:Def7:
ex F being Subset-Family of
X st (for A being Subset of X holds A in F iff A is open closed & x in A) &
meet F = it;
existence
proof
defpred P[set] means ex A1 being Subset of X st A1 = $1 & A1 is open
closed & x in $1;
consider F being Subset-Family of X such that
A1: for A being Subset of X holds A in F iff P[A] from SUBSET_1:sch 3;
reconsider S = meet F as Subset of X;
take S, F;
thus for A being Subset of X holds A in F iff A is open closed & x in A
proof
let A be Subset of X;
thus A in F implies A is open closed & x in A
proof
assume A in F;
then
ex A1 being Subset of X st A1 = A & A1 is open closed & x in A by A1;
hence thesis;
end;
thus thesis by A1;
end;
thus thesis;
end;
uniqueness
proof
let S,S9 be Subset of X;
assume that
A2: ex F being Subset-Family of X st (for A being Subset of X holds A
in F iff A is open closed & x in A) & meet F = S and
A3: ex F9 being Subset-Family of X st (for A being Subset of X holds
A in F9 iff A is open closed & x in A) & meet F9 = S9;
consider F being Subset-Family of X such that
A4: for A being Subset of X holds A in F iff A is open closed & x in A and
A5: meet F = S by A2;
consider F9 being Subset-Family of X such that
A6: for A being Subset of X holds A in F9 iff A is open closed & x in A and
A7: meet F9 = S9 by A3;
A8: F9 <> {} by A6,Th22;
A9: F <> {} by A4,Th22;
now
let y be object;
A10: now
assume
A11: y in S9;
for B being set st B in F holds y in B
proof
let B be set;
assume
A12: B in F;
then reconsider B1=B as Subset of X;
B1 is open closed & x in B1 by A4,A12;
then B1 in F9 by A6;
hence thesis by A7,A11,SETFAM_1:def 1;
end;
hence y in S by A5,A9,SETFAM_1:def 1;
end;
now
assume
A13: y in S;
for B being set st B in F9 holds y in B
proof
let B be set;
assume
A14: B in F9;
then reconsider B1=B as Subset of X;
B1 is open closed & x in B1 by A6,A14;
then B1 in F by A4;
hence thesis by A5,A13,SETFAM_1:def 1;
end;
hence y in S9 by A7,A8,SETFAM_1:def 1;
end;
hence y in S iff y in S9 by A10;
end;
hence thesis by TARSKI:2;
end;
end;
theorem
x in qComponent_of x
proof
consider F being Subset-Family of X such that
A1: for A being Subset of X holds A in F iff A is open closed & x in A and
A2: qComponent_of x = meet F by Def7;
F <> {} & for A being set holds A in F implies x in A by A1,Th22;
hence thesis by A2,SETFAM_1:def 1;
end;
theorem
for A being Subset of X st A is open closed & x in A holds A c=
qComponent_of x implies A = qComponent_of x
proof
let A be Subset of X;
consider F being Subset-Family of X such that
A1: for A being Subset of X holds (A in F iff A is open closed & x in A) and
A2: qComponent_of x = meet F by Def7;
assume A is open closed & x in A;
then A in F by A1;
then
A3: qComponent_of x c= A by A2,SETFAM_1:3;
assume A c= qComponent_of x;
hence thesis by A3,XBOOLE_0:def 10;
end;
theorem
qComponent_of x is closed
proof
consider F being Subset-Family of X such that
A1: for A being Subset of X holds (A in F iff A is open closed & x in A) and
A2: qComponent_of x = meet F by Def7;
for A being Subset of X st A in F holds A is closed by A1;
hence thesis by A2,PRE_TOPC:14;
end;
theorem
Component_of x c= qComponent_of x
proof
consider F9 being Subset-Family of X such that
A1: for A being Subset of X holds (A in F9 iff A is open closed & x in A ) and
A2: qComponent_of x = meet F9 by Def7;
A3: for B1 being set st B1 in F9 holds Component_of x c= B1
proof
set S=Component_of x;
let B1 be set;
A4: x in S by CONNSP_1:38;
assume
A5: B1 in F9;
then reconsider B=B1 as Subset of X;
A6: x in B by A1,A5;
A7: B is open closed by A1,A5;
then B` is closed;
then Cl B` = B` by PRE_TOPC:22;
then
A8: B misses Cl B` by XBOOLE_1:79;
A9: S /\ B c= B & S /\ B` c= B` by XBOOLE_1:17;
Cl B = B by A7,PRE_TOPC:22;
then Cl B misses B` by XBOOLE_1:79;
then B,B` are_separated by A8,CONNSP_1:def 1;
then
A10: S /\ B,S /\ B` are_separated by A9,CONNSP_1:7;
A11: [#] X = B \/ B` by PRE_TOPC:2;
S = S /\ [#] X by XBOOLE_1:28
.= (S /\ B) \/ (S /\ B`) by A11,XBOOLE_1:23;
then S /\ B = {}X or S /\ B` = {}X by A10,CONNSP_1:15;
then S misses B` by A6,A4,XBOOLE_0:def 4,def 7;
then S c= B`` by SUBSET_1:23;
hence thesis;
end;
F9 <> {} by A1,Th22;
hence thesis by A2,A3,SETFAM_1:5;
end;
:: Moved from YELLOW_6, AG 18.02.2006
theorem
for T being non empty TopSpace, A being Subset of T for p being Point
of T holds p in Cl A iff for G being a_neighborhood of p holds G meets A
proof
let T be non empty TopSpace, A be Subset of T;
let p be Point of T;
hereby
assume
A1: p in Cl A;
let G be a_neighborhood of p;
p in Int G & Int G is open by Def1;
then A meets Int G by A1,PRE_TOPC:def 7;
hence G meets A by TOPS_1:16,XBOOLE_1:63;
end;
assume
A2: for G being a_neighborhood of p holds G meets A;
now
let G be Subset of T;
assume G is open & p in G;
then G is a_neighborhood of p by Th3;
hence A meets G by A2;
end;
hence thesis by PRE_TOPC:def 7;
end;
theorem
for X be non empty TopSpace, A be Subset of X holds [#]X is
a_neighborhood of A
proof
let X be non empty TopSpace, A be Subset of X;
Int [#]X = [#]X by TOPS_1:15;
hence A c= Int [#]X;
end;
theorem
for X be non empty TopSpace, A be Subset of X, Y being a_neighborhood
of A holds A c= Y
proof
let X be non empty TopSpace, A be Subset of X, Y be a_neighborhood of A;
A c= Int Y & Int Y c= Y by Def2,TOPS_1:16;
hence thesis;
end;