:: CONNSP_2 semantic presentation

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

proof end;

end;

:: deftheorem Def1 defines a_neighborhood CONNSP_2:def 1 :

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

proof end;

end;

:: deftheorem Def2 defines a_neighborhood CONNSP_2:def 2 :

theorem :: CONNSP_2:1

canceled;

theorem :: CONNSP_2:2

canceled;

theorem :: CONNSP_2:3

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

proof end;

theorem :: CONNSP_2:4

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 )

proof end;

theorem Th5: :: CONNSP_2:5

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

proof end;

theorem Th6: :: CONNSP_2:6

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

proof end;

theorem Th7: :: CONNSP_2:7

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 )

proof end;

theorem Th8: :: CONNSP_2:8

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

proof end;

theorem :: CONNSP_2:9

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

proof end;

theorem :: CONNSP_2:10

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 )

proof end;

theorem Th11: :: CONNSP_2:11

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

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 Th12: :: CONNSP_2:12

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

proof end;

theorem Th13: :: CONNSP_2:13

for X being non empty TopSpace
for A, B being Subset of X st A is_a_component_of X & A c= B holds
A is_a_component_of B

proof end;

theorem :: CONNSP_2:14

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
skl x1 c= skl x

proof end;

definition

let X be non empty TopSpace;
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 );

end;

:: deftheorem Def3 defines is_locally_connected_in CONNSP_2:def 3 :

definition

let X be non empty TopSpace;
attr X 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 :

definition

let X be non empty TopSpace;
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 );

end;

:: deftheorem Def5 defines is_locally_connected_in CONNSP_2:def 5 :

definition

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

end;

:: deftheorem Def6 defines locally_connected CONNSP_2:def 6 :

theorem :: CONNSP_2:15

canceled;

theorem :: CONNSP_2:16

canceled;

theorem :: CONNSP_2:17

canceled;

theorem :: CONNSP_2:18

canceled;

theorem Th19: :: CONNSP_2:19

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 )

proof end;

theorem Th20: :: CONNSP_2:20

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

proof end;

theorem Th21: :: CONNSP_2:21

for X being non empty TopSpace st X is locally_connected holds
for S being Subset of X st S is_a_component_of X holds
S is open

proof end;

theorem Th22: :: CONNSP_2:22

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

proof end;

theorem Th23: :: CONNSP_2:23

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

proof end;

theorem Th24: :: CONNSP_2:24

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 )

proof end;

theorem :: CONNSP_2:25

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 )

proof end;

theorem Th26: :: CONNSP_2:26

for X being non empty TopSpace holds
( X is_T4 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:27

for X being non empty TopSpace st X is locally_connected & X is_T4 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 )

proof end;

theorem Th28: :: CONNSP_2:28

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 <> {}

proof end;

definition

let X be non empty TopSpace;
let x be Point of X;
func qskl 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

proof end;

uniqueness

proof end;

end;

:: deftheorem Def7 defines qskl CONNSP_2:def 7 :

theorem :: CONNSP_2:29

canceled;

theorem :: CONNSP_2:30

for X being non empty TopSpace
for x being Point of X holds x in qskl x

proof end;

theorem :: CONNSP_2:31

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= qskl x holds
A = qskl x

proof end;

theorem :: CONNSP_2:32

for X being non empty TopSpace
for x being Point of X holds qskl x is closed

proof end;

theorem :: CONNSP_2:33

for X being non empty TopSpace
for x being Point of X holds skl x c= qskl x

proof end;