:: Convergent Sequences and the Limit of Sequences
:: by Jaros{\l}aw Kotowicz
::
:: Received July 4, 1989
:: Copyright (c) 1990 Association of Mizar Users
theorem :: SEQ_2:1
canceled;
theorem :: SEQ_2:2
canceled;
theorem :: SEQ_2:3
canceled;
theorem :: SEQ_2:4
canceled;
theorem :: SEQ_2:5
canceled;
theorem :: SEQ_2:6
canceled;
theorem :: SEQ_2:7
canceled;
theorem :: SEQ_2:8
canceled;
theorem Th9: :: SEQ_2:9
theorem :: SEQ_2:10
canceled;
theorem Th11: :: SEQ_2:11
:: deftheorem Def1 defines bounded_above SEQ_2:def 1 :
:: deftheorem Def2 defines bounded_below SEQ_2:def 2 :
:: deftheorem Def3 defines bounded_above SEQ_2:def 3 :
:: deftheorem Def4 defines bounded_below SEQ_2:def 4 :
:: deftheorem defines bounded SEQ_2:def 5 :
theorem :: SEQ_2:12
canceled;
theorem :: SEQ_2:13
canceled;
theorem :: SEQ_2:14
canceled;
theorem Th15: :: SEQ_2:15
theorem Th16: :: SEQ_2:16
:: deftheorem Def6 defines convergent SEQ_2:def 6 :
:: deftheorem Def7 defines lim SEQ_2:def 7 :
:: deftheorem defines bounded SEQ_2:def 8 :
theorem :: SEQ_2:17
canceled;
theorem :: SEQ_2:18
canceled;
theorem Th19: :: SEQ_2:19
theorem Th20: :: SEQ_2:20
theorem Th21: :: SEQ_2:21
theorem Th22: :: SEQ_2:22
theorem :: SEQ_2:23
theorem Th24: :: SEQ_2:24
theorem Th25: :: SEQ_2:25
theorem Th26: :: SEQ_2:26
theorem Th27: :: SEQ_2:27
theorem Th28: :: SEQ_2:28
theorem Th29: :: SEQ_2:29
theorem Th30: :: SEQ_2:30
theorem Th31: :: SEQ_2:31
theorem :: SEQ_2:32
theorem Th33: :: SEQ_2:33
theorem :: SEQ_2:34
theorem Th35: :: SEQ_2:35
theorem Th36: :: SEQ_2:36
theorem :: SEQ_2:37
theorem :: SEQ_2:38
theorem Th39: :: SEQ_2:39
theorem :: SEQ_2:40