:: 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-2021 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;