:: Limit of Sequence of Subsets
:: by Bo Zhang , Hiroshi Yamazaki and Yatsuka Nakamura
::
:: Received March 15, 2005
:: Copyright (c) 2005 Association of Mizar Users
LM1:
for i, j being Element of NAT holds
( not i <= j or i = j or i + 1 <= j )
theorem Th5: :: SETLIM_1:1
theorem Th6: :: SETLIM_1:2
theorem Th7: :: SETLIM_1:3
theorem Th8: :: SETLIM_1:4
theorem Th10: :: SETLIM_1:5
theorem Th11: :: SETLIM_1:6
theorem Th15: :: SETLIM_1:7
theorem Th16: :: SETLIM_1:8
theorem :: SETLIM_1:9
theorem Th185: :: SETLIM_1:10
theorem Th186: :: SETLIM_1:11
theorem :: SETLIM_1:12
Th188:
for X being set
for A being Subset of X
for B being SetSequence of X st B is constant & the_value_of B = A holds
for n being Element of NAT holds
( B . n = A & Union B = A & Intersection B = A )
theorem Th190: :: SETLIM_1:13
theorem Th191: :: SETLIM_1:14
theorem Th17: :: SETLIM_1:15
theorem Th18: :: SETLIM_1:16
:: deftheorem def1 defines monotone SETLIM_1:def 1 :
:: deftheorem def2 defines inferior_setsequence SETLIM_1:def 2 :
:: deftheorem def3 defines superior_setsequence SETLIM_1:def 3 :
theorem Th19: :: SETLIM_1:17
theorem Th20: :: SETLIM_1:18
theorem Th21: :: SETLIM_1:19
theorem Th22: :: SETLIM_1:20
theorem Th23: :: SETLIM_1:21
theorem Th24: :: SETLIM_1:22
theorem Th25: :: SETLIM_1:23
theorem Th26: :: SETLIM_1:24
theorem :: SETLIM_1:25
theorem :: SETLIM_1:26
theorem :: SETLIM_1:27
theorem Th98: :: SETLIM_1:28
theorem :: SETLIM_1:29
theorem Th101: :: SETLIM_1:30
theorem :: SETLIM_1:31
theorem Th103: :: SETLIM_1:32
theorem :: SETLIM_1:33
theorem :: SETLIM_1:34
theorem :: SETLIM_1:35
theorem :: SETLIM_1:36
theorem :: SETLIM_1:37
theorem Th125: :: SETLIM_1:38
theorem Th126: :: SETLIM_1:39
theorem Th29: :: SETLIM_1:40
theorem Th30: :: SETLIM_1:41
theorem Th31: :: SETLIM_1:42
theorem Th32: :: SETLIM_1:43
theorem Th33: :: SETLIM_1:44
theorem Th34: :: SETLIM_1:45
theorem Th35: :: SETLIM_1:46
theorem Th36: :: SETLIM_1:47
theorem Th37: :: SETLIM_1:48
theorem Th38: :: SETLIM_1:49
theorem Th39: :: SETLIM_1:50
theorem Th40: :: SETLIM_1:51
theorem Th41: :: SETLIM_1:52
theorem Th42: :: SETLIM_1:53
:: deftheorem defines lim_inf SETLIM_1:def 4 :
:: deftheorem defines lim_sup SETLIM_1:def 5 :
theorem :: SETLIM_1:54
theorem :: SETLIM_1:55
theorem :: SETLIM_1:56
theorem :: SETLIM_1:57
theorem Th215: :: SETLIM_1:58
theorem Th48: :: SETLIM_1:59
theorem Th49: :: SETLIM_1:60
theorem Th51: :: SETLIM_1:61
theorem Th52: :: SETLIM_1:62
theorem Th50: :: SETLIM_1:63
theorem Th53: :: SETLIM_1:64
theorem :: SETLIM_1:65
:: deftheorem SETLIM_1:def 6 :
canceled;
theorem Th55: :: SETLIM_1:66
theorem Th56: :: SETLIM_1:67
theorem :: SETLIM_1:68
theorem :: SETLIM_1:69
theorem :: SETLIM_1:70
:: deftheorem defines @Complement SETLIM_1:def 7 :
theorem Th205: :: SETLIM_1:71
theorem :: SETLIM_1:72
theorem :: SETLIM_1:73
theorem :: SETLIM_1:74
theorem :: SETLIM_1:75
theorem :: SETLIM_1:76
theorem :: SETLIM_1:77
theorem Th61: :: SETLIM_1:78
theorem Th62: :: SETLIM_1:79
theorem Th63: :: SETLIM_1:80
theorem Th64: :: SETLIM_1:81
theorem Th65: :: SETLIM_1:82
theorem Th66: :: SETLIM_1:83
theorem :: SETLIM_1:84