:: Some Equations Related to the Limit of Sequence of Subsets
:: by Bo Zhang , Hiroshi Yamazaki and Yatsuka Nakamura
::
:: Received May 24, 2005
:: Copyright (c) 2005 Association of Mizar Users
theorem Th1: :: SETLIM_2:1
theorem Th2: :: SETLIM_2:2
definition
let X be
set ;
let A1,
A2 be
SetSequence of
X;
func A1 (/\) A2 -> SetSequence of
X means :
Def1:
:: SETLIM_2:def 1
for
n being
Element of
NAT holds
it . n = (A1 . n) /\ (A2 . n);
existence
ex b1 being SetSequence of X st
for n being Element of NAT holds b1 . n = (A1 . n) /\ (A2 . n)
uniqueness
for b1, b2 being SetSequence of X st ( for n being Element of NAT holds b1 . n = (A1 . n) /\ (A2 . n) ) & ( for n being Element of NAT holds b2 . n = (A1 . n) /\ (A2 . n) ) holds
b1 = b2
commutativity
for b1, A1, A2 being SetSequence of X st ( for n being Element of NAT holds b1 . n = (A1 . n) /\ (A2 . n) ) holds
for n being Element of NAT holds b1 . n = (A2 . n) /\ (A1 . n)
;
func A1 (\/) A2 -> SetSequence of
X means :
Def2:
:: SETLIM_2:def 2
for
n being
Element of
NAT holds
it . n = (A1 . n) \/ (A2 . n);
existence
ex b1 being SetSequence of X st
for n being Element of NAT holds b1 . n = (A1 . n) \/ (A2 . n)
uniqueness
for b1, b2 being SetSequence of X st ( for n being Element of NAT holds b1 . n = (A1 . n) \/ (A2 . n) ) & ( for n being Element of NAT holds b2 . n = (A1 . n) \/ (A2 . n) ) holds
b1 = b2
commutativity
for b1, A1, A2 being SetSequence of X st ( for n being Element of NAT holds b1 . n = (A1 . n) \/ (A2 . n) ) holds
for n being Element of NAT holds b1 . n = (A2 . n) \/ (A1 . n)
;
func A1 (\) A2 -> SetSequence of
X means :
Def3:
:: SETLIM_2:def 3
for
n being
Element of
NAT holds
it . n = (A1 . n) \ (A2 . n);
existence
ex b1 being SetSequence of X st
for n being Element of NAT holds b1 . n = (A1 . n) \ (A2 . n)
uniqueness
for b1, b2 being SetSequence of X st ( for n being Element of NAT holds b1 . n = (A1 . n) \ (A2 . n) ) & ( for n being Element of NAT holds b2 . n = (A1 . n) \ (A2 . n) ) holds
b1 = b2
func A1 (\+\) A2 -> SetSequence of
X means :
Def4:
:: SETLIM_2:def 4
for
n being
Element of
NAT holds
it . n = (A1 . n) \+\ (A2 . n);
existence
ex b1 being SetSequence of X st
for n being Element of NAT holds b1 . n = (A1 . n) \+\ (A2 . n)
uniqueness
for b1, b2 being SetSequence of X st ( for n being Element of NAT holds b1 . n = (A1 . n) \+\ (A2 . n) ) & ( for n being Element of NAT holds b2 . n = (A1 . n) \+\ (A2 . n) ) holds
b1 = b2
commutativity
for b1, A1, A2 being SetSequence of X st ( for n being Element of NAT holds b1 . n = (A1 . n) \+\ (A2 . n) ) holds
for n being Element of NAT holds b1 . n = (A2 . n) \+\ (A1 . n)
;
end;
:: deftheorem Def1 defines (/\) SETLIM_2:def 1 :
:: deftheorem Def2 defines (\/) SETLIM_2:def 2 :
:: deftheorem Def3 defines (\) SETLIM_2:def 3 :
:: deftheorem Def4 defines (\+\) SETLIM_2:def 4 :
theorem Th3: :: SETLIM_2:3
theorem Th4: :: SETLIM_2:4
theorem Th5: :: SETLIM_2:5
theorem Th6: :: SETLIM_2:6
theorem Th7: :: SETLIM_2:7
theorem Th8: :: SETLIM_2:8
theorem Th9: :: SETLIM_2:9
theorem Th10: :: SETLIM_2:10
theorem Th11: :: SETLIM_2:11
theorem Th12: :: SETLIM_2:12
theorem Th13: :: SETLIM_2:13
theorem Th14: :: SETLIM_2:14
:: deftheorem Def5 defines (/\) SETLIM_2:def 5 :
:: deftheorem Def6 defines (\/) SETLIM_2:def 6 :
:: deftheorem Def7 defines (\) SETLIM_2:def 7 :
:: deftheorem Def8 defines (\) SETLIM_2:def 8 :
:: deftheorem Def9 defines (\+\) SETLIM_2:def 9 :
theorem :: SETLIM_2:15
theorem Th16: :: SETLIM_2:16
theorem Th17: :: SETLIM_2:17
theorem Th18: :: SETLIM_2:18
theorem Th19: :: SETLIM_2:19
theorem Th20: :: SETLIM_2:20
theorem Th21: :: SETLIM_2:21
theorem Th22: :: SETLIM_2:22
theorem :: SETLIM_2:23
theorem Th24: :: SETLIM_2:24
theorem Th25: :: SETLIM_2:25
theorem :: SETLIM_2:26
theorem Th27: :: SETLIM_2:27
theorem Th28: :: SETLIM_2:28
theorem :: SETLIM_2:29
theorem Th30: :: SETLIM_2:30
theorem Th31: :: SETLIM_2:31
theorem :: SETLIM_2:32
theorem Th33: :: SETLIM_2:33
theorem Th34: :: SETLIM_2:34
theorem Th35: :: SETLIM_2:35
theorem Th36: :: SETLIM_2:36
theorem Th37: :: SETLIM_2:37
theorem Th38: :: SETLIM_2:38
theorem Th39: :: SETLIM_2:39
theorem Th40: :: SETLIM_2:40
theorem Th41: :: SETLIM_2:41
theorem Th42: :: SETLIM_2:42
theorem :: SETLIM_2:43
theorem :: SETLIM_2:44
theorem :: SETLIM_2:45
theorem :: SETLIM_2:46
theorem :: SETLIM_2:47
theorem :: SETLIM_2:48
theorem :: SETLIM_2:49
theorem Th50: :: SETLIM_2:50
theorem Th51: :: SETLIM_2:51
theorem :: SETLIM_2:52
theorem Th53: :: SETLIM_2:53
theorem :: SETLIM_2:54
theorem Th55: :: SETLIM_2:55
theorem Th56: :: SETLIM_2:56
theorem :: SETLIM_2:57
theorem Th58: :: SETLIM_2:58
theorem :: SETLIM_2:59
theorem Th60: :: SETLIM_2:60
theorem Th61: :: SETLIM_2:61
theorem Th62: :: SETLIM_2:62
theorem Th63: :: SETLIM_2:63
theorem Th64: :: SETLIM_2:64
theorem Th65: :: SETLIM_2:65
theorem Th66: :: SETLIM_2:66
theorem Th67: :: SETLIM_2:67
theorem Th68: :: SETLIM_2:68
theorem Th69: :: SETLIM_2:69
theorem :: SETLIM_2:70
theorem Th71: :: SETLIM_2:71
theorem Th72: :: SETLIM_2:72
theorem Th73: :: SETLIM_2:73
theorem Th74: :: SETLIM_2:74
theorem Th75: :: SETLIM_2:75
theorem Th76: :: SETLIM_2:76
theorem Th77: :: SETLIM_2:77
theorem Th78: :: SETLIM_2:78
theorem Th79: :: SETLIM_2:79
theorem Th80: :: SETLIM_2:80
theorem Th81: :: SETLIM_2:81
theorem Th82: :: SETLIM_2:82
theorem Th83: :: SETLIM_2:83
theorem Th84: :: SETLIM_2:84
theorem Th85: :: SETLIM_2:85
theorem Th86: :: SETLIM_2:86
theorem Th87: :: SETLIM_2:87
theorem :: SETLIM_2:88
theorem :: SETLIM_2:89
theorem :: SETLIM_2:90
theorem :: SETLIM_2:91
theorem :: SETLIM_2:92
theorem :: SETLIM_2:93
theorem :: SETLIM_2:94
theorem :: SETLIM_2:95
theorem :: SETLIM_2:96