:: Sequences in $R^n$
:: by Agnieszka Sakowicz , Jaros{\l}aw Gryko and Adam Grabowski
::
:: Received May 10, 1994
:: Copyright (c) 1994 Association of Mizar Users
theorem :: TOPRNS_1:1
canceled;
theorem Th2: :: TOPRNS_1:2
:: deftheorem Def1 defines non-zero TOPRNS_1:def 1 :
theorem Th3: :: TOPRNS_1:3
theorem Th4: :: TOPRNS_1:4
:: deftheorem Def2 defines + TOPRNS_1:def 2 :
:: deftheorem Def3 defines * TOPRNS_1:def 3 :
:: deftheorem Def4 defines - TOPRNS_1:def 4 :
:: deftheorem defines - TOPRNS_1:def 5 :
:: deftheorem TOPRNS_1:def 6 :
canceled;
:: deftheorem Def7 defines |. TOPRNS_1:def 7 :
theorem :: TOPRNS_1:5
canceled;
theorem :: TOPRNS_1:6
canceled;
theorem :: TOPRNS_1:7
canceled;
theorem Th8: :: TOPRNS_1:8
theorem :: TOPRNS_1:9
theorem :: TOPRNS_1:10
theorem Th11: :: TOPRNS_1:11
theorem Th12: :: TOPRNS_1:12
theorem Th13: :: TOPRNS_1:13
theorem Th14: :: TOPRNS_1:14
theorem Th15: :: TOPRNS_1:15
theorem :: TOPRNS_1:16
theorem Th17: :: TOPRNS_1:17
theorem Th18: :: TOPRNS_1:18
theorem :: TOPRNS_1:19
theorem :: TOPRNS_1:20
theorem :: TOPRNS_1:21
theorem Th22: :: TOPRNS_1:22
theorem :: TOPRNS_1:23
theorem Th24: :: TOPRNS_1:24
theorem Th25: :: TOPRNS_1:25
theorem :: TOPRNS_1:26
theorem :: TOPRNS_1:27
theorem Th28: :: TOPRNS_1:28
Lm1:
for N being Element of NAT
for w1, w2 being Point of (TOP-REAL N) st |.(w1 - w2).| = 0 holds
w1 = w2
Lm2:
for N being Element of NAT
for w1, w2 being Point of (TOP-REAL N) st w1 = w2 holds
|.(w1 - w2).| = 0
theorem :: TOPRNS_1:29
theorem Th30: :: TOPRNS_1:30
theorem :: TOPRNS_1:31
theorem :: TOPRNS_1:32
theorem Th33: :: TOPRNS_1:33
theorem :: TOPRNS_1:34
theorem :: TOPRNS_1:35
theorem :: TOPRNS_1:36
canceled;
theorem :: TOPRNS_1:37
canceled;
theorem :: TOPRNS_1:38
canceled;
:: deftheorem Def8 defines bounded TOPRNS_1:def 8 :
theorem Th39: :: TOPRNS_1:39
:: deftheorem Def9 defines convergent TOPRNS_1:def 9 :
:: deftheorem Def10 defines lim TOPRNS_1:def 10 :
theorem :: TOPRNS_1:40
canceled;
theorem Th41: :: TOPRNS_1:41
theorem Th42: :: TOPRNS_1:42
theorem Th43: :: TOPRNS_1:43
theorem Th44: :: TOPRNS_1:44
theorem Th45: :: TOPRNS_1:45
theorem Th46: :: TOPRNS_1:46
theorem :: TOPRNS_1:47
theorem :: TOPRNS_1:48
theorem :: TOPRNS_1:49
canceled;
theorem :: TOPRNS_1:50
theorem :: TOPRNS_1:51