:: The Sequential Closure Operator In Sequential and Frechet Spaces
:: by Bart{\l}omiej Skorulski
::
:: Received February 13, 1999
:: Copyright (c) 1999 Association of Mizar Users
Lm1:
for T being non empty TopSpace st ( for p being Point of T holds Cl {p} = {p} ) holds
T is T_1
Lm2:
for T being non empty TopSpace st not T is T_1 holds
ex x1, x2 being Point of T st
( x1 <> x2 & x2 in Cl {x1} )
Lm3:
for T being non empty TopSpace st not T is T_1 holds
ex x1, x2 being Point of T ex S being sequence of T st
( S = NAT --> x1 & x1 <> x2 & S is_convergent_to x2 )
Lm4:
for T being non empty TopSpace st T is T_2 holds
T is T_1
theorem :: FRECHET2:1
theorem :: FRECHET2:2
theorem :: FRECHET2:3
canceled;
theorem :: FRECHET2:4
canceled;
theorem :: FRECHET2:5
canceled;
theorem Th6: :: FRECHET2:6
theorem Th7: :: FRECHET2:7
Lm10:
for T being non empty TopSpace st T is first-countable holds
for x being Point of T ex B being Basis of x ex S being Function st
( dom S = NAT & rng S = B & ( for n, m being Element of NAT st m >= n holds
S . m c= S . n ) )
theorem :: FRECHET2:8
theorem Th9: :: FRECHET2:9
theorem :: FRECHET2:10
theorem Th11: :: FRECHET2:11
theorem Th12: :: FRECHET2:12
theorem :: FRECHET2:13
theorem Th14: :: FRECHET2:14
theorem :: FRECHET2:15
:: deftheorem FRECHET2:def 1 :
canceled;
:: deftheorem Def2 defines Cl_Seq FRECHET2:def 2 :
theorem Th16: :: FRECHET2:16
theorem Th17: :: FRECHET2:17
theorem Th18: :: FRECHET2:18
theorem Th19: :: FRECHET2:19
theorem Th20: :: FRECHET2:20
theorem Th21: :: FRECHET2:21
theorem Th22: :: FRECHET2:22
theorem Th23: :: FRECHET2:23
theorem Th24: :: FRECHET2:24
theorem Th25: :: FRECHET2:25
theorem :: FRECHET2:26
:: deftheorem Def3 defines lim FRECHET2:def 3 :
theorem Th27: :: FRECHET2:27
theorem Th28: :: FRECHET2:28
theorem :: FRECHET2:29
theorem :: FRECHET2:30
theorem Th31: :: FRECHET2:31
theorem :: FRECHET2:32
theorem :: FRECHET2:33
:: deftheorem Def4 defines is_a_cluster_point_of FRECHET2:def 4 :
theorem Th34: :: FRECHET2:34
theorem :: FRECHET2:35
theorem Th36: :: FRECHET2:36
theorem Th37: :: FRECHET2:37
theorem Th38: :: FRECHET2:38
theorem Th39: :: FRECHET2:39
theorem Th40: :: FRECHET2:40
theorem :: FRECHET2:41
theorem :: FRECHET2:42
canceled;
theorem Th43: :: FRECHET2:43
theorem Th44: :: FRECHET2:44
theorem :: FRECHET2:45
theorem :: FRECHET2:46
theorem :: FRECHET2:47
theorem :: FRECHET2:48
theorem :: FRECHET2:49