:: On the {K}uratowski Limit Operators
:: by Adam Grabowski
::
:: Received August 12, 2003
:: Copyright (c) 2003 Association of Mizar Users
theorem :: KURATO_2:1
canceled;
theorem :: KURATO_2:2
theorem :: KURATO_2:3
canceled;
theorem Th4: :: KURATO_2:4
:: deftheorem KURATO_2:def 1 :
canceled;
:: deftheorem KURATO_2:def 2 :
canceled;
:: deftheorem Def3 defines lim_inf KURATO_2:def 3 :
:: deftheorem Def4 defines lim_sup KURATO_2:def 4 :
theorem :: KURATO_2:5
canceled;
theorem Th6: :: KURATO_2:6
theorem Th7: :: KURATO_2:7
theorem Th8: :: KURATO_2:8
theorem :: KURATO_2:9
theorem Th10: :: KURATO_2:10
theorem Th11: :: KURATO_2:11
theorem :: KURATO_2:12
theorem :: KURATO_2:13
theorem :: KURATO_2:14
theorem :: KURATO_2:15
theorem :: KURATO_2:16
theorem Th17: :: KURATO_2:17
theorem Th18: :: KURATO_2:18
theorem :: KURATO_2:19
theorem :: KURATO_2:20
theorem Th21: :: KURATO_2:21
:: deftheorem Def5 defines non-ascending KURATO_2:def 5 :
:: deftheorem Def6 defines non-descending KURATO_2:def 6 :
theorem :: KURATO_2:22
canceled;
theorem :: KURATO_2:23
canceled;
theorem Th24: :: KURATO_2:24
theorem :: KURATO_2:25
theorem :: KURATO_2:26
:: deftheorem Def7 defines convergent KURATO_2:def 7 :
theorem :: KURATO_2:27
:: deftheorem KURATO_2:def 8 :
canceled;
:: deftheorem Def9 defines Lim_K KURATO_2:def 9 :
theorem :: KURATO_2:28
theorem :: KURATO_2:29
canceled;
theorem Th30: :: KURATO_2:30
theorem :: KURATO_2:31
canceled;
theorem Th32: :: KURATO_2:32
theorem Th33: :: KURATO_2:33
theorem :: KURATO_2:34
theorem :: KURATO_2:35
canceled;
theorem :: KURATO_2:36
theorem :: KURATO_2:37
theorem Th38: :: KURATO_2:38
theorem Th39: :: KURATO_2:39
theorem Th40: :: KURATO_2:40
theorem Th41: :: KURATO_2:41
theorem :: KURATO_2:42
canceled;
theorem :: KURATO_2:43
canceled;
theorem :: KURATO_2:44
canceled;
theorem Th47: :: KURATO_2:45
theorem :: KURATO_2:46
canceled;
theorem :: KURATO_2:47
:: deftheorem KURATO_2:def 10 :
canceled;
:: deftheorem Def11 defines Lim_inf KURATO_2:def 11 :
theorem Th50: :: KURATO_2:48
theorem Th51: :: KURATO_2:49
theorem Th52: :: KURATO_2:50
theorem :: KURATO_2:51
theorem Th54: :: KURATO_2:52
theorem :: KURATO_2:53
theorem :: KURATO_2:54
theorem Th57: :: KURATO_2:55
theorem :: KURATO_2:56
theorem Th59: :: KURATO_2:57
theorem Th60: :: KURATO_2:58
theorem :: KURATO_2:59
theorem Th62: :: KURATO_2:60
theorem :: KURATO_2:61
theorem Th64: :: KURATO_2:62
theorem :: KURATO_2:63
theorem :: KURATO_2:64
:: deftheorem Def12 defines Lim_sup KURATO_2:def 12 :
theorem :: KURATO_2:65
theorem Th68: :: KURATO_2:66
theorem Th69: :: KURATO_2:67
theorem :: KURATO_2:68
theorem Th71: :: KURATO_2:69
theorem :: KURATO_2:70
theorem :: KURATO_2:71
theorem Th74: :: KURATO_2:72
theorem :: KURATO_2:73
theorem Th76: :: KURATO_2:74
theorem :: KURATO_2:75
theorem :: KURATO_2:76