:: CONNSP_2 semantic presentation

definition

let c₁ be non empty TopSpace;
let c₂ be Point of c₁;
mode a_neighborhood of c₂ -> Subset of a₁ means :Def1: :: CONNSP_2:def 1
a₂ in Int a₃;
existence

proof end;

end;

:: deftheorem Def1 defines a_neighborhood CONNSP_2:def 1 :

definition

let c₁ be TopSpace;
let c₂ be Subset of c₁;
mode a_neighborhood of c₂ -> Subset of a₁ means :Def2: :: CONNSP_2:def 2
a₂ c= Int a₃;
existence

proof end;

end;

:: deftheorem Def2 defines a_neighborhood CONNSP_2:def 2 :

theorem Th1: :: CONNSP_2:1

canceled;

theorem Th2: :: CONNSP_2:2

canceled;

theorem Th3: :: CONNSP_2:3

for b₁ being non empty TopSpace
for b₂ being Point of b₁
for b₃, b₄ being Subset of b₁ st b₃ is a_neighborhood of b₂ & b₄ is a_neighborhood of b₂ holds
b₃ \/ b₄ is a_neighborhood of b₂

proof end;

theorem Th4: :: CONNSP_2:4

for b₁ being non empty TopSpace
for b₂ being Point of b₁
for b₃, b₄ being Subset of b₁ holds
( ( b₃ is a_neighborhood of b₂ & b₄ is a_neighborhood of b₂ ) iff b₃ /\ b₄ is a_neighborhood of b₂ )

proof end;

theorem Th5: :: CONNSP_2:5

for b₁ being non empty TopSpace
for b₂ being Subset of b₁
for b₃ being Point of b₁ st b₂ is open & b₃ in b₂ holds
b₂ is a_neighborhood of b₃

proof end;

theorem Th6: :: CONNSP_2:6

for b₁ being non empty TopSpace
for b₂ being Subset of b₁
for b₃ being Point of b₁ st b₂ is a_neighborhood of b₃ holds
b₃ in b₂

proof end;

theorem Th7: :: CONNSP_2:7

for b₁ being non empty TopSpace
for b₂ being Point of b₁
for b₃ being Subset of b₁ st b₃ is a_neighborhood of b₂ holds
ex b₄ being non empty Subset of b₁ st
( b₄ is a_neighborhood of b₂ & b₄ is open & b₄ c= b₃ )

proof end;

theorem Th8: :: CONNSP_2:8

for b₁ being non empty TopSpace
for b₂ being Point of b₁
for b₃ being Subset of b₁ holds
( b₃ is a_neighborhood of b₂ iff ex b₄ being Subset of b₁ st
( b₄ is open & b₄ c= b₃ & b₂ in b₄ ) )

proof end;

theorem Th9: :: CONNSP_2:9

for b₁ being non empty TopSpace
for b₂ being Subset of b₁ holds
( b₂ is open iff for b₃ being Point of b₁ st b₃ in b₂ holds
ex b₄ being Subset of b₁ st
( b₄ is a_neighborhood of b₃ & b₄ c= b₂ ) )

proof end;

theorem Th10: :: CONNSP_2:10

for b₁ being non empty TopSpace
for b₂ being Point of b₁
for b₃ being Subset of b₁ holds
( b₃ is a_neighborhood of {b₂} iff b₃ is a_neighborhood of b₂ )

proof end;

theorem Th11: :: CONNSP_2:11

for b₁ being non empty TopSpace
for b₂ being non empty Subset of b₁
for b₃ being Point of (b₁ | b₂)
for b₄ being Subset of (b₁ | b₂)
for b₅ being Subset of b₁
for b₆ being Point of b₁ st b₂ is open & b₄ is a_neighborhood of b₃ & b₄ = b₅ & b₃ = b₆ holds
b₅ is a_neighborhood of b₆

proof end;

Lemma8: for b₁ being non empty TopSpace
for b₂ being SubSpace of b₁
for b₃ being Subset of b₁
for b₄ being Subset of b₂ st b₃ = b₄ holds
(Int b₃) /\ ([#] b₂) c= Int b₄

proof end;

theorem Th12: :: CONNSP_2:12

for b₁ being non empty TopSpace
for b₂ being non empty Subset of b₁
for b₃ being Point of (b₁ | b₂)
for b₄ being Subset of (b₁ | b₂)
for b₅ being Subset of b₁
for b₆ being Point of b₁ st b₅ is a_neighborhood of b₆ & b₄ = b₅ & b₃ = b₆ holds
b₄ is a_neighborhood of b₃

proof end;

theorem Th13: :: CONNSP_2:13

for b₁ being non empty TopSpace
for b₂, b₃ being Subset of b₁ st b₂ is_a_component_of b₁ & b₂ c= b₃ holds
b₂ is_a_component_of b₃

proof end;

theorem Th14: :: CONNSP_2:14

for b₁ being non empty TopSpace
for b₂ being non empty SubSpace of b₁
for b₃ being Point of b₁
for b₄ being Point of b₂ st b₃ = b₄ holds
skl b₄ c= skl b₃

proof end;

definition

let c₁ be non empty TopSpace;
let c₂ be Point of c₁;
pred c₁ is_locally_connected_in c₂ means :Def3: :: CONNSP_2:def 3
for b₁ being Subset of a₁ st b₁ is a_neighborhood of a₂ holds
ex b₂ being Subset of a₁ st
( b₂ is a_neighborhood of a₂ & b₂ is connected & b₂ c= b₁ );

end;

:: deftheorem Def3 defines is_locally_connected_in CONNSP_2:def 3 :

definition

let c₁ be non empty TopSpace;
attr a₁ is locally_connected means :Def4: :: CONNSP_2:def 4
for b₁ being Point of a₁ holds a₁ is_locally_connected_in b₁;

end;

:: deftheorem Def4 defines locally_connected CONNSP_2:def 4 :

definition

let c₁ be non empty TopSpace;
let c₂ be Subset of c₁;
let c₃ be Point of c₁;
pred c₂ is_locally_connected_in c₃ means :Def5: :: CONNSP_2:def 5
for b₁ being non empty Subset of a₁ st a₂ = b₁ holds
ex b₂ being Point of (a₁ | b₁) st
( b₂ = a₃ & a₁ | b₁ is_locally_connected_in b₂ );

end;

:: deftheorem Def5 defines is_locally_connected_in CONNSP_2:def 5 :

definition

let c₁ be non empty TopSpace;
let c₂ be non empty Subset of c₁;
attr a₂ is locally_connected means :Def6: :: CONNSP_2:def 6
a₁ | a₂ is locally_connected;

end;

:: deftheorem Def6 defines locally_connected CONNSP_2:def 6 :

theorem Th15: :: CONNSP_2:15

canceled;

theorem Th16: :: CONNSP_2:16

canceled;

theorem Th17: :: CONNSP_2:17

canceled;

theorem Th18: :: CONNSP_2:18

canceled;

theorem Th19: :: CONNSP_2:19

for b₁ being non empty TopSpace
for b₂ being Point of b₁ holds
( b₁ is_locally_connected_in b₂ iff for b₃, b₄ being Subset of b₁ st b₃ is a_neighborhood of b₂ & b₄ is_a_component_of b₃ & b₂ in b₄ holds
b₄ is a_neighborhood of b₂ )

proof end;

theorem Th20: :: CONNSP_2:20

for b₁ being non empty TopSpace
for b₂ being Point of b₁ holds
( b₁ is_locally_connected_in b₂ iff for b₃ being non empty Subset of b₁ st b₃ is open & b₂ in b₃ holds
ex b₄ being Point of (b₁ | b₃) st
( b₄ = b₂ & b₂ in Int (skl b₄) ) )

proof end;

theorem Th21: :: CONNSP_2:21

for b₁ being non empty TopSpace st b₁ is locally_connected holds
for b₂ being Subset of b₁ st b₂ is_a_component_of b₁ holds
b₂ is open

proof end;

theorem Th22: :: CONNSP_2:22

for b₁ being non empty TopSpace
for b₂ being Point of b₁ st b₁ is_locally_connected_in b₂ holds
for b₃ being non empty Subset of b₁ st b₃ is open & b₂ in b₃ holds
b₃ is_locally_connected_in b₂

proof end;

theorem Th23: :: CONNSP_2:23

for b₁ being non empty TopSpace st b₁ is locally_connected holds
for b₂ being non empty Subset of b₁ st b₂ is open holds
b₂ is locally_connected

proof end;

theorem Th24: :: CONNSP_2:24

for b₁ being non empty TopSpace holds
( b₁ is locally_connected iff for b₂ being non empty Subset of b₁
for b₃ being Subset of b₁ st b₂ is open & b₃ is_a_component_of b₂ holds
b₃ is open )

proof end;

theorem Th25: :: CONNSP_2:25

for b₁ being non empty TopSpace st b₁ is locally_connected holds
for b₂ being non empty Subset of b₁
for b₃ being non empty Subset of (b₁ | b₂) st b₃ is connected & b₃ is open holds
ex b₄ being Subset of b₁ st
( b₄ is open & b₄ is connected & b₃ = b₂ /\ b₄ )

proof end;

theorem Th26: :: CONNSP_2:26

for b₁ being non empty TopSpace holds
( b₁ is_T4 iff for b₂, b₃ being Subset of b₁ st b₂ <> {} & b₃ <> [#] b₁ & b₂ c= b₃ & b₂ is closed & b₃ is open holds
ex b₄ being Subset of b₁ st
( b₄ is open & b₂ c= b₄ & Cl b₄ c= b₃ ) )

proof end;

theorem Th27: :: CONNSP_2:27

for b₁ being non empty TopSpace st b₁ is locally_connected & b₁ is_T4 holds
for b₂, b₃ being Subset of b₁ st b₂ <> {} & b₃ <> {} & b₂ is closed & b₃ is closed & b₂ misses b₃ & b₂ is connected & b₃ is connected holds
ex b₄, b₅ being Subset of b₁ st
( b₄ is connected & b₅ is connected & b₄ is open & b₅ is open & b₂ c= b₄ & b₃ c= b₅ & b₄ misses b₅ )

proof end;

theorem Th28: :: CONNSP_2:28

for b₁ being non empty TopSpace
for b₂ being Point of b₁
for b₃ being Subset-Family of b₁ st ( for b₄ being Subset of b₁ holds
( b₄ in b₃ iff ( b₄ is open & b₄ is closed & b₂ in b₄ ) ) ) holds
b₃ <> {}

proof end;

definition

let c₁ be non empty TopSpace;
let c₂ be Point of c₁;
func qskl c₂ -> Subset of a₁ means :Def7: :: CONNSP_2:def 7
ex b₁ being Subset-Family of a₁ st
( ( for b₂ being Subset of a₁ holds
( b₂ in b₁ iff ( b₂ is open & b₂ is closed & a₂ in b₂ ) ) ) & meet b₁ = a₃ );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def7 defines qskl CONNSP_2:def 7 :

theorem Th29: :: CONNSP_2:29

canceled;

theorem Th30: :: CONNSP_2:30

for b₁ being non empty TopSpace
for b₂ being Point of b₁ holds b₂ in qskl b₂

proof end;

theorem Th31: :: CONNSP_2:31

for b₁ being non empty TopSpace
for b₂ being Point of b₁
for b₃ being Subset of b₁ st b₃ is open & b₃ is closed & b₂ in b₃ & b₃ c= qskl b₂ holds
b₃ = qskl b₂

proof end;

theorem Th32: :: CONNSP_2:32

for b₁ being non empty TopSpace
for b₂ being Point of b₁ holds qskl b₂ is closed

proof end;

theorem Th33: :: CONNSP_2:33

for b₁ being non empty TopSpace
for b₂ being Point of b₁ holds skl b₂ c= qskl b₂

proof end;