:: 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 LEM1: :: MESFUN7C:1
:: deftheorem defines inf MESFUN7C:def 2 :
theorem Def3a: :: MESFUN7C:2
:: deftheorem defines sup MESFUN7C:def 3 :
theorem Def4a: :: MESFUN7C:3
:: deftheorem defines inferior_realsequence MESFUN7C:def 4 :
theorem Def5a: :: MESFUN7C:4
:: deftheorem defines superior_realsequence MESFUN7C:def 5 :
theorem Def6a: :: MESFUN7C:5
theorem :: MESFUN7C:6
theorem LEM4: :: MESFUN7C:7
theorem LEM5: :: MESFUN7C:8
theorem :: MESFUN7C:9
theorem :: MESFUN7C:10
theorem Th10: :: MESFUN7C:11
:: deftheorem defines lim_inf MESFUN7C:def 6 :
theorem Def8a: :: MESFUN7C:12
:: deftheorem defines lim_sup MESFUN7C:def 7 :
theorem Def9a: :: MESFUN7C:13
:: deftheorem defines lim MESFUN7C:def 8 :
theorem Def10a: :: MESFUN7C:14
theorem Th14: :: MESFUN7C:15
theorem :: MESFUN7C:16
theorem :: MESFUN7C:17
theorem Th23: :: MESFUN7C:18
theorem :: MESFUN7C:19
theorem :: MESFUN7C:20
theorem Th25: :: MESFUN7C:21
theorem Th26: :: MESFUN7C:22
:: deftheorem Def11 defines # MESFUN7C:def 9 :
:: deftheorem Def12 defines lim MESFUN7C:def 10 :
:: deftheorem Def13 defines Re MESFUN7C:def 11 :
:: deftheorem Def14 defines Im MESFUN7C:def 12 :
theorem Th7a: :: MESFUN7C:23
theorem Th7b: :: MESFUN7C:24
theorem Th7c: :: MESFUN7C:25
theorem :: MESFUN7C:26
theorem :: MESFUN7C:27
theorem :: MESFUN7C:28
Lem01:
for X being non empty set
for f being PartFunc of X,COMPLEX holds |.f.| is nonnegative
theorem :: MESFUN7C:29
theorem LEM6: :: MESFUN7C:30
theorem MES715: :: MESFUN7C:31
theorem COM715: :: MESFUN7C:32
theorem :: MESFUN7C:33
theorem MES591: :: MESFUN7C:34
theorem LEM7: :: MESFUN7C:35
theorem :: MESFUN7C:36
theorem Th18: :: MESFUN7C:37
theorem Th19: :: MESFUN7C:38
theorem Th20: :: MESFUN7C:39
theorem Th21: :: MESFUN7C:40
theorem MES71: :: MESFUN7C:41
theorem :: MESFUN7C:42
:: deftheorem MES2def5 defines is_simple_func_in MESFUN7C:def 13 :
:: deftheorem MES3def1 defines are_Re-presentation_of MESFUN7C:def 14 :
:: deftheorem MES3Cdef1 defines are_Re-presentation_of MESFUN7C:def 15 :
theorem :: MESFUN7C:43
theorem MES33A: :: MESFUN7C:44
theorem MES312: :: MESFUN7C:45
theorem Def31: :: MESFUN7C:46
theorem Def32: :: MESFUN7C:47
theorem Def16: :: MESFUN7C:48
theorem :: MESFUN7C:49