:: The Measurability of Complex-Valued Functional Sequences
:: by Keiko Narita , Noboru Endou and Yasunari Shidama
::
:: Received December 16, 2008
:: Copyright (c) 2008 Association of Mizar Users
:: deftheorem defines R_EAL MESFUN7C:def 1 :
theorem Th1: :: MESFUN7C:1
:: deftheorem defines inf MESFUN7C:def 2 :
theorem Th2: :: MESFUN7C:2
:: deftheorem defines sup MESFUN7C:def 3 :
theorem Th3: :: MESFUN7C:3
:: deftheorem defines inferior_realsequence MESFUN7C:def 4 :
theorem Th4: :: MESFUN7C:4
:: deftheorem defines superior_realsequence MESFUN7C:def 5 :
theorem Th5: :: MESFUN7C:5
theorem :: MESFUN7C:6
theorem Th7: :: MESFUN7C:7
theorem Th8: :: MESFUN7C:8
theorem :: MESFUN7C:9
theorem :: MESFUN7C:10
theorem Th11: :: MESFUN7C:11
:: deftheorem defines lim_inf MESFUN7C:def 6 :
theorem Th12: :: MESFUN7C:12
:: deftheorem defines lim_sup MESFUN7C:def 7 :
theorem Th13: :: MESFUN7C:13
:: deftheorem defines lim MESFUN7C:def 8 :
theorem Th14: :: MESFUN7C:14
theorem Th15: :: MESFUN7C:15
theorem :: MESFUN7C:16
theorem :: MESFUN7C:17
theorem Th18: :: MESFUN7C:18
theorem :: MESFUN7C:19
theorem :: MESFUN7C:20
theorem Th21: :: MESFUN7C:21
theorem Th22: :: MESFUN7C:22
:: deftheorem Def9 defines # MESFUN7C:def 9 :
:: deftheorem Def10 defines lim MESFUN7C:def 10 :
:: deftheorem Def11 defines Re MESFUN7C:def 11 :
:: deftheorem Def12 defines Im MESFUN7C:def 12 :
theorem Th23: :: MESFUN7C:23
theorem Th24: :: MESFUN7C:24
theorem Th25: :: MESFUN7C:25
theorem :: MESFUN7C:26
theorem :: MESFUN7C:27
theorem :: MESFUN7C:28
Lm1:
for X being non empty set
for f being PartFunc of X,COMPLEX holds |.f.| is nonnegative
theorem :: MESFUN7C:29
theorem Th30: :: MESFUN7C:30
theorem Th31: :: MESFUN7C:31
theorem Th32: :: MESFUN7C:32
theorem :: MESFUN7C:33
theorem Th34: :: MESFUN7C:34
theorem Th35: :: MESFUN7C:35
theorem :: MESFUN7C:36
theorem Th37: :: MESFUN7C:37
theorem Th38: :: MESFUN7C:38
theorem Th39: :: MESFUN7C:39
theorem Th40: :: MESFUN7C:40
theorem Th41: :: MESFUN7C:41
theorem :: MESFUN7C:42
:: deftheorem Def13 defines is_simple_func_in MESFUN7C:def 13 :
:: deftheorem Def14 defines are_Re-presentation_of MESFUN7C:def 14 :
:: deftheorem Def15 defines are_Re-presentation_of MESFUN7C:def 15 :
theorem :: MESFUN7C:43
theorem Th44: :: MESFUN7C:44
theorem Th45: :: MESFUN7C:45
theorem Th46: :: MESFUN7C:46
theorem Th47: :: MESFUN7C:47
theorem Th48: :: MESFUN7C:48
theorem :: MESFUN7C:49