:: Conjugate Sequences, Bounded Complex Sequences and ConvergentComplex Sequences
:: by Adam Naumowicz
::
:: Received December 20, 1996
:: Copyright (c) 1996 Association of Mizar Users
theorem Th1: :: COMSEQ_2:1
theorem Th2: :: COMSEQ_2:2
:: deftheorem Def1 defines *' COMSEQ_2:def 1 :
:: deftheorem Def2 defines *' COMSEQ_2:def 2 :
theorem :: COMSEQ_2:3
theorem :: COMSEQ_2:4
theorem :: COMSEQ_2:5
theorem :: COMSEQ_2:6
theorem :: COMSEQ_2:7
:: deftheorem Def3 defines bounded COMSEQ_2:def 3 :
reconsider sc = NAT --> 0c as Complex_Sequence ;
Lm1:
for n being Element of NAT holds sc . n = 0c
by FUNCOP_1:13;
theorem Th8: :: COMSEQ_2:8
:: deftheorem Def4 defines convergent COMSEQ_2:def 4 :
:: deftheorem Def5 defines lim COMSEQ_2:def 5 :
theorem Th9: :: COMSEQ_2:9
theorem Th10: :: COMSEQ_2:10
reconsider cs = NAT --> 0 as Real_Sequence by FUNCOP_1:57;
theorem Th11: :: COMSEQ_2:11
theorem Th12: :: COMSEQ_2:12
theorem Th13: :: COMSEQ_2:13
theorem Th14: :: COMSEQ_2:14
theorem :: COMSEQ_2:15
theorem :: COMSEQ_2:16
theorem :: COMSEQ_2:17
theorem Th18: :: COMSEQ_2:18
theorem :: COMSEQ_2:19
theorem :: COMSEQ_2:20
theorem :: COMSEQ_2:21
theorem Th22: :: COMSEQ_2:22
theorem :: COMSEQ_2:23
theorem :: COMSEQ_2:24
theorem Th25: :: COMSEQ_2:25
theorem Th26: :: COMSEQ_2:26
theorem :: COMSEQ_2:27
theorem :: COMSEQ_2:28
theorem Th29: :: COMSEQ_2:29
theorem Th30: :: COMSEQ_2:30
theorem :: COMSEQ_2:31
theorem :: COMSEQ_2:32
theorem Th33: :: COMSEQ_2:33
theorem Th34: :: COMSEQ_2:34
theorem Th35: :: COMSEQ_2:35
theorem :: COMSEQ_2:36
theorem :: COMSEQ_2:37
theorem Th38: :: COMSEQ_2:38
theorem Th39: :: COMSEQ_2:39
theorem :: COMSEQ_2:40
theorem :: COMSEQ_2:41
theorem Th42: :: COMSEQ_2:42
theorem Th43: :: COMSEQ_2:43
theorem :: COMSEQ_2:44
theorem :: COMSEQ_2:45