:: Limit of Sequence of Subsets :: by Bo Zhang , Hiroshi Yamazaki and Yatsuka Nakamura :: :: Received March 15, 2005 :: Copyright (c) 2005-2018 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, XXREAL_0, ARYTM_3, FUNCT_1, XBOOLE_0, TARSKI, NAT_1, RELAT_1, CARD_1, SETFAM_1, EQREL_1, CARD_3, ZFMISC_1, SEQM_3, ORDINAL2, SEQ_2, SETLIM_1; notations ORDINAL1, NUMBERS, XXREAL_0, XCMPLX_0, NAT_1, RELAT_1, FUNCT_1, TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELSET_1, SETFAM_1, PROB_1, FUNCT_2, KURATO_0; constructors SETFAM_1, NAT_1, KURATO_0, XREAL_0, RELSET_1, FINSUB_1, PROB_2; registrations XBOOLE_0, SUBSET_1, ORDINAL1, XREAL_0, FUNCT_2, RELAT_1, PROB_1, RELSET_1, NAT_1; requirements NUMERALS, BOOLE, SUBSET; definitions TARSKI; equalities SUBSET_1; expansions TARSKI; theorems FUNCT_1, FUNCT_2, PROB_1, NAT_1, TARSKI, XBOOLE_0, XBOOLE_1, XCMPLX_1, SETFAM_1, ZFMISC_1, CARD_3, KURATO_0, PROB_2, XREAL_1, ORDINAL1, VALUED_0, RELAT_1; schemes NAT_1, FUNCT_1; begin reserve n,m,k,k1,k2,i,j for Nat; reserve x,y,z for object,X,Y,Z for set; reserve A for Subset of X; reserve B,A1,A2,A3 for SetSequence of X; reserve Si for SigmaField of X; reserve S,S1,S2,S3 for SetSequence of Si; Lm1: for i,j being Nat holds i <= j implies i = j or i + 1 <= j proof let i,j be Nat; assume i<=j; then i + 1 <= j + 1 by XREAL_1:6; hence thesis by NAT_1:8,XCMPLX_1:2; end; theorem Th1: for f be sequence of Y holds f.(n + m) in {f.k: n <= k} proof n <= n + m by NAT_1:11; hence thesis; end; theorem Th2: for f being sequence of Y holds {f.k1: n <= k1} = {f.k2 : n+1 <=k2} \/ {f.n} proof let f be sequence of Y; set Z1 = {f.k1:n <= k1}; set Z2 = {f.k2:(n+1) <= k2}; A1: Z2 \/ {f.n} c= Z1 proof let x be object; assume A2: x in Z2 \/ {f.n}; now per cases by A2,XBOOLE_0:def 3; case x in Z2; then consider z such that A3: x = z and A4: z in Z2; consider k11 being Nat such that A5: z=f.k11 and A6: n+1 <= k11 by A4; n <= k11 by A6,NAT_1:13; hence thesis by A3,A5; end; case x in {f.n}; then x = f.n by TARSKI:def 1; hence thesis; end; end; hence thesis; end; {f.k1: n <= k1} c= {f.k2 : n+1 <= k2} \/ {f.n} proof let x be object; assume x in Z1; then consider z such that A7: x=z and A8: z in Z1; consider k such that A9: z = f.k & n <= k by A8; z = f.k & n+1 <= k or z = f.k & n = k by A9,Lm1; then z in Z2 or z in {f.n} by TARSKI:def 1; hence thesis by A7,XBOOLE_0:def 3; end; hence thesis by A1,XBOOLE_0:def 10; end; theorem Th3: for f be sequence of Y holds (for k1 holds x in f.(n+k1)) iff for Z st Z in {f.k2 : n <= k2} holds x in Z proof let f be sequence of Y; set Z = {f.k2 : n <= k2}; now assume A1: for k1 holds x in f.(n+k1); now let Z1 be set; assume Z1 in Z; then consider k1 being Nat such that A2: Z1=f.k1 and A3: n <= k1; ex m be Nat st k1 = n + m by A3,NAT_1:10; then consider k2 being Nat such that A4: Z1=f.(n + k2) by A2; thus x in Z1 by A1,A4; end; hence for Z1 being set st Z1 in {f.k2 : n <= k2} holds x in Z1; end; hence thesis by Th1; end; theorem Th4: for Y being non empty set for f being sequence of Y holds x in rng f iff ex n st x = f.n proof let Y be non empty set; let f be sequence of Y; thus x in rng f implies ex n st x = f.n proof assume x in rng f; then consider y being object such that A1: y in dom f and A2: x = f.y by FUNCT_1:def 3; reconsider m=y as Element of NAT by A1; take m; thus thesis by A2; end; given n such that A3: x = f.n; A4: n in NAT by ORDINAL1:def 12; dom f = NAT by FUNCT_2:def 1; hence thesis by A3,FUNCT_1:def 3,A4; end; theorem Th5: for Y be non empty set for f being sequence of Y holds rng f = {f.k : 0 <= k} proof let Y be non empty set; let f be sequence of Y; set Z = {f.k : 0 <= k}; A1: dom f = NAT by FUNCT_2:def 1; A2: rng f c= Z proof let y be object; assume y in rng f; then consider n be object such that A3: n in NAT and A4: y = f.n by A1,FUNCT_1:def 3; reconsider n as Element of NAT by A3; 0 <= n by NAT_1:2; hence thesis by A4; end; Z c= rng f proof let x be object; assume x in Z; then consider n1 being Nat such that A5: x=f.n1 & 0 <= n1; n1 in NAT by ORDINAL1:def 12; hence thesis by FUNCT_2:4,A5; end; hence thesis by A2,XBOOLE_0:def 10; end; theorem Th6: for Y being non empty set for f being sequence of Y holds rng (f ^\ k) = {f.n: k <= n} proof let Y be non empty set; let f be sequence of Y; reconsider f1 = f ^\ k as sequence of Y; rng f1 = {f.m: k <= m} proof set Z = {f.m : k <= m}; A1: dom f1 = NAT by FUNCT_2:def 1; A2: rng f1 c= Z proof let y be object; assume y in rng f1; then consider m1 be object such that A3: m1 in NAT and A4: y = f1.m1 by A1,FUNCT_1:def 3; reconsider m1 as Element of NAT by A3; y = f.(k+m1) by A4,NAT_1:def 3; hence thesis by Th1; end; Z c= rng f1 proof let x be object; assume x in Z; then consider k1 being Nat such that A5: x = f.k1 and A6: k <= k1; consider k2 being Nat such that A7: k1 = k + k2 by A6,NAT_1:10; k2 in NAT & x = f1.k2 by A5,A7,NAT_1:def 3,ORDINAL1:def 12; hence thesis by FUNCT_2:4; end; hence thesis by A2,XBOOLE_0:def 10; end; hence thesis; end; theorem Th7: x in meet rng B iff for n being Nat holds x in B.n proof A1: dom B = NAT by FUNCT_2:def 1; A2: now let x; assume A3: for n being Nat holds x in B.n; now let Y; assume Y in rng B; then consider n be object such that A4: n in NAT and A5: Y = B.n by A1,FUNCT_1:def 3; thus x in Y by A3,A4,A5; end; hence x in meet rng B by SETFAM_1:def 1; end; now let x; assume A6: x in meet rng B; now let k be Nat; k in NAT by ORDINAL1:def 12; then B.k in rng B by FUNCT_2:4; hence x in B.k by A6,SETFAM_1:def 1; end; hence for n being Nat holds x in B.n; end; hence thesis by A2; end; theorem Th8: Intersection B = meet rng B proof now let x be object; assume x in meet rng B; then for n being Nat holds x in B.n by Th7; hence x in Intersection B by PROB_1:13; end; then A1: meet rng B c= Intersection B; Intersection B c= meet rng B proof let x be object; assume x in Intersection B; then for n being Nat holds x in B.n by PROB_1:13; hence thesis by Th7; end; hence thesis by A1,XBOOLE_0:def 10; end; theorem Intersection B c= Union B proof meet rng B c= union rng B by SETFAM_1:2; then Intersection B c= union rng B by Th8; hence thesis by CARD_3:def 4; end; theorem Th10: (for n holds B.n = A) implies Union B = A proof assume A1: for n holds B.n = A; now let x be object; assume x in rng B; then ex n st x = B.n by Th4; hence x = A by A1; end; then rng B = {A} by ZFMISC_1:35; then union rng B = A by ZFMISC_1:25; hence thesis by CARD_3:def 4; end; theorem Th11: (for n holds B.n = A) implies Intersection B = A proof assume A1: for n holds B.n = A; now let x be object; assume x in rng B; then ex n st x = B.n by Th4; hence x = A by A1; end; then rng B = {A} by ZFMISC_1:35; then meet rng B = A by SETFAM_1:10; hence thesis by Th8; end; theorem B is constant implies Union B = Intersection B proof assume B is constant; then consider A being Subset of X such that A1: for n being Nat holds B.n = A by VALUED_0:def 18; Union B = A by Th10,A1; hence thesis by Th11,A1; end; Lm2: B is constant & the_value_of B = A implies for n holds B.n = A & Union B = A & Intersection B = A proof assume that A1: B is constant and A2: the_value_of B = A; consider x being set such that A3: x in dom B and A4: A = B.x by A1,A2,FUNCT_1:def 12; A5: dom B = NAT by FUNCT_2:def 1; for n holds B.n = A proof let n; reconsider n as Element of NAT by ORDINAL1:def 12; B.n = A by A1,A3,A4,FUNCT_1:def 10,A5; hence thesis; end; hence thesis by Th10,Th11; end; theorem Th13: B is constant & the_value_of B = A implies for n holds union {B. k: n <= k} = A proof assume A1: B is constant & the_value_of B = A; let n; set Y = {B.k : n <= k}; A2: now let x be object; assume x in Y; then ex k st x = B.k & n <= k; hence x = A by A1,Lm2; end; Y <> {} by Th1; then Y = {A} by A2,ZFMISC_1:35; hence thesis by ZFMISC_1:25; end; theorem Th14: B is constant & the_value_of B = A implies for n holds meet {B.k : n <= k} = A proof assume A1: B is constant & the_value_of B = A; let n; set Y = {B.k : n <= k}; A2: now let x be object; assume x in Y; then ex k st x = B.k & n <= k; hence x = A by A1,Lm2; end; Y <> {} by Th1; then Y = {A} by A2,ZFMISC_1:35; hence thesis by SETFAM_1:10; end; theorem Th15: for X, B for f being Function st dom f = NAT & for n holds f.n = meet {B.k: n <= k} holds f is SetSequence of X proof let X, B; let f be Function such that A1: dom f = NAT and A2: for n holds f.n = meet {B.k: n <= k}; rng f c= bool X proof let z be object; assume z in rng f; then consider x being object such that A3: x in dom f and A4: z = f.x by FUNCT_1:def 3; reconsider n = x as Element of NAT by A1,A3; set Y = {B.k: n <= k}; set y = meet Y; A5: y is Subset of X proof per cases; suppose Y<>{}; then consider Z1 being object such that A6: Z1 in Y by XBOOLE_0:def 1; reconsider Z1 as set by TARSKI:1; consider k1 being Nat such that A7: Z1 = B.k1 & n <= k1 by A6; reconsider k1 as Element of NAT by ORDINAL1:def 12; now let x be object; assume x in y; then x in Z1 by A6,SETFAM_1:def 1; then x in B.k1 by A7; hence x in X; end; hence thesis by TARSKI:def 3; end; suppose Y = {}; then y = {} by SETFAM_1:def 1; hence thesis by XBOOLE_1:2; end; end; z = y by A2,A4; hence thesis by A5; end; hence thesis by A1,FUNCT_2:2; end; theorem Th16: for X being set, B being SetSequence of X for f being Function st dom f = NAT & for n holds f.n = union {B.k: n <= k} holds f is sequence of bool X proof let X be set, B be SetSequence of X; let f be Function such that A1: dom f = NAT and A2: for n holds f.n = union {B.k: n <= k}; rng f c= bool X proof let z be object; assume z in rng f; then consider x being object such that A3: x in dom f and A4: z = f.x by FUNCT_1:def 3; reconsider n = x as Nat by A1,A3; set Y = {B.k: n <= k}; set y = union Y; now let z be object; assume z in y; then ex Z st z in Z & Z in Y by TARSKI:def 4; then consider Z1 be set such that A5: Z1 in Y and A6: z in Z1; consider k1 such that A7: Z1 = B.k1 & n <= k1 by A5; reconsider k1 as Element of NAT by ORDINAL1:def 12; Z1 = B.k1 by A7; hence z in X by A6; end; then A8: y is Subset of X by TARSKI:def 3; z = y by A2,A4; hence thesis by A8; end; hence thesis by A1,FUNCT_2:2; end; definition let X,B; attr B is monotone means B is non-descending or B is non-ascending; end; definition let B be Function; func inferior_setsequence B -> Function means :Def2: dom it = NAT & for n holds it.n = meet {B.k : n <= k}; existence proof deffunc F(Nat) = meet {B.k : \$1 <= k}; consider f being Function such that A1: dom f = NAT & for n being Element of NAT holds f.n = F(n) from FUNCT_1:sch 4; take f; thus dom f = NAT by A1; let n be Nat; n in NAT by ORDINAL1:def 12; hence thesis by A1; end; uniqueness proof let BSeq,CSeq be Function such that A2: dom BSeq = NAT & for n holds BSeq.n = meet {B.k : n <= k} and A3: dom CSeq = NAT & for m holds CSeq.m = meet {B.k : m <= k}; for y being object st y in NAT holds BSeq.y = CSeq.y proof let y be object; assume y in NAT; then reconsider y as Nat; set Y = {B.k: y <= k}; BSeq.y = meet Y by A2; hence thesis by A3; end; hence thesis by A2,A3,FUNCT_1:2; end; end; definition let X be set, B be SetSequence of X; redefine func inferior_setsequence B -> SetSequence of X; coherence proof A1: for n be Nat holds (inferior_setsequence B).n = meet {B.k : n <= k} by Def2; dom inferior_setsequence B = NAT by Def2; hence thesis by A1,Th15; end; end; definition let B be Function; func superior_setsequence B -> Function means :Def3: dom it = NAT & for n holds it.n = union {B.k : n <= k}; existence proof deffunc F(Nat) = union {B.k : \$1 <= k}; consider f being Function such that A1: dom f = NAT & for n be Element of NAT holds f. n = F(n) from FUNCT_1:sch 4; take f; thus dom f = NAT by A1; let n be Nat; n in NAT by ORDINAL1:def 12; hence thesis by A1; end; uniqueness proof let BSeq,CSeq be Function such that A2: dom BSeq = NAT & for n holds BSeq.n = union {B.k : n <= k} and A3: dom CSeq = NAT & for m holds CSeq.m = union {B.k : m <= k}; for y being object st y in NAT holds BSeq.y = CSeq.y proof let y be object; assume y in NAT; then reconsider y as Nat; set Y = {B.k: y <= k}; BSeq.y = union Y by A2; hence thesis by A3; end; hence thesis by A2,A3,FUNCT_1:2; end; end; definition let X be set, B be SetSequence of X; redefine func superior_setsequence B -> SetSequence of X; coherence proof A1: for n holds (superior_setsequence B).n = union {B.k : n <= k} by Def3; dom superior_setsequence B = NAT by Def3; hence thesis by A1,Th16; end; end; theorem Th17: (inferior_setsequence B).0 = Intersection B proof (inferior_setsequence B).0 = meet {B.k : k >= 0} by Def2 .= meet rng B by Th5 .= Intersection B by Th8; hence thesis; end; theorem Th18: (superior_setsequence B).0 = Union B proof (superior_setsequence B).0 = union {B.k : 0 <= k} by Def3 .= union rng B by Th5 .= Union B by CARD_3:def 4; hence thesis; end; theorem Th19: for n being Nat holds x in (inferior_setsequence B).n iff for k being Nat holds x in B.(n+k) proof let n be Nat; reconsider nn=n as Nat; set Y = {B.k : nn <= k}; A1: (inferior_setsequence B).n = meet {B.k : n <= k} by Def2; A2: now assume A3: x in (inferior_setsequence B).n; now let k be Nat; B.(n + k) in Y by Th1; hence x in B.(n + k) by A1,A3,SETFAM_1:def 1; end; hence for k being Nat holds x in B.(n+k); end; A4: Y <> {} by Th1; now assume for k holds x in B.(n+k); then for Z st Z in Y holds x in Z by Th3; hence x in (inferior_setsequence B).n by A1,A4,SETFAM_1:def 1; end; hence thesis by A2; end; theorem Th20: for n being Nat holds x in (superior_setsequence B).n iff ex k being Nat st x in B.(n + k) proof let n be Nat; set Y = {B.k : n <= k}; A1: (superior_setsequence B).n = union {B.k : n <= k} by Def3; thus x in (superior_setsequence B).n implies ex k being Nat st x in B.(n + k) proof assume x in (superior_setsequence B).n; then consider Y1 being set such that A2: x in Y1 and A3: Y1 in Y by A1,TARSKI:def 4; consider k11 being Nat such that A4: Y1 = B.k11 and A5: n <= k11 by A3; ex k be Nat st k11 = n + k by A5,NAT_1:10; then consider k22 being Nat such that A6: Y1=B.(n + k22) by A4; thus thesis by A2,A6; end; now given k1 being Nat such that A7: x in B.(n + k1); B.(n+k1) in Y by Th1; hence x in (superior_setsequence B).n by A1,A7,TARSKI:def 4; end; hence thesis; end; theorem Th21: for n being Nat holds (inferior_setsequence B).n = (inferior_setsequence B).(n+1) /\ B .n proof let n be Nat; A1: (inferior_setsequence B).n = meet {B.k1 : n <= k1} by Def2; A2: {B.k1: n <= k1} = {B.k2 : n+1 <=k2} \/ {B.n} by Th2; A3: (inferior_setsequence B).(n+1) = meet {B.k2 : n+1 <= k2} by Def2; A4: {B.k1 : n <= k1} <> {} by Th1; A5: now let x be object; assume that A6: x in (inferior_setsequence B).(n+1) and A7: x in B.n; for Z st Z in {B.k2 : n <= k2} holds x in Z proof let Z; assume Z in {B.k1 : n <= k1}; then consider Z1 being set such that A8: Z=Z1 & Z1 in {B.k1 : n <= k1}; consider k11 being Nat such that A9: Z1=B.k11 & n <= k11 by A8; now per cases by A9,Lm1; suppose Z1=B.k11 & n = k11; hence x in Z1 by A7; end; suppose Z1=B.k11 & n+1 <= k11; then Z1 in {B.k2 : n+1 <= k2}; hence x in Z1 by A3,A6,SETFAM_1:def 1; end; end; hence thesis by A8; end; then x in meet {B.k2 : n <= k2} by A4,SETFAM_1:def 1; hence x in (inferior_setsequence B).n by Def2; end; {B.k2 : n+1 <= k2} <> {} by Th1; then A10: (inferior_setsequence B).(n) c= (inferior_setsequence B).(n+1) by A1,A3,A2 ,SETFAM_1:6,XBOOLE_1:7; now let x be object; A11: B.n in {B.k1 : n <= k1}; assume x in (inferior_setsequence B).n; hence x in (inferior_setsequence B).(n+1) & x in B.n by A1,A10,A11, SETFAM_1:def 1; end; hence (inferior_setsequence B).n = (inferior_setsequence B).(n+1) /\ B.n by A5, XBOOLE_0:def 4; end; theorem Th22: for n being Nat holds (superior_setsequence B).n = (superior_setsequence B).(n+1) \/ B .n proof let n be Nat; {B.k1: n <= k1} = {B.k2 : n+1 <=k2} \/ {B.n} by Th2; then union {B.k2 : n+1 <= k2} c= union {B.k1 : n <= k1} by XBOOLE_1:7 ,ZFMISC_1:77; then (superior_setsequence B).(n+1) c= union {B.k1 : n <= k1} by Def3; then A1: (superior_setsequence B).(n+1) c= (superior_setsequence B).n by Def3; A2: now let x be object; assume A3: x in (superior_setsequence B).(n+1) or x in B.n; thus x in (superior_setsequence B).n proof now per cases by A3; case x in (superior_setsequence B).(n+1); hence thesis by A1; end; case A4: x in B.n; B.n in {B.k1 : n <= k1}; then x in union {B.k1 : n <= k1} by A4,TARSKI:def 4; hence thesis by Def3; end; end; hence thesis; end; end; now let x be object; assume x in (superior_setsequence B).n; then x in union {B.k1 : n <= k1} by Def3; then consider Y1 being set such that A5: x in Y1 & Y1 in {B.k1 : n <= k1} by TARSKI:def 4; consider k11 being Nat such that A6: Y1=B.k11 & n <= k11 by A5; now per cases by A6,Lm1; case Y1=B.k11 & n = k11; hence x in B.n by A5; end; case Y1=B.k11 & n+1 <= k11; then Y1 in {B.k2 : n+1 <= k2}; hence x in union {B.k2 : n+1 <= k2} by A5,TARSKI:def 4; end; end; hence x in B.n or x in (superior_setsequence B).(n+1) by Def3; end; then for x being object holds x in (superior_setsequence B).n iff x in B.n or x in ( superior_setsequence B).(n+1) by A2; hence (superior_setsequence B).n = (superior_setsequence B).(n+1) \/ B.n by XBOOLE_0:def 3; end; theorem Th23: inferior_setsequence B is non-descending proof now let n be Nat; (inferior_setsequence B).n = (inferior_setsequence B).(n+1) /\ B.n by Th21; hence (inferior_setsequence B).n c= (inferior_setsequence B).(n+1) by XBOOLE_1:17; end; hence thesis by PROB_2:7; end; theorem Th24: superior_setsequence B is non-ascending proof now let n be Nat; (superior_setsequence B).n = (superior_setsequence B).(n+1) \/ B.n by Th22; hence (superior_setsequence B).(n+1) c= (superior_setsequence B).n by XBOOLE_1:7; end; hence thesis by PROB_2:6; end; theorem inferior_setsequence B is monotone & superior_setsequence B is monotone by Th23,Th24; registration let X be set, A be SetSequence of X; cluster inferior_setsequence A -> non-descending for SetSequence of X; coherence by Th23; end; registration let X be set, A be SetSequence of X; cluster superior_setsequence A -> non-ascending for SetSequence of X; coherence by Th24; end; theorem Intersection B c= (inferior_setsequence B).n proof 0 <= n by NAT_1:2; then (inferior_setsequence B).0 c= (inferior_setsequence B).n by PROB_1:def 5 ; hence thesis by Th17; end; theorem (superior_setsequence B).n c= Union B proof 0 <= n by NAT_1:2; then (superior_setsequence B).n c= (superior_setsequence B).0 by PROB_1:def 4 ; hence thesis by Th18; end; theorem Th28: for B,n holds {B.k: n <= k} is Subset-Family of X proof let B,n; set Y1 = {B.k: n <= k}; Y1 c= bool X proof let x be object; assume x in Y1; then consider k such that A1: x = B.k & n <= k; reconsider k as Element of NAT by ORDINAL1:def 12; x = B.k by A1; hence thesis; end; hence thesis; end; theorem Union B = (Intersection Complement B)` proof (Intersection Complement B)` = (Union Complement Complement B)`` by PROB_1:def 3 .= Union B; hence thesis; end; theorem Th30: for n being Element of NAT holds (inferior_setsequence B).n = ((superior_setsequence Complement B ).n)` proof let n be Element of NAT; set Y1 = {B.k1: n <= k1}; set Y2 = {(Complement B).k2 : n <= k2}; set Y3 = {(B.k)` where k is Element of NAT: n <= k}; A1: Y3 c= Y2 proof let y be object; assume y in Y3; then consider k being Element of NAT such that A2: y = (B.k)` and A3: n <= k; y = (Complement B).k by A2,PROB_1:def 2; hence thesis by A3; end; Y2 c= Y3 proof let x be object; assume x in Y2; then consider k such that A4: x = (Complement B).k and A5: n <= k; reconsider k as Element of NAT by ORDINAL1:def 12; x = (B.k)` by A4,PROB_1:def 2; hence thesis by A5; end; then A6: Y2 = Y3 by A1,XBOOLE_0:def 10; A7: Y1 <> {} by Th1; reconsider Y1 as Subset-Family of X by Th28; A8: COMPLEMENT Y1 c= Y3 proof let y be object; assume A9: y in COMPLEMENT Y1; then reconsider y as Subset of X; y` in Y1 by A9,SETFAM_1:def 7; then consider k such that A10: y` = B.k and A11: n <= k; reconsider k as Element of NAT by ORDINAL1:def 12; y = (B.k)` by A10; hence thesis by A11; end; Y3 c= COMPLEMENT Y1 proof let x be object; assume x in Y3; then consider k being Element of NAT such that A12: x = (B.k)` and A13: n <= k; reconsider z = B.k as Subset of X; (z`)` in Y1 by A13; hence thesis by A12,SETFAM_1:def 7; end; then Y3 = COMPLEMENT Y1 by A8,XBOOLE_0:def 10; then (superior_setsequence(Complement B)).n = union COMPLEMENT Y1 by A6,Def3 .= [#] X \ meet Y1 by A7,SETFAM_1:34 .= (meet Y1)`; hence thesis by Def2; end; theorem for n being Element of NAT holds (superior_setsequence B).n = ((inferior_setsequence Complement B).n)` proof let n be Element of NAT; reconsider Y = (inferior_setsequence(Complement B)).n as Subset of X; Y = ((superior_setsequence(Complement Complement B)).n)` by Th30 .= ((superior_setsequence B).n)`; hence thesis; end; theorem Th32: Complement (inferior_setsequence B) = (superior_setsequence Complement B) proof reconsider A2 = inferior_setsequence B as SetSequence of X; reconsider A3 = superior_setsequence Complement B as SetSequence of X; now let n be Element of NAT; (A2.n)` = ((A3.n)`)` by Th30; hence (Complement A2).n = A3.n by PROB_1:def 2; end; hence thesis by FUNCT_2:63; end; theorem Complement superior_setsequence B = inferior_setsequence Complement B proof reconsider A2 = inferior_setsequence Complement B as SetSequence of X; Complement A2 = superior_setsequence Complement Complement B by Th32 .= superior_setsequence B; hence thesis; end; theorem (for n being Nat holds A3.n = A1.n \/ A2.n) implies for n being Nat holds ( inferior_setsequence A1).n \/ (inferior_setsequence(A2)).n c= ( inferior_setsequence(A3)).n proof assume A1: for n being Nat holds A3.n = A1.n \/ A2.n; let n be Nat; set X1 = inferior_setsequence A1, X2 = inferior_setsequence A2, X3 = inferior_setsequence A3; now let x be object; assume A2: x in X1.n \/ X2.n; per cases by A2,XBOOLE_0:def 3; suppose A3: x in X1.n; now let k be Nat; x in A1.(n+k) & A3.(n+k) = A1.(n+k) \/ A2.(n+k) by A1,A3,Th19; hence x in A3.(n+k) by XBOOLE_0:def 3; end; hence x in X3.n by Th19; end; suppose A4: x in X2.n; now let k be Nat; x in A2.(n+k) & A3.(n+k) = A1.(n+k) \/ A2.(n+k) by A1,A4,Th19; hence x in A3.(n+k) by XBOOLE_0:def 3; end; hence x in X3.n by Th19; end; end; hence thesis; end; theorem (for n being Nat holds A3.n = A1.n /\ A2.n) implies for n being Nat holds ( inferior_setsequence A3).n = (inferior_setsequence A1).n /\ ( inferior_setsequence A2).n proof assume A1: for n being Nat holds A3.n = A1.n /\ A2.n; let n be Nat; reconsider X3 = inferior_setsequence A3 as SetSequence of X; reconsider X2 = inferior_setsequence A2 as SetSequence of X; set B = A1; reconsider X1 = inferior_setsequence B as SetSequence of X; A2: X1.n /\ X2.n c= X3.n proof let x be object; assume x in (X1.n /\ X2.n); then A3: x in X1.n & x in X2.n by XBOOLE_0:def 4; now let k be Nat; x in B.(n+k) & x in A2.(n+k) by A3,Th19; then x in B.(n+k) /\ A2.(n+k) by XBOOLE_0:def 4; hence x in A3.(n+k) by A1; end; hence thesis by Th19; end; X3.n c= X1.n /\ X2.n proof let x be object; assume A4: x in X3.n; now let k be Nat; x in A3.(n+k) by A4,Th19; then x in (B.(n+k) /\ A2.(n+k)) by A1; hence x in B.(n+k) & x in A2.(n+k) by XBOOLE_0:def 4; end; then x in X1.n & x in X2.n by Th19; hence thesis by XBOOLE_0:def 4; end; hence thesis by A2,XBOOLE_0:def 10; end; theorem (for n holds A3.n = A1.n \/ A2.n) implies for n holds ( superior_setsequence(A3)).n = (superior_setsequence(A1)).n \/ ( superior_setsequence(A2)).n proof assume A1: for n holds A3.n = A1.n \/ A2.n; let n; reconsider X3 = superior_setsequence A3 as SetSequence of X; reconsider X2 = superior_setsequence A2 as SetSequence of X; set B = A1; reconsider X1 = superior_setsequence B as SetSequence of X; A2: X1.n \/ X2.n c= X3.n proof let x be object; assume A3: x in (X1.n \/ X2.n); per cases by A3,XBOOLE_0:def 3; suppose x in X1.n; then consider k being Nat such that A4: x in B.(n+k) by Th20; A3.(n+k) = B.(n+k) \/ A2.(n+k) by A1; then x in A3.(n+k) by A4,XBOOLE_0:def 3; hence thesis by Th20; end; suppose x in X2.n; then consider k being Nat such that A5: x in A2.(n+k) by Th20; A3.(n+k) = B.(n+k) \/ A2.(n+k) by A1; then x in A3.(n+k) by A5,XBOOLE_0:def 3; hence thesis by Th20; end; end; X3.n c= X1.n \/ X2.n proof let x be object; assume x in X3.n; then consider k being Nat such that A6: x in A3.(n+k) by Th20; A7: x in (B.(n+k) \/ A2.(n+k)) by A1,A6; now per cases by A7,XBOOLE_0:def 3; case x in B.(n+k); hence x in X1.n by Th20; end; case x in A2.(n+k); hence x in X2.n by Th20; end; end; hence thesis by XBOOLE_0:def 3; end; hence thesis by A2,XBOOLE_0:def 10; end; theorem (for n holds A3.n = A1.n /\ A2.n) implies for n holds ( superior_setsequence A3).n c= (superior_setsequence A1).n /\ ( superior_setsequence A2).n proof assume A1: for n holds A3.n = A1.n /\ A2.n; let n; reconsider X3 = superior_setsequence A3 as SetSequence of X; reconsider X2 = superior_setsequence A2 as SetSequence of X; set B = A1; reconsider X1 = superior_setsequence B as SetSequence of X; X3.n c= X1.n /\ X2.n proof let x be object; assume x in X3.n; then consider k being Nat such that A2: x in A3.(n+k) by Th20; A3: A3.(n+k) = B.(n+k) /\ A2.(n+k) by A1; then x in A2.(n+k) by A2,XBOOLE_0:def 4; then A4: x in X2.n by Th20; x in B.(n+k) by A2,A3,XBOOLE_0:def 4; then x in X1.n by Th20; hence thesis by A4,XBOOLE_0:def 4; end; hence thesis; end; theorem Th38: B is constant & the_value_of B = A implies for n holds ( inferior_setsequence B).n = A proof assume A1: B is constant & the_value_of B = A; let n; (inferior_setsequence(B)).n = meet {B.k : n <= k} by Def2; hence thesis by A1,Th14; end; theorem Th39: B is constant & the_value_of B = A implies for n holds ( superior_setsequence B).n = A proof assume A1: B is constant & the_value_of B = A; let n; (superior_setsequence(B)).n = union {B.k : n <= k} by Def3; hence thesis by A1,Th13; end; theorem Th40: for n being Nat holds B is non-descending implies B.n c= (superior_setsequence(B)).(n+ 1) proof let n be Nat; assume B is non-descending; then A1: B.n c= B.(n+1) by PROB_2:7; B.n c= union {B.k : n+1 <= k} proof let x be object; A2: B.(n+1) in {B.k : n+1 <= k}; assume x in B.n; hence thesis by A1,A2,TARSKI:def 4; end; hence thesis by Def3; end; theorem Th41: for n being Nat holds B is non-descending implies (superior_setsequence B).n = ( superior_setsequence B).(n+1) proof let n be Nat; assume B is non-descending; then (superior_setsequence B).(n+1) \/ B.n = (superior_setsequence B).(n+1) by Th40,XBOOLE_1:12; hence thesis by Th22; end; theorem Th42: for n being Nat holds B is non-descending implies (superior_setsequence B).n = Union B proof let n be Nat; defpred P[Nat] means (superior_setsequence B).\$1 = Union B; assume B is non-descending; then A1: for k being Nat st P[k] holds P[k+1] by Th41; A2: P[0] by Th18; for k being Nat holds P[k] from NAT_1:sch 2(A2,A1); hence thesis; end; theorem Th43: B is non-descending implies Intersection superior_setsequence B = Union B proof assume A1: B is non-descending; now let x be object; assume A2: x in Intersection superior_setsequence B; now let n; (superior_setsequence B).n = Union B by A1,Th42; hence x in Union B by A2,PROB_1:13; end; hence x in Union B; end; then A3: Intersection superior_setsequence(B) c= Union B; now let y be object; assume y in Union B; then for n being Nat holds y in (superior_setsequence(B)).n by A1,Th42; hence y in Intersection superior_setsequence(B) by PROB_1:13; end; then Union B c= Intersection superior_setsequence(B); hence thesis by A3,XBOOLE_0:def 10; end; theorem Th44: B is non-descending implies B.n c= (inferior_setsequence B).(n+1 ) proof set Y = {B.k : n+1 <= k}; assume A1: B is non-descending; let x be object; assume A2: x in B.n; A3: now let y be set; assume y in Y; then consider k1 being Nat such that A4: y=B.k1 and A5: n+1 <= k1; n <= k1 by A5,NAT_1:13; then B.n c= B.k1 by A1,PROB_1:def 5; hence x in y by A2,A4; end; A6: Y <> {} by Th1; (inferior_setsequence B).(n+1) = meet {B.k : n+1 <= k} by Def2; hence thesis by A6,A3,SETFAM_1:def 1; end; theorem Th45: B is non-descending implies (inferior_setsequence B).n = B.n proof assume B is non-descending; then (inferior_setsequence B).(n+1) /\ B.n = B.n by Th44,XBOOLE_1:28; hence thesis by Th21; end; theorem Th46: B is non-descending implies inferior_setsequence B = B proof assume B is non-descending; then (inferior_setsequence B).n = B.n by Th45; then for n being Element of NAT holds (inferior_setsequence B).n = B.n; hence thesis by FUNCT_2:63; end; theorem Th47: B is non-ascending implies (superior_setsequence B).(n+1) c= B.n proof assume A1: B is non-ascending; let x be object; assume x in (superior_setsequence(B)).(n+1); then consider k being Nat such that A2: x in B.(n +1+k) by Th20; n+1 <= n+1+k by NAT_1:11; then n <= n+1+k by NAT_1:13; then B.(n +1+k) c= B.n by A1,PROB_1:def 4; hence thesis by A2; end; theorem Th48: B is non-ascending implies (superior_setsequence(B)).n = B.n proof assume B is non-ascending; then (superior_setsequence(B)).(n+1) \/ B.n = B.n by Th47,XBOOLE_1:12; hence thesis by Th22; end; theorem Th49: B is non-ascending implies superior_setsequence(B) = B proof assume B is non-ascending; then (superior_setsequence(B)).n = B.n by Th48; then for n being Element of NAT holds (superior_setsequence(B)).n = B.n; hence thesis by FUNCT_2:63; end; theorem Th50: for n being Nat holds B is non-ascending implies (inferior_setsequence(B)).(n+1) c= B. n proof let n be Nat; set Y = {B.k : n+1 <= k}; assume B is non-ascending; then A1: B.(n+1) c= B.n by PROB_2:6; A2: B.(n+1) in Y; A3: now let x be object; assume x in meet Y; then x in B.(n+1) by A2,SETFAM_1:def 1; hence x in B.n by A1; end; (inferior_setsequence(B)).(n+1) = meet {B.k : n+1 <= k} by Def2; hence thesis by A3; end; theorem Th51: for n being Nat holds B is non-ascending implies (inferior_setsequence(B)).n = ( inferior_setsequence(B)).(n+1) proof let n be Nat; assume B is non-ascending; then (inferior_setsequence(B)).(n+1) /\ B.n = (inferior_setsequence(B)).(n+1) by Th50,XBOOLE_1:28; hence thesis by Th21; end; theorem Th52: for n being Nat holds B is non-ascending implies (inferior_setsequence(B)).n = Intersection B proof let n be Nat; defpred P[Nat] means (inferior_setsequence(B)).\$1 = Intersection B; assume B is non-ascending; then A1: for k being Nat st P[k] holds P[k+1] by Th51; A2: P[0] by Th17; for k being Nat holds P[k] from NAT_1:sch 2(A2,A1); hence thesis; end; theorem Th53: B is non-ascending implies Union inferior_setsequence(B) = Intersection B proof assume A1: B is non-ascending; now let x be object; assume x in Union inferior_setsequence(B); then ex k being Nat st x in (inferior_setsequence(B)).k by PROB_1:12; hence x in Intersection B by A1,Th52; end; then A2: Union inferior_setsequence(B) c= Intersection B; now let y be object; assume y in Intersection B; then y in (inferior_setsequence(B)).0 by Th17; hence y in Union inferior_setsequence(B) by PROB_1:12; end; then Intersection B c= Union inferior_setsequence(B); hence thesis by A2,XBOOLE_0:def 10; end; definition let X be set, B be SetSequence of X; redefine func lim_inf B equals Union inferior_setsequence B; compatibility proof let F be Subset of X; hereby assume A1: F = lim_inf B; for x being object holds x in F iff x in Union inferior_setsequence B proof let x be object; hereby assume x in F; then consider n being Nat such that A2: for k being Nat holds x in B.(n+k) by A1,KURATO_0:4; x in (inferior_setsequence B).n by A2,Th19; hence x in Union inferior_setsequence B by PROB_1:12; end; assume x in Union inferior_setsequence B; then consider n being Nat such that A3: x in (inferior_setsequence B).n by PROB_1:12; for k being Nat holds x in B.(n + k) by A3,Th19; hence thesis by A1,KURATO_0:4; end; hence F = Union inferior_setsequence B by TARSKI:2; end; assume A4: F = Union inferior_setsequence B; for x being object holds x in F iff x in lim_inf B proof let x be object; hereby assume x in F; then consider n being Nat such that A5: x in (inferior_setsequence B).n by A4,PROB_1:12; for k being Nat holds x in B.(n + k) by A5,Th19; hence x in lim_inf B by KURATO_0:4; end; assume x in lim_inf B; then consider n being Nat such that A6: for k being Nat holds x in B.(n+k) by KURATO_0:4; x in (inferior_setsequence B).n by A6,Th19; hence thesis by A4,PROB_1:12; end; hence thesis by TARSKI:2; end; end; definition let X be set, B be SetSequence of X; redefine func lim_sup B equals Intersection superior_setsequence B; compatibility proof let F be Subset of X; hereby assume A1: F = lim_sup B; for x being object holds x in F iff x in Intersection superior_setsequence B proof let x be object; hereby assume A2: x in F; for m being Nat holds x in (superior_setsequence B).m proof let m be Nat; ex k being Nat st x in B.(m+k) by A1,A2,KURATO_0:5; hence thesis by Th20; end; hence x in Intersection superior_setsequence B by PROB_1:13; end; assume A3: x in Intersection superior_setsequence B; now let m be Nat; x in (superior_setsequence B).m by A3,PROB_1:13; hence ex k being Nat st x in B.(m + k) by Th20; end; hence thesis by A1,KURATO_0:5; end; hence F = Intersection superior_setsequence B by TARSKI:2; end; assume A4: F = Intersection superior_setsequence B; for x being object holds x in F iff x in lim_sup B proof let x be object; hereby assume A5: x in F; now let m be Nat; x in (superior_setsequence B).m by A4,A5,PROB_1:13; hence ex k being Nat st x in B.(m + k) by Th20; end; hence x in lim_sup B by KURATO_0:5; end; assume A6: x in lim_sup B; for m being Nat holds x in (superior_setsequence B).m proof let m be Nat; ex k being Nat st x in B.(m+k) by A6,KURATO_0:5; hence thesis by Th20; end; hence thesis by A4,PROB_1:13; end; hence thesis by TARSKI:2; end; end; notation let X be set, B be SetSequence of X; synonym lim B for lim_sup B; end; theorem Intersection B c= lim_inf B proof let x be object; assume x in Intersection B; then for k being Nat holds x in B.(0+k) by PROB_1:13; hence thesis by KURATO_0:4; end; theorem lim_inf B = lim inferior_setsequence(B) by Th43; theorem lim_sup B = lim superior_setsequence(B) by Th49; theorem lim_sup B = (lim_inf Complement B)` proof lim_inf Complement B = (lim_sup Complement Complement B)` by KURATO_0:9 .= (lim_sup B)`; hence thesis; end; theorem Th58: B is constant & the_value_of B = A implies B is convergent & lim B = A & lim_inf B = A & lim_sup B = A proof assume A1: B is constant & the_value_of B = A; then for n holds (superior_setsequence(B)).n = A by Th39; then A2: lim_sup B = A by Th11; for n holds (inferior_setsequence(B)).n = A by A1,Th38; then lim_inf B = A by Th10; hence thesis by A2,KURATO_0:def 5; end; theorem B is non-descending implies lim_sup B = Union B by Th43; theorem B is non-descending implies lim_inf B = Union B by Th46; theorem B is non-ascending implies lim_sup B = Intersection B by Th49; theorem B is non-ascending implies lim_inf B = Intersection B by Th53; theorem Th63: B is non-descending implies B is convergent & lim B = Union B proof assume A1: B is non-descending; then lim_sup B = Union B & lim_inf B = Union B by Th43,Th46; hence B is convergent by KURATO_0:def 5; thus thesis by A1,Th43; end; theorem Th64: B is non-ascending implies B is convergent & lim B = Intersection B proof assume A1: B is non-ascending; then lim_sup B = Intersection B & lim_inf B = Intersection B by Th49,Th53; hence B is convergent by KURATO_0:def 5; thus thesis by A1,Th49; end; theorem B is monotone implies B is convergent proof assume A1: B is monotone; per cases by A1; suppose B is non-ascending; hence thesis by Th64; end; suppose B is non-descending; hence thesis by Th63; end; end; definition let X be set, Si be SigmaField of X, S be SetSequence of Si; redefine func inferior_setsequence S -> SetSequence of Si; coherence proof now let n be Nat; reconsider DSeq = S ^\ n as SetSequence of X; reconsider n1=n as Nat; for m being Nat holds DSeq.m in Si proof let m be Nat; DSeq.m = S.(m+n1) & S.(m+n1) in rng S by NAT_1:51,def 3; hence thesis; end; then rng DSeq c= Si by NAT_1:52; then A1: Intersection DSeq in Si by PROB_1:def 6; Intersection DSeq = meet rng DSeq by Th8; then Intersection DSeq = meet {S.k: n1 <= k} by Th6; hence (inferior_setsequence S).n in Si by A1,Def2; end; then rng inferior_setsequence S c= Si by NAT_1:52; hence thesis by RELAT_1:def 19; end; end; definition let X be set, Si be SigmaField of X, S be SetSequence of Si; redefine func superior_setsequence S -> SetSequence of Si; coherence proof now let n be Nat; reconsider DSeq = S ^\ n as SetSequence of X; reconsider n1=n as Nat; A1: Union DSeq in Si by PROB_1:17; Union DSeq = union rng DSeq by CARD_3:def 4; then Union DSeq =union {S.k: n1 <= k} by Th6; hence (superior_setsequence(S)).n in Si by A1,Def3; end; then rng superior_setsequence S c= Si by NAT_1:52; hence thesis by RELAT_1:def 19; end; end; theorem Th66: x in lim_sup S iff for n being Nat ex k being Nat st x in S.(n+k) proof x in Intersection superior_setsequence B iff for n being Nat ex k being Nat st x in B.(n+k) proof lim_sup B = Intersection superior_setsequence B; hence thesis by KURATO_0:5; end; hence thesis; end; theorem Th67: x in lim_inf S iff ex n being Nat st for k being Nat holds x in S.(n+k) proof x in Union inferior_setsequence(B) iff ex n being Nat st for k being Nat holds x in B.(n+k) proof lim_inf B = Union inferior_setsequence(B); hence thesis by KURATO_0:4; end; hence thesis; end; theorem Intersection S c= lim_inf S proof let x be object; assume x in Intersection S; then for k being Nat holds x in S.(0+k) by PROB_1:13; hence thesis by Th67; end; theorem lim_sup S c= Union S proof let x be object; assume x in lim_sup S; then ex k being Nat st x in S.(0+k) by Th66; hence thesis by PROB_1:12; end; theorem lim_inf S c= lim_sup S proof Union inferior_setsequence B c= Intersection superior_setsequence B proof lim_inf B = Union inferior_setsequence(B) & lim_sup B = Intersection superior_setsequence(B); hence thesis by KURATO_0:6; end; hence thesis; end; theorem Th71: lim_inf S = (lim_sup Complement S)` proof Union inferior_setsequence(B) = (Intersection superior_setsequence( Complement B))` proof lim_inf B = Union inferior_setsequence(B) & (lim_sup Complement B)` = ( Intersection superior_setsequence(Complement B))`; hence thesis by KURATO_0:9; end; hence thesis; end; theorem lim_sup S = (lim_inf Complement S)` proof lim_inf (Complement S qua non empty SetSequence of X) = (lim_sup Complement Complement S)` by Th71 .= (lim_sup S)`; hence thesis; end; theorem (for n being Nat holds S3.n = S1.n \/ S2.n) implies lim_inf S1 \/ lim_inf S2 c= lim_inf S3 proof A1: (for n being Nat holds A3.n = B.n \/ A2.n) implies Union inferior_setsequence(B) \/ Union inferior_setsequence(A2) c= Union inferior_setsequence(A3) proof A2: lim_inf B = Union inferior_setsequence(B) & lim_inf A2 = Union inferior_setsequence(A2); A3: lim_inf A3 = Union inferior_setsequence(A3); assume for n being Nat holds A3.n = B.n \/ A2.n; hence thesis by A2,A3,KURATO_0:12; end; assume for n being Nat holds S3.n = S1.n \/ S2.n; hence thesis by A1; end; theorem (for n being Nat holds S3.n = S1.n /\ S2.n) implies lim_inf S3 = lim_inf S1 /\ lim_inf S2 proof A1: (for n being Nat holds A3.n = B.n /\ A2.n) implies Union inferior_setsequence(B) /\ Union inferior_setsequence(A2) = Union inferior_setsequence(A3) proof A2: lim_inf B = Union inferior_setsequence(B) & lim_inf A2 = Union inferior_setsequence(A2); A3: lim_inf A3 = Union inferior_setsequence(A3); assume for n being Nat holds A3.n = B.n /\ A2.n; hence thesis by A2,A3,KURATO_0:10; end; assume for n being Nat holds S3.n = S1.n /\ S2.n; hence thesis by A1; end; theorem (for n being Nat holds S3.n = S1.n \/ S2.n) implies lim_sup S3 = lim_sup S1 \/ lim_sup S2 proof A1: (for n being Nat holds A3.n = B.n \/ A2.n) implies Intersection superior_setsequence(B) \/ Intersection superior_setsequence(A2) = Intersection superior_setsequence(A3) proof A2: lim_sup B = Intersection superior_setsequence(B) & lim_sup A2 = Intersection superior_setsequence(A2); A3: lim_sup A3 = Intersection superior_setsequence(A3); assume for n being Nat holds A3.n = B.n \/ A2.n; hence thesis by A2,A3,KURATO_0:11; end; assume for n being Nat holds S3.n = S1.n \/ S2.n; hence thesis by A1; end; theorem (for n being Nat holds S3.n = S1.n /\ S2.n) implies lim_sup S3 c= lim_sup S1 /\ lim_sup S2 proof A1: (for n being Nat holds A3.n = B.n /\ A2.n) implies Intersection superior_setsequence(A3) c= Intersection superior_setsequence(B) /\ Intersection superior_setsequence(A2) proof A2: lim_sup B = Intersection superior_setsequence(B) & lim_sup A2 = Intersection superior_setsequence(A2); A3: lim_sup A3 = Intersection superior_setsequence(A3); assume for n being Nat holds A3.n = B.n /\ A2.n; hence thesis by A2,A3,KURATO_0:13; end; assume for n being Nat holds S3.n = S1.n /\ S2.n; hence thesis by A1; end; theorem S is constant & the_value_of S = A implies S is convergent & lim S = A & lim_inf S = A & lim_sup S = A proof A1: B is constant & the_value_of B = A implies Union inferior_setsequence(B) = A & Intersection superior_setsequence(B) = A proof A2: lim_inf B = Union inferior_setsequence(B) & lim_sup B = Intersection superior_setsequence(B); assume B is constant & the_value_of B = A; hence thesis by A2,Th58; end; assume S is constant & the_value_of S = A; then lim_inf S = A & lim_sup S = A by A1; hence thesis by KURATO_0:def 5; end; theorem Th78: S is non-descending implies lim_sup S = Union S by Th43; theorem Th79: S is non-descending implies lim_inf S = Union S by Th46; theorem Th80: S is non-descending implies S is convergent & lim S = Union S proof assume A1: S is non-descending; then lim_sup S = Union S & lim_inf S = Union S by Th78,Th79; hence S is convergent by KURATO_0:def 5; thus thesis by A1,Th78; end; theorem Th81: S is non-ascending implies lim_sup S = Intersection S by Th49; theorem Th82: S is non-ascending implies lim_inf S = Intersection S by Th53; theorem Th83: S is non-ascending implies S is convergent & lim S = Intersection S proof assume A1: S is non-ascending; then lim_sup S = Intersection S & lim_inf S = Intersection S by Th81,Th82; hence S is convergent by KURATO_0:def 5; thus thesis by A1,Th81; end; theorem S is monotone implies S is convergent proof assume A1: S is monotone; per cases by A1; suppose S is non-ascending; hence thesis by Th83; end; suppose S is non-descending; hence thesis by Th80; end; end;