:: Locally Connected Spaces
:: by Beata Padlewska
::
:: Received September 5, 1990
:: Copyright (c) 1990 Association of Mizar Users
:: deftheorem Def1 defines a_neighborhood CONNSP_2:def 1 :
:: deftheorem Def2 defines a_neighborhood CONNSP_2:def 2 :
theorem :: CONNSP_2:1
canceled;
theorem :: CONNSP_2:2
canceled;
theorem :: CONNSP_2:3
theorem :: CONNSP_2:4
theorem Th5: :: CONNSP_2:5
theorem Th6: :: CONNSP_2:6
theorem Th7: :: CONNSP_2:7
theorem Th8: :: CONNSP_2:8
theorem :: CONNSP_2:9
theorem :: CONNSP_2:10
theorem Th11: :: CONNSP_2:11
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
theorem Th12: :: CONNSP_2:12
theorem Th13: :: CONNSP_2:13
theorem :: CONNSP_2:14
:: deftheorem Def3 defines is_locally_connected_in CONNSP_2:def 3 :
:: deftheorem Def4 defines locally_connected CONNSP_2:def 4 :
:: deftheorem Def5 defines is_locally_connected_in CONNSP_2:def 5 :
:: 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
theorem Th20: :: CONNSP_2:20
theorem Th21: :: CONNSP_2:21
theorem Th22: :: CONNSP_2:22
theorem Th23: :: CONNSP_2:23
theorem Th24: :: CONNSP_2:24
theorem :: CONNSP_2:25
theorem Th26: :: CONNSP_2:26
theorem :: CONNSP_2:27
theorem Th28: :: CONNSP_2:28
:: deftheorem Def7 defines qComponent_of CONNSP_2:def 7 :
theorem :: CONNSP_2:29
canceled;
theorem :: CONNSP_2:30
theorem :: CONNSP_2:31
theorem :: CONNSP_2:32
theorem :: CONNSP_2:33
theorem :: CONNSP_2:34
theorem :: CONNSP_2:35
theorem :: CONNSP_2:36