:: 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;