:: Locally Connected Spaces
:: by Beata Padlewska
::
:: Received September 5, 1990
:: Copyright (c) 1990-2012 Association of Mizar Users


begin

::
:: A NEIGHBORHOOD OF A POINT
::
definition
let X be non empty TopSpace;
let x be Point of X;
mode a_neighborhood of x ->  Subset of X means :Def1: :: CONNSP_2:def 1
x in Int it;
existence
 ex b1 being Subset of X st x in Int b1
proofend;
end;

:: deftheorem Def1 defines a_neighborhood CONNSP_2:def_1_:_
 for X being non empty TopSpace
for x being Point of X
for b3 being Subset of X holds
( b3 is a_neighborhood of x iff x in Int b3 );

::
:: A NEIGHBORHOOD OF A SET
::
definition
let X be TopSpace;
let A be Subset of X;
mode a_neighborhood of A ->  Subset of X means :Def2: :: CONNSP_2:def 2
A c= Int it;
existence
 ex b1 being Subset of X st A c= Int b1
proofend;
end;

:: deftheorem Def2 defines a_neighborhood CONNSP_2:def_2_:_
 for X being TopSpace
for A, b3 being Subset of X holds
( b3 is a_neighborhood of A iff A c= Int b3 );

theorem :: CONNSP_2:1
for X being non empty TopSpace
for x being Point of X
for A, B being Subset of X st A is a_neighborhood of x & B is a_neighborhood of x holds
A \/ B is a_neighborhood of x
proofend;

theorem :: CONNSP_2:2
for X being non empty TopSpace
for x being Point of X
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 )
proofend;

theorem Th3: :: CONNSP_2:3
for X being non empty TopSpace
for U1 being Subset of X
for x being Point of X st U1 is open & x in U1 holds
U1 is a_neighborhood of x
proofend;

theorem Th4: :: CONNSP_2:4
for X being non empty TopSpace
for U1 being Subset of X
for x being Point of X st U1 is a_neighborhood of x holds
x in U1
proofend;

theorem Th5: :: CONNSP_2:5
for X being non empty TopSpace
for x being Point of X
for U1 being Subset of X st U1 is a_neighborhood of x holds
ex V being non empty Subset of X st
( V is a_neighborhood of x & V is open & V c= U1 )
proofend;

theorem Th6: :: CONNSP_2:6
for X being non empty TopSpace
for x being Point of X
for U1 being Subset of X holds
( U1 is a_neighborhood of x iff ex V being Subset of X st
( V is open & V c= U1 & x in V ) )
proofend;

theorem :: CONNSP_2:7
for X being non empty TopSpace
for U1 being Subset of X holds
( U1 is open iff for x being Point of X st x in U1 holds
ex A being Subset of X st
( A is a_neighborhood of x & A c= U1 ) )
proofend;

theorem :: CONNSP_2:8
for X being non empty TopSpace
for x being Point of X
for V being Subset of X holds
( V is a_neighborhood of {x} iff V is a_neighborhood of x )
proofend;

theorem Th9: :: CONNSP_2:9
for X being non empty TopSpace
for B being non empty Subset of X
for x being Point of (X | B)
for A being Subset of (X | B)
for A1 being Subset of X
for 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
proofend;

Lm1:  for X being non empty TopSpace
for X1 being SubSpace of X
for A being Subset of X
for A1 being Subset of X1 st A = A1 holds
(Int A) /\ ([#] X1) c= Int A1
proofend;

theorem Th10: :: CONNSP_2:10
for X being non empty TopSpace
for B being non empty Subset of X
for x being Point of (X | B)
for A being Subset of (X | B)
for A1 being Subset of X
for x1 being Point of X st A1 is a_neighborhood of x1 & A = A1 & x = x1 holds
A is a_neighborhood of x
proofend;

theorem Th11: :: CONNSP_2:11
for X being non empty TopSpace
for A, B being Subset of X st A is a_component & A c= B holds
A is_a_component_of B
proofend;

theorem :: CONNSP_2:12
for X being non empty TopSpace
for X1 being non empty SubSpace of X
for x being Point of X
for x1 being Point of X1 st x = x1 holds
Component_of x1 c= Component_of x
proofend;

::
:: LOCALLY CONNECTED TOPOLOGICAL SPACES
::
definition
let X be non empty TopSpace;
let x be Point of X;
predX is_locally_connected_in x means :Def3: :: CONNSP_2:def 3
 for U1 being Subset of X st U1 is a_neighborhood of x holds
ex V being Subset of X st
( V is a_neighborhood of x & V is connected & V c= U1 );
end;

:: deftheorem Def3 defines is_locally_connected_in CONNSP_2:def_3_:_
 for X being non empty TopSpace
for x being Point of X holds
( X is_locally_connected_in x iff for U1 being Subset of X st U1 is a_neighborhood of x holds
ex V being Subset of X st
( V is a_neighborhood of x & V is connected & V c= U1 ) );

definition
let X be non empty TopSpace;
attrX is locally_connected  means :Def4: :: CONNSP_2:def 4
 for x being Point of X holds X is_locally_connected_in x;
end;

:: deftheorem Def4 defines locally_connected CONNSP_2:def_4_:_
 for X being non empty TopSpace holds
( X is locally_connected iff for x being Point of X holds X is_locally_connected_in x );

definition
let X be non empty TopSpace;
let A be Subset of X;
let x be Point of X;
predA is_locally_connected_in x means :Def5: :: CONNSP_2:def 5
 for B being non empty Subset of X st A = B holds
ex x1 being Point of (X | B) st
( x1 = x & X | B is_locally_connected_in x1 );
end;

:: deftheorem Def5 defines is_locally_connected_in CONNSP_2:def_5_:_
 for X being non empty TopSpace
for A being Subset of X
for x being Point of X holds
( A is_locally_connected_in x iff for B being non empty Subset of X st A = B holds
ex x1 being Point of (X | B) st
( x1 = x & X | B is_locally_connected_in x1 ) );

definition
let X be non empty TopSpace;
let A be non empty Subset of X;
attrA is locally_connected  means :Def6: :: CONNSP_2:def 6
X | A is locally_connected ;
end;

:: deftheorem Def6 defines locally_connected CONNSP_2:def_6_:_
 for X being non empty TopSpace
for A being non empty Subset of X holds
( A is locally_connected iff X | A is locally_connected );

theorem Th13: :: CONNSP_2:13
for X being non empty TopSpace
for x being Point of 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 )
proofend;

theorem Th14: :: CONNSP_2:14
for X being non empty TopSpace
for x being Point of X holds
( X is_locally_connected_in x iff for U1 being non empty Subset of X st U1 is open & x in U1 holds
ex x1 being Point of (X | U1) st
( x1 = x & x in Int (Component_of x1) ) )
proofend;

theorem Th15: :: CONNSP_2:15
for X being non empty TopSpace st X is locally_connected holds
for S being Subset of X st S is a_component holds
S is open
proofend;

theorem Th16: :: CONNSP_2:16
for X being non empty TopSpace
for x being Point of X st X is_locally_connected_in x holds
for A being non empty Subset of X st A is open & x in A holds
A is_locally_connected_in x
proofend;

theorem Th17: :: CONNSP_2:17
for X being non empty TopSpace st X is locally_connected holds
for A being non empty Subset of X st A is open holds
A is locally_connected
proofend;

theorem Th18: :: CONNSP_2:18
for X being non empty TopSpace holds
( X is locally_connected iff for A being non empty Subset of X
for B being Subset of X st A is open & B is_a_component_of A holds
B is open )
proofend;

theorem :: CONNSP_2:19
for X being non empty TopSpace st X is locally_connected holds
for E being non empty Subset of X
for C being non empty Subset of (X | E) st C is connected & C is open holds
ex H being Subset of X st
( H is open & H is connected & C = E /\ H )
proofend;

theorem Th20: :: CONNSP_2:20
for X being non empty TopSpace holds
( X is normal iff for A, C being Subset of X st A <> {} &amp; C <> [#] X &amp; A c= C &amp; A is closed &amp; C is open holds
ex G being Subset of X st
( G is open &amp; A c= G &amp; Cl G c= C ) )
proofend;

theorem :: CONNSP_2:21
for X being non empty TopSpace st X is locally_connected &amp; X is normal holds
for A, B being Subset of X st A <> {} &amp; B <> {} &amp; A is closed &amp; B is closed &amp; A misses B &amp; A is connected &amp; B is connected holds
ex R, S being Subset of X st
( R is connected &amp; S is connected &amp; R is open &amp; S is open &amp; A c= R &amp; B c= S &amp; R misses S )
proofend;

theorem Th22: :: CONNSP_2:22
for X being non empty TopSpace
for x being Point of X
for F being Subset-Family of X st ( for A being Subset of X holds
( A in F iff ( A is open &amp; A is closed &amp; x in A ) ) ) holds
F <> {}
proofend;

::
:: A QUASICOMPONENT OF A POINT
::
definition
let X be non empty TopSpace;
let x be Point of X;
func qComponent_of x ->  Subset of X means :Def7: :: 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 &amp; A is closed &amp; x in A ) ) ) &amp; meet F = it );
existence
 ex b1 being Subset of X ex F being Subset-Family of X st
( ( for A being Subset of X holds
( A in F iff ( A is open &amp; A is closed &amp; x in A ) ) ) &amp; meet F = b1 )
proofend;
uniqueness
 for b1, b2 being Subset of X st ex F being Subset-Family of X st
( ( for A being Subset of X holds
( A in F iff ( A is open &amp; A is closed &amp; x in A ) ) ) &amp; meet F = b1 ) &amp; ex F being Subset-Family of X st
( ( for A being Subset of X holds
( A in F iff ( A is open &amp; A is closed &amp; x in A ) ) ) &amp; meet F = b2 ) holds
b1 = b2
proofend;
end;

:: deftheorem Def7 defines qComponent_of CONNSP_2:def_7_:_
 for X being non empty TopSpace
for x being Point of X
for b3 being Subset of X holds
( b3 = qComponent_of x iff ex F being Subset-Family of X st
( ( for A being Subset of X holds
( A in F iff ( A is open &amp; A is closed &amp; x in A ) ) ) &amp; meet F = b3 ) );

theorem :: CONNSP_2:23
for X being non empty TopSpace
for x being Point of X holds x in qComponent_of x
proofend;

theorem :: CONNSP_2:24
for X being non empty TopSpace
for x being Point of X
for A being Subset of X st A is open &amp; A is closed &amp; x in A &amp; A c= qComponent_of x holds
A = qComponent_of x
proofend;

theorem :: CONNSP_2:25
for X being non empty TopSpace
for x being Point of X holds qComponent_of x is closed
proofend;

theorem :: CONNSP_2:26
for X being non empty TopSpace
for x being Point of X holds Component_of x c= qComponent_of x
proofend;

:: Moved from YELLOW_6, AG 18.02.2006
theorem :: CONNSP_2:27
for T being non empty TopSpace
for 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 )
proofend;

theorem :: CONNSP_2:28
for X being non empty TopSpace
for A being Subset of X holds [#] X is a_neighborhood of A
proofend;

theorem :: CONNSP_2:29
for X being non empty TopSpace
for A being Subset of X
for Y being a_neighborhood of A holds A c= Y
proofend;