:: by Beata Padlewska

::

:: Received September 5, 1990

:: Copyright (c) 1990-2012 Association of Mizar Users

begin

definition

let X be non empty TopSpace;

let x be Point of X;

existence

ex b_{1} being Subset of X st x in Int b_{1}

end;
let x be Point of X;

existence

ex b

proof end;

:: deftheorem Def1 defines a_neighborhood CONNSP_2:def 1 :

for X being non empty TopSpace

for x being Point of X

for b_{3} being Subset of X holds

( b_{3} is a_neighborhood of x iff x in Int b_{3} );

for X being non empty TopSpace

for x being Point of X

for b

( b

::

:: A NEIGHBORHOOD OF A SET

::

:: A NEIGHBORHOOD OF A SET

::

definition

let X be TopSpace;

let A be Subset of X;

existence

ex b_{1} being Subset of X st A c= Int b_{1}

end;
let A be Subset of X;

existence

ex b

proof end;

:: deftheorem Def2 defines a_neighborhood CONNSP_2:def 2 :

for X being TopSpace

for A, b_{3} being Subset of X holds

( b_{3} is a_neighborhood of A iff A c= Int b_{3} );

for X being TopSpace

for A, b

( b

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

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

proof end;

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 )

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 )

proof end;

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

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

proof end;

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

for U1 being Subset of X

for x being Point of X st U1 is a_neighborhood of x holds

x in U1

proof end;

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 )

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 )

proof end;

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 ) )

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 ) )

proof end;

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 ) )

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 ) )

proof end;

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 )

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 )

proof end;

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

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

proof end;

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

proof end;

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

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

proof end;

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

for A, B being Subset of X st A is a_component & A c= B holds

A is_a_component_of B

proof end;

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

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

proof end;

::

:: LOCALLY CONNECTED TOPOLOGICAL SPACES

::

:: LOCALLY CONNECTED TOPOLOGICAL SPACES

::

definition

let X be non empty TopSpace;

let x be Point of X;

end;
let x be Point of X;

pred X 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 );

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

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

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;

end;
attr X is locally_connected means :Def4: :: CONNSP_2:def 4

for x being Point of X holds X is_locally_connected_in x;

for x being Point of X holds X is_locally_connected_in x;

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

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;

end;
let A be Subset of X;

let x be Point of X;

pred A 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 );

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

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

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

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

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 )

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 )

proof end;

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) ) )

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) ) )

proof end;

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

for S being Subset of X st S is a_component holds

S is open

proof end;

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

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

proof end;

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

for A being non empty Subset of X st A is open holds

A is locally_connected

proof end;

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 )

( 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 )

proof end;

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 )

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 )

proof end;

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 <> {} & C <> [#] X & A c= C & A is closed & C is open holds

ex G being Subset of X st

( G is open & A c= G & Cl G c= C ) )

( X is normal iff for A, C being Subset of X st A <> {} & C <> [#] X & A c= C & A is closed & C is open holds

ex G being Subset of X st

( G is open & A c= G & Cl G c= C ) )

proof end;

theorem :: CONNSP_2:21

for X being non empty TopSpace st X is locally_connected & X is normal holds

for A, B being Subset of X st A <> {} & B <> {} & A is closed & B is closed & A misses B & A is connected & B is connected holds

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 )

for A, B being Subset of X st A <> {} & B <> {} & A is closed & B is closed & A misses B & A is connected & B is connected holds

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

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 & A is closed & x in A ) ) ) holds

F <> {}

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 & A is closed & x in A ) ) ) holds

F <> {}

proof end;

::

:: A QUASICOMPONENT OF A POINT

::

:: A QUASICOMPONENT OF A POINT

::

definition

let X be non empty TopSpace;

let x be Point of X;

ex b_{1} 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 & A is closed & x in A ) ) ) & meet F = b_{1} )

for b_{1}, b_{2} 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 & A is closed & x in A ) ) ) & meet F = b_{1} ) & ex F being Subset-Family of X st

( ( for A being Subset of X holds

( A in F iff ( A is open & A is closed & x in A ) ) ) & meet F = b_{2} ) holds

b_{1} = b_{2}

end;
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 & A is closed & x in A ) ) ) & meet F = it );

existence ex F being Subset-Family of X st

( ( for A being Subset of X holds

( A in F iff ( A is open & A is closed & x in A ) ) ) & meet F = it );

ex b

( ( for A being Subset of X holds

( A in F iff ( A is open & A is closed & x in A ) ) ) & meet F = b

proof end;

uniqueness for b

( ( for A being Subset of X holds

( A in F iff ( A is open & A is closed & x in A ) ) ) & meet F = b

( ( for A being Subset of X holds

( A in F iff ( A is open & A is closed & x in A ) ) ) & meet F = b

b

proof end;

:: deftheorem Def7 defines qComponent_of CONNSP_2:def 7 :

for X being non empty TopSpace

for x being Point of X

for b_{3} being Subset of X holds

( b_{3} = 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 & A is closed & x in A ) ) ) & meet F = b_{3} ) );

for X being non empty TopSpace

for x being Point of X

for b

( b

( ( for A being Subset of X holds

( A in F iff ( A is open & A is closed & x in A ) ) ) & meet F = b

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 & A is closed & x in A & A c= qComponent_of x holds

A = qComponent_of x

for x being Point of X

for A being Subset of X st A is open & A is closed & x in A & A c= qComponent_of x holds

A = qComponent_of x

proof end;

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

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 )

proof end;

:: A NEIGHBORHOOD OF A POINT

::