:: Egoroff's Theorem
:: by Noboru Endou , Yasunari Shidama and Keiko Narita
::
:: Received October 30, 2007
:: Copyright (c) 2007 Association of Mizar Users
theorem Th1: :: MESFUNC8:1
theorem Th2: :: MESFUNC8:2
theorem Th3: :: MESFUNC8:3
theorem Th4: :: MESFUNC8:4
theorem :: MESFUNC8:5
theorem :: MESFUNC8:6
:: deftheorem Def1 defines with_the_same_dom MESFUNC8:def 1 :
:: deftheorem Def2 defines with_the_same_dom MESFUNC8:def 2 :
:: deftheorem Def3 defines inf MESFUNC8:def 3 :
:: deftheorem Def4 defines sup MESFUNC8:def 4 :
:: deftheorem Def5 defines inferior_realsequence MESFUNC8:def 5 :
:: deftheorem Def6 defines superior_realsequence MESFUNC8:def 6 :
theorem Th7: :: MESFUNC8:7
theorem Th8: :: MESFUNC8:8
theorem Th9: :: MESFUNC8:9
theorem Th10: :: MESFUNC8:10
:: deftheorem MESFUNC8:def 7 :
canceled;
:: deftheorem Def8 defines lim_inf MESFUNC8:def 8 :
:: deftheorem Def9 defines lim_sup MESFUNC8:def 9 :
theorem Th11: :: MESFUNC8:11
theorem Th12: :: MESFUNC8:12
theorem :: MESFUNC8:13
:: deftheorem Def10 defines lim MESFUNC8:def 10 :
theorem Th14: :: MESFUNC8:14
theorem Th15: :: MESFUNC8:15
theorem Th16: :: MESFUNC8:16
theorem Th17: :: MESFUNC8:17
theorem Th18: :: MESFUNC8:18
theorem Th19: :: MESFUNC8:19
theorem Th20: :: MESFUNC8:20
theorem Th21: :: MESFUNC8:21
theorem Th22: :: MESFUNC8:22
theorem Th23: :: MESFUNC8:23
theorem :: MESFUNC8:24
theorem Th25: :: MESFUNC8:25
theorem Th26: :: MESFUNC8:26
theorem Th27: :: MESFUNC8:27
theorem Th28: :: MESFUNC8:28
theorem :: MESFUNC8:29
theorem :: MESFUNC8:30