:: Locally Connected Spaces
:: by Beata Padlewska
::
:: Received September 5, 1990
:: 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 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;
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
:: CONNSP_2:def 1
x in Int(it);
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
:: CONNSP_2:def 2
A c= Int(it);
end;
reserve X for non empty TopSpace;
reserve x for Point of X;
reserve U1 for Subset of X;
theorem :: CONNSP_2:1
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;
theorem :: CONNSP_2:2
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;
theorem :: CONNSP_2:3
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;
theorem :: CONNSP_2:4
for U1 being Subset of X, x being Point of X st U1 is
a_neighborhood of x holds x in U1;
theorem :: CONNSP_2:5
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;
theorem :: CONNSP_2:6
U1 is a_neighborhood of x iff ex V being Subset of X st V is open
& V c= U1 & x in V;
theorem :: CONNSP_2:7
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;
theorem :: CONNSP_2:8
for V being Subset of X holds V is a_neighborhood of {x} iff V is
a_neighborhood of x;
theorem :: CONNSP_2:9
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;
theorem :: CONNSP_2:10
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;
theorem :: CONNSP_2:11
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;
theorem :: CONNSP_2:12
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;
::
:: LOCALLY CONNECTED TOPOLOGICAL SPACES
::
definition
let X be non empty TopSpace, x be Point of X;
pred X is_locally_connected_in x means
:: CONNSP_2:def 3
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
:: CONNSP_2:def 4
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
:: CONNSP_2:def 5
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
:: CONNSP_2:def 6
X|A is locally_connected;
end;
theorem :: CONNSP_2:13
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;
theorem :: CONNSP_2:14
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);
theorem :: CONNSP_2:15
X is locally_connected implies
for S being Subset of X st S is a_component holds S is open;
theorem :: CONNSP_2:16
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;
theorem :: CONNSP_2:17
X is locally_connected implies for A being non empty Subset of X
st A is open holds A is locally_connected;
theorem :: CONNSP_2:18
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;
theorem :: CONNSP_2:19
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;
theorem :: CONNSP_2:20
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;
theorem :: CONNSP_2:21
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);
theorem :: CONNSP_2:22
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 <> {};
::
:: 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
:: CONNSP_2:def 7
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;
end;
theorem :: CONNSP_2:23
x in qComponent_of x;
theorem :: CONNSP_2:24
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;
theorem :: CONNSP_2:25
qComponent_of x is closed;
theorem :: CONNSP_2:26
Component_of x c= qComponent_of x;
:: Moved from YELLOW_6, AG 18.02.2006
theorem :: CONNSP_2:27
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;
theorem :: CONNSP_2:28
for X be non empty TopSpace, A be Subset of X holds [#]X is
a_neighborhood of A;
theorem :: CONNSP_2:29
for X be non empty TopSpace, A be Subset of X, Y being a_neighborhood
of A holds A c= Y;