:: 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-2017 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies SUBSET_1, NUMBERS, PROB_1, SETLIM_1, FUNCT_1, EQREL_1, NAT_1,
XXREAL_0, SETFAM_1, RELAT_1, CARD_3, TARSKI, XBOOLE_0, ARYTM_3, CARD_1,
SEQM_3, ORDINAL2, SEQ_2, SETLIM_2;
notations TARSKI, SUBSET_1, FUNCT_1, ORDINAL1, NUMBERS, XCMPLX_0, NAT_1,
SETFAM_1, KURATO_0, PROB_1, SETLIM_1, XXREAL_0;
constructors SETFAM_1, NAT_1, KURATO_0, SETLIM_1, XREAL_0, RELSET_1;
registrations SUBSET_1, RELSET_1, XREAL_0, ORDINAL1, FUNCT_2, NAT_1;
requirements NUMERALS, SUBSET, ARITHM;
begin
reserve n,m,k for Nat,
x,X for set,
A for Subset of X,
A1,A2 for SetSequence of X;
theorem :: SETLIM_2:1
(inferior_setsequence(A1)).n = Intersection (A1 ^\n);
theorem :: SETLIM_2:2
(superior_setsequence(A1)).n = Union (A1 ^\n);
definition
let X;
let A1,A2 be SetSequence of X;
func A1 (/\) A2 -> SetSequence of X means
:: SETLIM_2:def 1
for n holds it.n = A1.n /\ A2.n;
commutativity;
func A1 (\/) A2 -> SetSequence of X means
:: SETLIM_2:def 2
for n holds it.n = A1.n \/ A2.n;
commutativity;
func A1 (\) A2 -> SetSequence of X means
:: SETLIM_2:def 3
for n holds it.n = A1.n \ A2 .n;
func A1 (\+\) A2 -> SetSequence of X means
:: SETLIM_2:def 4
for n holds it.n = A1.n \+\ A2.n;
commutativity;
end;
theorem :: SETLIM_2:3
A1 (\+\) A2 = (A1 (\) A2) (\/) (A2 (\) A1);
theorem :: SETLIM_2:4
(A1 (/\) A2) ^\k = (A1 ^\k) (/\) (A2 ^\k);
theorem :: SETLIM_2:5
(A1 (\/) A2) ^\k = (A1 ^\k) (\/) (A2 ^\k);
theorem :: SETLIM_2:6
(A1 (\) A2) ^\k = (A1 ^\k) (\) (A2 ^\k);
theorem :: SETLIM_2:7
(A1 (\+\) A2) ^\k = (A1 ^\k) (\+\) (A2 ^\k);
theorem :: SETLIM_2:8
Union (A1 (/\) A2) c= Union A1 /\ Union A2;
theorem :: SETLIM_2:9
Union (A1 (\/) A2) = Union A1 \/ Union A2;
theorem :: SETLIM_2:10
Union A1 \ Union A2 c= Union (A1 (\) A2);
theorem :: SETLIM_2:11
Union A1 \+\ Union A2 c= Union (A1 (\+\) A2);
theorem :: SETLIM_2:12
Intersection (A1 (/\) A2) = Intersection A1 /\ Intersection A2;
theorem :: SETLIM_2:13
Intersection A1 \/ Intersection A2 c= Intersection (A1 (\/) A2);
theorem :: SETLIM_2:14
Intersection (A1 (\) A2) c= Intersection A1 \ Intersection A2;
definition
let X;
let A1 be SetSequence of X, A be Subset of X;
func A (/\) A1 -> SetSequence of X means
:: SETLIM_2:def 5
for n holds it.n = A /\ A1.n;
func A (\/) A1 -> SetSequence of X means
:: SETLIM_2:def 6
for n holds it.n = A \/ A1.n;
func A (\) A1 -> SetSequence of X means
:: SETLIM_2:def 7
for n holds it.n = A \ A1.n;
func A1 (\) A -> SetSequence of X means
:: SETLIM_2:def 8
for n holds it.n = A1.n \ A;
func A (\+\) A1 -> SetSequence of X means
:: SETLIM_2:def 9
for n holds it.n = A \+\ A1 .n;
end;
theorem :: SETLIM_2:15
A (\+\) A1 = (A (\) A1) (\/) (A1 (\) A);
theorem :: SETLIM_2:16
(A (/\) A1) ^\k = A (/\) (A1 ^\k);
theorem :: SETLIM_2:17
(A (\/) A1) ^\k = A (\/) (A1 ^\k);
theorem :: SETLIM_2:18
(A (\) A1) ^\k = A (\) (A1 ^\k);
theorem :: SETLIM_2:19
(A1 (\) A) ^\k = (A1 ^\k) (\) A;
theorem :: SETLIM_2:20
(A (\+\) A1) ^\k = A (\+\) (A1 ^\k);
theorem :: SETLIM_2:21
A1 is non-ascending implies A (/\) A1 is non-ascending;
theorem :: SETLIM_2:22
A1 is non-descending implies A (/\) A1 is non-descending;
theorem :: SETLIM_2:23
A1 is monotone implies A (/\) A1 is monotone;
theorem :: SETLIM_2:24
A1 is non-ascending implies A (\/) A1 is non-ascending;
theorem :: SETLIM_2:25
A1 is non-descending implies A (\/) A1 is non-descending;
theorem :: SETLIM_2:26
A1 is monotone implies A (\/) A1 is monotone;
theorem :: SETLIM_2:27
A1 is non-ascending implies A (\) A1 is non-descending;
theorem :: SETLIM_2:28
A1 is non-descending implies A (\) A1 is non-ascending;
theorem :: SETLIM_2:29
A1 is monotone implies A (\) A1 is monotone;
theorem :: SETLIM_2:30
A1 is non-ascending implies A1 (\) A is non-ascending;
theorem :: SETLIM_2:31
A1 is non-descending implies A1 (\) A is non-descending;
theorem :: SETLIM_2:32
A1 is monotone implies A1 (\) A is monotone;
theorem :: SETLIM_2:33
Intersection (A (/\) A1) = A /\ Intersection A1;
theorem :: SETLIM_2:34
Intersection (A (\/) A1) = A \/ Intersection A1;
theorem :: SETLIM_2:35
Intersection (A (\) A1) c= A \ Intersection A1;
theorem :: SETLIM_2:36
Intersection (A1 (\) A) = Intersection A1 \ A;
theorem :: SETLIM_2:37
Intersection (A (\+\) A1) c= A \+\ Intersection A1;
theorem :: SETLIM_2:38
Union (A (/\) A1) = A /\ Union A1;
theorem :: SETLIM_2:39
Union (A (\/) A1) = A \/ Union A1;
theorem :: SETLIM_2:40
A \ Union A1 c= Union (A (\) A1);
theorem :: SETLIM_2:41
Union (A1 (\) A) = Union A1 \ A;
theorem :: SETLIM_2:42
A \+\ Union A1 c= Union (A (\+\) A1);
theorem :: SETLIM_2:43
(inferior_setsequence(A1 (/\) A2)).n = (inferior_setsequence A1).n /\
(inferior_setsequence A2).n;
theorem :: SETLIM_2:44
(inferior_setsequence A1).n \/ (inferior_setsequence A2).n c= (
inferior_setsequence(A1 (\/) A2)).n;
theorem :: SETLIM_2:45
(inferior_setsequence(A1 (\) A2)).n c= (inferior_setsequence A1).n \ (
inferior_setsequence A2).n;
theorem :: SETLIM_2:46
(superior_setsequence(A1 (/\) A2)).n c= (superior_setsequence A1).n /\
(superior_setsequence A2).n;
theorem :: SETLIM_2:47
(superior_setsequence(A1 (\/) A2)).n = (superior_setsequence A1).n \/
(superior_setsequence A2).n;
theorem :: SETLIM_2:48
(superior_setsequence A1).n \ (superior_setsequence A2).n c= (
superior_setsequence(A1 (\) A2)).n;
theorem :: SETLIM_2:49
(superior_setsequence A1).n \+\ (superior_setsequence A2).n c= (
superior_setsequence(A1 (\+\) A2)).n;
theorem :: SETLIM_2:50
(inferior_setsequence(A (/\) A1)).n = A /\ (inferior_setsequence A1).n;
theorem :: SETLIM_2:51
(inferior_setsequence(A (\/) A1)).n = A \/ (inferior_setsequence A1).n;
theorem :: SETLIM_2:52
(inferior_setsequence(A (\) A1)).n c= A \ (inferior_setsequence A1).n;
theorem :: SETLIM_2:53
(inferior_setsequence(A1 (\) A)).n = (inferior_setsequence A1).n \ A;
theorem :: SETLIM_2:54
(inferior_setsequence(A (\+\) A1)).n c= A \+\ (inferior_setsequence A1 ).n;
theorem :: SETLIM_2:55
(superior_setsequence(A (/\) A1)).n = A /\ (superior_setsequence A1).n;
theorem :: SETLIM_2:56
(superior_setsequence(A (\/) A1)).n = A \/ (superior_setsequence A1).n;
theorem :: SETLIM_2:57
A \ (superior_setsequence A1).n c= (superior_setsequence(A (\) A1)).n;
theorem :: SETLIM_2:58
(superior_setsequence(A1 (\) A)).n = (superior_setsequence A1).n \ A;
theorem :: SETLIM_2:59
A \+\ (superior_setsequence A1).n c= (superior_setsequence(A (\+\) A1) ).n;
theorem :: SETLIM_2:60
lim_inf (A1 (/\) A2) = lim_inf A1 /\ lim_inf A2;
theorem :: SETLIM_2:61
lim_inf A1 \/ lim_inf A2 c= lim_inf (A1 (\/) A2);
theorem :: SETLIM_2:62
lim_inf (A1 (\) A2) c= lim_inf A1 \ lim_inf A2;
theorem :: SETLIM_2:63
A1 is convergent or A2 is convergent implies lim_inf (A1 (\/) A2
) = lim_inf A1 \/ lim_inf A2;
theorem :: SETLIM_2:64
A2 is convergent implies lim_inf (A1 (\) A2) = lim_inf A1 \ lim_inf A2;
theorem :: SETLIM_2:65
A1 is convergent or A2 is convergent implies lim_inf (A1 (\+\)
A2) c= lim_inf A1 \+\ lim_inf A2;
theorem :: SETLIM_2:66
A1 is convergent & A2 is convergent implies lim_inf (A1 (\+\) A2
) = lim_inf A1 \+\ lim_inf A2;
theorem :: SETLIM_2:67
lim_sup (A1 (/\) A2) c= lim_sup A1 /\ lim_sup A2;
theorem :: SETLIM_2:68
lim_sup (A1 (\/) A2) = lim_sup A1 \/ lim_sup A2;
theorem :: SETLIM_2:69
lim_sup A1 \ lim_sup A2 c= lim_sup (A1 (\) A2);
theorem :: SETLIM_2:70
lim_sup A1 \+\ lim_sup A2 c= lim_sup (A1 (\+\) A2);
theorem :: SETLIM_2:71
A1 is convergent or A2 is convergent implies lim_sup (A1 (/\) A2
) = lim_sup A1 /\ lim_sup A2;
theorem :: SETLIM_2:72
A2 is convergent implies lim_sup (A1 (\) A2) = lim_sup A1 \ lim_sup A2;
theorem :: SETLIM_2:73
A1 is convergent & A2 is convergent implies lim_sup (A1 (\+\) A2
) = lim_sup A1 \+\ lim_sup A2;
theorem :: SETLIM_2:74
lim_inf (A (/\) A1) = A /\ lim_inf A1;
theorem :: SETLIM_2:75
lim_inf (A (\/) A1) = A \/ lim_inf A1;
theorem :: SETLIM_2:76
lim_inf (A (\) A1) c= A \ lim_inf A1;
theorem :: SETLIM_2:77
lim_inf (A1 (\) A) = lim_inf A1 \ A;
theorem :: SETLIM_2:78
lim_inf (A (\+\) A1) c= A \+\ lim_inf A1;
theorem :: SETLIM_2:79
A1 is convergent implies lim_inf (A (\) A1) = A \ lim_inf A1;
theorem :: SETLIM_2:80
A1 is convergent implies lim_inf (A (\+\) A1) = A \+\ lim_inf A1;
theorem :: SETLIM_2:81
lim_sup (A (/\) A1) = A /\ lim_sup A1;
theorem :: SETLIM_2:82
lim_sup (A (\/) A1) = A \/ lim_sup A1;
theorem :: SETLIM_2:83
A \ lim_sup A1 c= lim_sup (A (\) A1);
theorem :: SETLIM_2:84
lim_sup (A1 (\) A) = lim_sup A1 \ A;
theorem :: SETLIM_2:85
A \+\ lim_sup A1 c= lim_sup (A (\+\) A1);
theorem :: SETLIM_2:86
A1 is convergent implies lim_sup (A (\) A1) = A \ lim_sup A1;
theorem :: SETLIM_2:87
A1 is convergent implies lim_sup (A (\+\) A1) = A \+\ lim_sup A1;
theorem :: SETLIM_2:88
A1 is convergent & A2 is convergent implies (A1 (/\) A2) is convergent
& lim (A1 (/\) A2) = lim A1 /\ lim A2;
theorem :: SETLIM_2:89
A1 is convergent & A2 is convergent implies (A1 (\/) A2) is convergent
& lim (A1 (\/) A2) = lim A1 \/ lim A2;
theorem :: SETLIM_2:90
A1 is convergent & A2 is convergent implies (A1 (\) A2) is convergent
& lim (A1 (\) A2) = lim A1 \ lim A2;
theorem :: SETLIM_2:91
A1 is convergent & A2 is convergent implies (A1 (\+\) A2) is
convergent & lim (A1 (\+\) A2) = lim A1 \+\ lim A2;
theorem :: SETLIM_2:92
A1 is convergent implies (A (/\) A1) is convergent & lim (A (/\) A1) =
A /\ lim A1;
theorem :: SETLIM_2:93
A1 is convergent implies (A (\/) A1) is convergent & lim (A (\/) A1) =
A \/ lim A1;
theorem :: SETLIM_2:94
A1 is convergent implies (A (\) A1) is convergent & lim (A (\) A1) = A
\ lim A1;
theorem :: SETLIM_2:95
A1 is convergent implies (A1 (\) A) is convergent & lim (A1 (\) A) =
lim A1 \ A;
theorem :: SETLIM_2:96
A1 is convergent implies (A (\+\) A1) is convergent & lim (A (\+\) A1)
= A \+\ lim A1;