:: Locally Connected Spaces :: by Beata Padlewska :: :: Received September 5, 1990 :: 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 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;