:: First-countable, Sequential, and { F } rechet Spaces
:: by Bart{\l}omiej Skorulski
::
:: Received May 13, 1998
:: Copyright (c) 1998 Association of Mizar Users
Lm2:
for r being Real st r > 0 holds
ex n being Element of NAT st
( 1 / n < r & n > 0 )
theorem :: FRECHET:1
theorem Th2: :: FRECHET:2
theorem Th3: :: FRECHET:3
Lm3:
for T being TopStruct
for A being Subset of T holds
( A is open iff ([#] T) \ A is closed )
theorem Th4: :: FRECHET:4
theorem Th5: :: FRECHET:5
theorem Th6: :: FRECHET:6
theorem Th7: :: FRECHET:7
theorem :: FRECHET:8
theorem Th9: :: FRECHET:9
theorem Th10: :: FRECHET:10
theorem Th11: :: FRECHET:11
theorem Th12: :: FRECHET:12
theorem Th13: :: FRECHET:13
for
A,
B being
set st
B c= A holds
(id A) .: B = B
theorem :: FRECHET:14
canceled;
theorem Th15: :: FRECHET:15
theorem Th16: :: FRECHET:16
theorem Th17: :: FRECHET:17
theorem Th18: :: FRECHET:18
theorem Th19: :: FRECHET:19
theorem Th20: :: FRECHET:20
:: deftheorem Def1 defines first-countable FRECHET:def 1 :
theorem Th21: :: FRECHET:21
theorem :: FRECHET:22
:: deftheorem Def2 defines is_convergent_to FRECHET:def 2 :
theorem Th23: :: FRECHET:23
:: deftheorem Def3 defines convergent FRECHET:def 3 :
:: deftheorem Def4 defines Lim FRECHET:def 4 :
:: deftheorem Def5 defines Frechet FRECHET:def 5 :
:: deftheorem defines sequential FRECHET:def 6 :
theorem Th24: :: FRECHET:24
theorem :: FRECHET:25
canceled;
theorem Th26: :: FRECHET:26
theorem Th27: :: FRECHET:27
theorem Th28: :: FRECHET:28
:: deftheorem Def7 defines REAL? FRECHET:def 7 :
Lm4:
{REAL } c= the carrier of REAL?
theorem :: FRECHET:29
canceled;
theorem Th30: :: FRECHET:30
theorem Th31: :: FRECHET:31
theorem Th32: :: FRECHET:32
theorem Th33: :: FRECHET:33
theorem Th34: :: FRECHET:34
theorem Th35: :: FRECHET:35
theorem Th36: :: FRECHET:36
theorem :: FRECHET:37
theorem :: FRECHET:38
canceled;
theorem :: FRECHET:39
theorem :: FRECHET:40