:: 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-2026 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;
definitions TARSKI, XBOOLE_0, FUNCT_2;
equalities XBOOLE_0;
expansions XBOOLE_0;
theorems XBOOLE_0, XBOOLE_1, KURATO_0, SETLIM_1, CARD_3, PROB_1, NAT_1,
ORDINAL1;
schemes FUNCT_2;
begin
reserve n,m,k for Nat,
x,X for set,
A for Subset of X,
A1,A2 for SetSequence of X;
theorem Th1:
(inferior_setsequence(A1)).n = Intersection (A1 ^\n)
proof
reconsider Y = {A1.k: n <= k} as Subset-Family of X by SETLIM_1:28;
(inferior_setsequence(A1)).n = meet Y by SETLIM_1:def 2
.= meet rng (A1 ^\ n) by SETLIM_1:6;
hence thesis by SETLIM_1:8;
end;
theorem Th2:
(superior_setsequence(A1)).n = Union (A1 ^\n)
proof
reconsider Y = {A1.k: n <= k} as Subset-Family of X by SETLIM_1:28;
(superior_setsequence(A1)).n = union Y by SETLIM_1:def 3
.= union rng (A1 ^\ n) by SETLIM_1:6;
hence thesis by CARD_3:def 4;
end;
definition
let X;
let A1,A2 be SetSequence of X;
func A1 (/\) A2 -> SetSequence of X means
:Def1:
for n holds it.n = A1.n /\ A2.n;
existence
proof
deffunc F(Nat) = A1.$1 /\ A2.$1;
consider f being SetSequence of X such that
A1: for n being Element of NAT holds f.n = F(n) from FUNCT_2:sch 4;
take f;
let n;
n in NAT by ORDINAL1:def 12;
then f.n = F(n) by A1;
hence thesis;
end;
uniqueness
proof
let A3 be SetSequence of X,A4 be SetSequence of X such that
A2: for n holds A3.n = A1.n /\ A2.n and
A3: for n holds A4.n = A1.n /\ A2.n;
let n be Element of NAT;
thus A3.n = A1.n /\ A2.n by A2
.= A4.n by A3;
end;
commutativity;
func A1 (\/) A2 -> SetSequence of X means
:Def2:
for n holds it.n = A1.n \/ A2.n;
existence
proof
deffunc F(Nat) = A1.$1 \/ A2.$1;
consider f being SetSequence of X such that
A4: for n being Element of NAT holds f.n = F(n) from FUNCT_2:sch 4;
take f;
let n;
n in NAT by ORDINAL1:def 12;
then f.n = F(n) by A4;
hence thesis;
end;
uniqueness
proof
let A3 be SetSequence of X,A4 be SetSequence of X such that
A5: for n holds A3.n = A1.n \/ A2.n and
A6: for n holds A4.n = A1.n \/ A2.n;
let n be Element of NAT;
thus A3.n = A1.n \/ A2.n by A5
.= A4.n by A6;
end;
commutativity;
func A1 (\) A2 -> SetSequence of X means
:Def3:
for n holds it.n = A1.n \ A2 .n;
existence
proof
deffunc F(Nat) = A1.$1 \ A2.$1;
consider f being SetSequence of X such that
A7: for n being Element of NAT holds f.n = F(n) from FUNCT_2:sch 4;
take f;
let n;
n in NAT by ORDINAL1:def 12;
then f.n = F(n) by A7;
hence thesis;
end;
uniqueness
proof
let A3 be SetSequence of X,A4 be SetSequence of X such that
A8: for n holds A3.n = A1.n \ A2.n and
A9: for n holds A4.n = A1.n \ A2.n;
let n be Element of NAT;
thus A3.n = A1.n \ A2.n by A8
.= A4.n by A9;
end;
func A1 (\+\) A2 -> SetSequence of X means
:Def4:
for n holds it.n = A1.n \+\ A2.n;
existence
proof
deffunc F(Nat) = A1.$1 \+\ A2.$1;
consider f being SetSequence of X such that
A10: for n being Element of NAT holds f.n = F(n) from FUNCT_2:sch 4;
take f;
let n;
n in NAT by ORDINAL1:def 12;
then f.n = F(n) by A10;
hence thesis;
end;
uniqueness
proof
let A3 be SetSequence of X,A4 be SetSequence of X such that
A11: for n holds A3.n = A1.n \+\ A2.n and
A12: for n holds A4.n = A1.n \+\ A2.n;
let n be Element of NAT;
thus A3.n = A1.n \+\ A2.n by A11
.= A4.n by A12;
end;
commutativity;
end;
theorem Th3:
A1 (\+\) A2 = (A1 (\) A2) (\/) (A2 (\) A1)
proof
let n be Element of NAT;
thus (A1 (\+\) A2).n = A1.n \+\ A2.n by Def4
.= (A1 (\) A2).n \/ (A2.n \ A1.n) by Def3
.= (A1 (\) A2).n \/ (A2 (\) A1).n by Def3
.= ((A1 (\) A2) (\/) (A2 (\) A1)).n by Def2;
end;
theorem Th4:
(A1 (/\) A2) ^\k = (A1 ^\k) (/\) (A2 ^\k)
proof
let n be Element of NAT;
thus ((A1 (/\) A2) ^\k).n = (A1 (/\) A2).(n+k) by NAT_1:def 3
.= A1.(n+k) /\ A2.(n+k) by Def1
.= (A1 ^\k).n /\ A2.(n+k) by NAT_1:def 3
.= (A1 ^\k).n /\ (A2 ^\k).n by NAT_1:def 3
.= ((A1 ^\k) (/\) (A2 ^\k)).n by Def1;
end;
theorem Th5:
(A1 (\/) A2) ^\k = (A1 ^\k) (\/) (A2 ^\k)
proof
let n be Element of NAT;
thus ((A1 (\/) A2) ^\k).n = (A1 (\/) A2).(n+k) by NAT_1:def 3
.= A1.(n+k) \/ A2.(n+k) by Def2
.= (A1 ^\k).n \/ A2.(n+k) by NAT_1:def 3
.= (A1 ^\k).n \/ (A2 ^\k).n by NAT_1:def 3
.= ((A1 ^\k) (\/) (A2 ^\k)).n by Def2;
end;
theorem Th6:
(A1 (\) A2) ^\k = (A1 ^\k) (\) (A2 ^\k)
proof
let n be Element of NAT;
thus ((A1 (\) A2) ^\k).n = (A1 (\) A2).(n+k) by NAT_1:def 3
.= A1.(n+k) \ A2.(n+k) by Def3
.= (A1 ^\k).n \ A2.(n+k) by NAT_1:def 3
.= (A1 ^\k).n \ (A2 ^\k).n by NAT_1:def 3
.= ((A1 ^\k) (\) (A2 ^\k)).n by Def3;
end;
theorem Th7:
(A1 (\+\) A2) ^\k = (A1 ^\k) (\+\) (A2 ^\k)
proof
let n be Element of NAT;
thus ((A1 (\+\) A2) ^\k).n = (A1 (\+\) A2).(n+k) by NAT_1:def 3
.= A1.(n+k) \+\ A2.(n+k) by Def4
.= (A1 ^\k).n \+\ A2.(n+k) by NAT_1:def 3
.= (A1 ^\k).n \+\ (A2 ^\k).n by NAT_1:def 3
.= ((A1 ^\k) (\+\) (A2 ^\k)).n by Def4;
end;
theorem Th8:
Union (A1 (/\) A2) c= Union A1 /\ Union A2
proof
let x be object;
assume x in Union (A1 (/\) A2);
then consider n such that
A1: x in (A1 (/\) A2).n by PROB_1:12;
A2: x in A1.n /\ A2.n by A1,Def1;
then x in A2.n by XBOOLE_0:def 4;
then
A3: x in Union A2 by PROB_1:12;
x in A1.n by A2,XBOOLE_0:def 4;
then x in Union A1 by PROB_1:12;
hence thesis by A3,XBOOLE_0:def 4;
end;
theorem Th9:
Union (A1 (\/) A2) = Union A1 \/ Union A2
proof
thus Union (A1 (\/) A2) c= Union A1 \/ Union A2
proof
let x be object;
assume x in Union (A1 (\/) A2);
then consider n1 being Nat such that
A1: x in (A1 (\/) A2).n1 by PROB_1:12;
A2: x in A1.n1 \/ A2.n1 by A1,Def2;
per cases by A2,XBOOLE_0:def 3;
suppose
x in A1.n1;
then x in Union A1 by PROB_1:12;
hence thesis by XBOOLE_0:def 3;
end;
suppose
x in A2.n1;
then x in Union A2 by PROB_1:12;
hence thesis by XBOOLE_0:def 3;
end;
end;
let x be object;
assume
A3: x in Union A1 \/ Union A2;
per cases by A3,XBOOLE_0:def 3;
suppose
x in Union A1;
then consider n2 being Nat such that
A4: x in A1.n2 by PROB_1:12;
x in A1.n2 \/ A2.n2 by A4,XBOOLE_0:def 3;
then x in (A1 (\/) A2).n2 by Def2;
hence thesis by PROB_1:12;
end;
suppose
x in Union A2;
then consider n3 being Nat such that
A5: x in A2.n3 by PROB_1:12;
x in A1.n3 \/ A2.n3 by A5,XBOOLE_0:def 3;
then x in (A1 (\/) A2).n3 by Def2;
hence thesis by PROB_1:12;
end;
end;
theorem Th10:
Union A1 \ Union A2 c= Union (A1 (\) A2)
proof
let x be object;
assume
A1: x in Union A1 \ Union A2;
then x in Union A1 by XBOOLE_0:def 5;
then consider n1 being Nat such that
A2: x in A1.n1 by PROB_1:12;
not x in Union A2 by A1,XBOOLE_0:def 5;
then not x in A2.n1 by PROB_1:12;
then x in A1.n1 \ A2.n1 by A2,XBOOLE_0:def 5;
then x in (A1 (\) A2).n1 by Def3;
hence thesis by PROB_1:12;
end;
theorem Th11:
Union A1 \+\ Union A2 c= Union (A1 (\+\) A2)
proof
A1: (Union A1 \ Union A2) c= Union (A1 (\) A2) & (Union A2 \ Union A1) c=
Union (A2 (\) A1) by Th10;
Union (A1 (\) A2) \/ Union (A2 (\) A1) = Union ((A1 (\) A2) (\/) (A2 (\)
A1)) by Th9
.= Union (A1 (\+\) A2) by Th3;
hence thesis by A1,XBOOLE_1:13;
end;
theorem Th12:
Intersection (A1 (/\) A2) = Intersection A1 /\ Intersection A2
proof
thus Intersection (A1 (/\) A2) c= Intersection A1 /\ Intersection A2
proof
let x be object;
assume
A1: x in Intersection (A1 (/\) A2);
now
let k;
x in (A1 (/\) A2).k by A1,PROB_1:13;
then x in (A1.k /\ A2.k) by Def1;
hence x in A1.k & x in A2.k by XBOOLE_0:def 4;
end;
then x in Intersection A1 & x in Intersection A2 by PROB_1:13;
hence thesis by XBOOLE_0:def 4;
end;
let x be object;
assume x in Intersection A1 /\ Intersection A2;
then
A2: x in Intersection A1 & x in Intersection A2 by XBOOLE_0:def 4;
now
let k;
x in A1.k & x in A2.k by A2,PROB_1:13;
then x in A1.k /\ A2.k by XBOOLE_0:def 4;
hence x in (A1 (/\) A2).k by Def1;
end;
hence thesis by PROB_1:13;
end;
theorem Th13:
Intersection A1 \/ Intersection A2 c= Intersection (A1 (\/) A2)
proof
let x be object;
assume
A1: x in Intersection A1 \/ Intersection A2;
per cases by A1,XBOOLE_0:def 3;
suppose
A2: x in Intersection A1;
now
let k;
x in A1.k by A2,PROB_1:13;
then x in (A1.k \/ A2.k) by XBOOLE_0:def 3;
hence x in (A1 (\/) A2).k by Def2;
end;
hence thesis by PROB_1:13;
end;
suppose
A3: x in Intersection A2;
now
let k;
x in A2.k by A3,PROB_1:13;
then x in A1.k \/ A2.k by XBOOLE_0:def 3;
hence x in (A1 (\/) A2).k by Def2;
end;
hence thesis by PROB_1:13;
end;
end;
theorem Th14:
Intersection (A1 (\) A2) c= Intersection A1 \ Intersection A2
proof
let x be object;
assume
A1: x in Intersection (A1 (\) A2);
A2: now
let k;
x in (A1 (\) A2).k by A1,PROB_1:13;
then x in (A1.k \ A2.k) by Def3;
hence x in A1.k & not x in A2.k by XBOOLE_0:def 5;
end;
then not x in A2.0;
then
A3: not x in Intersection A2 by PROB_1:13;
x in Intersection A1 by A2,PROB_1:13;
hence thesis by A3,XBOOLE_0:def 5;
end;
definition
let X;
let A1 be SetSequence of X, A be Subset of X;
func A (/\) A1 -> SetSequence of X means
:Def5:
for n holds it.n = A /\ A1.n;
existence
proof
deffunc F(Nat) = A /\ A1.$1;
consider f being SetSequence of X such that
A1: for n being Element of NAT holds f.n = F(n) from FUNCT_2:sch 4;
take f;
let n;
n in NAT by ORDINAL1:def 12;
then f.n = F(n) by A1;
hence thesis;
end;
uniqueness
proof
let A3 be SetSequence of X,A4 be SetSequence of X such that
A2: for n holds A3.n = A /\ A1.n and
A3: for n holds A4.n = A /\ A1.n;
let n be Element of NAT;
thus A3.n = A /\ A1.n by A2
.= A4.n by A3;
end;
func A (\/) A1 -> SetSequence of X means
:Def6:
for n holds it.n = A \/ A1.n;
existence
proof
deffunc F(Nat) = A \/ A1.$1;
consider f being SetSequence of X such that
A4: for n being Element of NAT holds f.n = F(n) from FUNCT_2:sch
4;
take f;
let n;
n in NAT by ORDINAL1:def 12;
then f.n = F(n) by A4;
hence thesis;
end;
uniqueness
proof
let A3 be SetSequence of X,A4 be SetSequence of X such that
A5: for n holds A3.n = A \/ A1.n and
A6: for n holds A4.n = A \/ A1.n;
let n be Element of NAT;
thus A3.n = A \/ A1.n by A5
.= A4.n by A6;
end;
func A (\) A1 -> SetSequence of X means
:Def7:
for n holds it.n = A \ A1.n;
existence
proof
deffunc F(Nat) = A \ A1.$1;
consider f being SetSequence of X such that
A7: for n being Element of NAT holds f.n = F(n) from FUNCT_2:sch 4;
take f;
let n;
n in NAT by ORDINAL1:def 12;
then f.n = F(n) by A7;
hence thesis;
end;
uniqueness
proof
let A3 be SetSequence of X,A4 be SetSequence of X such that
A8: for n holds A3.n = A \ A1.n and
A9: for n holds A4.n = A \ A1.n;
let n be Element of NAT;
thus A3.n = A \ A1.n by A8
.= A4.n by A9;
end;
func A1 (\) A -> SetSequence of X means
:Def8:
for n holds it.n = A1.n \ A;
existence
proof
deffunc F(Nat) = A1.$1 \ A;
consider f being SetSequence of X such that
A10: for n being Element of NAT holds f.n = F(n) from FUNCT_2:sch 4;
take f;
let n;
n in NAT by ORDINAL1:def 12;
then f.n = F(n) by A10;
hence thesis;
end;
uniqueness
proof
let A3 be SetSequence of X,A4 be SetSequence of X such that
A11: for n holds A3.n = A1.n \ A and
A12: for n holds A4.n = A1.n \ A;
let n be Element of NAT;
thus A3.n = A1.n \ A by A11
.= A4.n by A12;
end;
func A (\+\) A1 -> SetSequence of X means
:Def9:
for n holds it.n = A \+\ A1 .n;
existence
proof
deffunc F(Nat) = A \+\ A1.$1;
consider f being SetSequence of X such that
A13: for n being Element of NAT holds f.n = F(n) from FUNCT_2:sch 4;
take f;
let n;
n in NAT by ORDINAL1:def 12;
then f.n = F(n) by A13;
hence thesis;
end;
uniqueness
proof
let A3 be SetSequence of X,A4 be SetSequence of X such that
A14: for n holds A3.n = A \+\ A1.n and
A15: for n holds A4.n = A \+\ A1.n;
let n be Element of NAT;
thus A3.n = A \+\ A1.n by A14
.= A4.n by A15;
end;
end;
theorem
A (\+\) A1 = (A (\) A1) (\/) (A1 (\) A)
proof
let n be Element of NAT;
thus (A (\+\) A1).n = A \+\ A1.n by Def9
.= (A (\) A1).n \/ (A1.n \ A) by Def7
.= (A (\) A1).n \/ (A1 (\) A).n by Def8
.= ((A (\) A1) (\/) (A1 (\) A)).n by Def2;
end;
theorem Th16:
(A (/\) A1) ^\k = A (/\) (A1 ^\k)
proof
let n be Element of NAT;
thus ((A (/\) A1) ^\k).n = (A (/\) A1).(n+k) by NAT_1:def 3
.= A /\ A1.(n+k) by Def5
.= A /\ (A1 ^\k).n by NAT_1:def 3
.= (A (/\) (A1 ^\k)).n by Def5;
end;
theorem Th17:
(A (\/) A1) ^\k = A (\/) (A1 ^\k)
proof
let n be Element of NAT;
thus ((A (\/) A1) ^\k).n = (A (\/) A1).(n+k) by NAT_1:def 3
.= A \/ A1.(n+k) by Def6
.= A \/ (A1 ^\k).n by NAT_1:def 3
.= (A (\/) (A1 ^\k)).n by Def6;
end;
theorem Th18:
(A (\) A1) ^\k = A (\) (A1 ^\k)
proof
let n be Element of NAT;
thus ((A (\) A1) ^\k).n = (A (\) A1).(n+k) by NAT_1:def 3
.= A \ A1.(n+k) by Def7
.= A \ (A1 ^\k).n by NAT_1:def 3
.= (A (\) (A1 ^\k)).n by Def7;
end;
theorem Th19:
(A1 (\) A) ^\k = (A1 ^\k) (\) A
proof
let n be Element of NAT;
thus ((A1 (\) A) ^\k).n = (A1 (\) A).(n+k) by NAT_1:def 3
.= A1.(n+k) \ A by Def8
.= (A1 ^\k).n \ A by NAT_1:def 3
.= ((A1 ^\k) (\) A).n by Def8;
end;
theorem Th20:
(A (\+\) A1) ^\k = A (\+\) (A1 ^\k)
proof
let n be Element of NAT;
thus ((A (\+\) A1) ^\k).n = (A (\+\) A1).(n+k) by NAT_1:def 3
.= A \+\ A1.(n+k) by Def9
.= A \+\ (A1 ^\k).n by NAT_1:def 3
.= (A (\+\) (A1 ^\k)).n by Def9;
end;
theorem Th21:
A1 is non-ascending implies A (/\) A1 is non-ascending
proof
assume
A1: A1 is non-ascending;
for n,m st n <= m holds (A (/\) A1).m c= (A (/\) A1).n
proof
let n,m;
assume n <= m;
then A1.m c= A1.n by A1,PROB_1:def 4;
then A /\ A1.m c= A /\ A1.n by XBOOLE_1:27;
then (A (/\) A1).m c= A /\ A1.n by Def5;
hence thesis by Def5;
end;
hence thesis by PROB_1:def 4;
end;
theorem Th22:
A1 is non-descending implies A (/\) A1 is non-descending
proof
assume
A1: A1 is non-descending;
for n,m st n <= m holds (A (/\) A1).n c= (A (/\) A1).m
proof
let n,m;
assume n <= m;
then A1.n c= A1.m by A1,PROB_1:def 5;
then A /\ A1.n c= A /\ A1.m by XBOOLE_1:27;
then (A (/\) A1).n c= A /\ A1.m by Def5;
hence thesis by Def5;
end;
hence thesis by PROB_1:def 5;
end;
theorem
A1 is monotone implies A (/\) A1 is monotone
proof
assume
A1: A1 is monotone;
per cases by A1,SETLIM_1:def 1;
suppose
A1 is non-ascending;
then A (/\) A1 is non-ascending by Th21;
hence thesis by SETLIM_1:def 1;
end;
suppose
A1 is non-descending;
then A (/\) A1 is non-descending by Th22;
hence thesis by SETLIM_1:def 1;
end;
end;
theorem Th24:
A1 is non-ascending implies A (\/) A1 is non-ascending
proof
assume
A1: A1 is non-ascending;
for n,m st n <= m holds (A (\/) A1).m c= (A (\/) A1).n
proof
let n,m;
assume n <= m;
then A1.m c= A1.n by A1,PROB_1:def 4;
then A \/ A1.m c= A \/ A1.n by XBOOLE_1:9;
then (A (\/) A1).m c= A \/ A1.n by Def6;
hence thesis by Def6;
end;
hence thesis by PROB_1:def 4;
end;
theorem Th25:
A1 is non-descending implies A (\/) A1 is non-descending
proof
assume
A1: A1 is non-descending;
for n,m st n <= m holds (A (\/) A1).n c= (A (\/) A1).m
proof
let n,m;
assume n <= m;
then A1.n c= A1.m by A1,PROB_1:def 5;
then A \/ A1.n c= A \/ A1.m by XBOOLE_1:9;
then (A (\/) A1).n c= A \/ A1.m by Def6;
hence thesis by Def6;
end;
hence thesis by PROB_1:def 5;
end;
theorem
A1 is monotone implies A (\/) A1 is monotone
proof
assume
A1: A1 is monotone;
per cases by A1,SETLIM_1:def 1;
suppose
A1 is non-ascending;
then A (\/) A1 is non-ascending by Th24;
hence thesis by SETLIM_1:def 1;
end;
suppose
A1 is non-descending;
then A (\/) A1 is non-descending by Th25;
hence thesis by SETLIM_1:def 1;
end;
end;
theorem Th27:
A1 is non-ascending implies A (\) A1 is non-descending
proof
assume
A1: A1 is non-ascending;
for n,m st n <= m holds (A (\) A1).n c= (A (\) A1).m
proof
let n,m;
assume n <= m;
then A1.m c= A1.n by A1,PROB_1:def 4;
then A \ A1.n c= A \ A1.m by XBOOLE_1:34;
then (A (\) A1).n c= A \ A1.m by Def7;
hence thesis by Def7;
end;
hence thesis by PROB_1:def 5;
end;
theorem Th28:
A1 is non-descending implies A (\) A1 is non-ascending
proof
assume
A1: A1 is non-descending;
for n,m st n <= m holds (A (\) A1).m c= (A (\) A1).n
proof
let n,m;
assume n <= m;
then A1.n c= A1.m by A1,PROB_1:def 5;
then A \ A1.m c= A \ A1.n by XBOOLE_1:34;
then (A (\) A1).m c= A \ A1.n by Def7;
hence thesis by Def7;
end;
hence thesis by PROB_1:def 4;
end;
theorem
A1 is monotone implies A (\) A1 is monotone
proof
assume
A1: A1 is monotone;
per cases by A1,SETLIM_1:def 1;
suppose
A1 is non-ascending;
then A (\) A1 is non-descending by Th27;
hence thesis by SETLIM_1:def 1;
end;
suppose
A1 is non-descending;
then A (\) A1 is non-ascending by Th28;
hence thesis by SETLIM_1:def 1;
end;
end;
theorem Th30:
A1 is non-ascending implies A1 (\) A is non-ascending
proof
assume
A1: A1 is non-ascending;
for n,m st n <= m holds (A1 (\) A).m c= (A1 (\) A).n
proof
let n,m;
assume n <= m;
then A1.m c= A1.n by A1,PROB_1:def 4;
then A1.m \ A c= A1.n \ A by XBOOLE_1:33;
then (A1 (\) A).m c= A1.n \ A by Def8;
hence thesis by Def8;
end;
hence thesis by PROB_1:def 4;
end;
theorem Th31:
A1 is non-descending implies A1 (\) A is non-descending
proof
assume
A1: A1 is non-descending;
for n,m st n <= m holds (A1 (\) A).n c= (A1 (\) A).m
proof
let n,m;
assume n <= m;
then A1.n c= A1.m by A1,PROB_1:def 5;
then A1.n \ A c= A1.m \ A by XBOOLE_1:33;
then (A1 (\) A).n c= A1.m \ A by Def8;
hence thesis by Def8;
end;
hence thesis by PROB_1:def 5;
end;
theorem
A1 is monotone implies A1 (\) A is monotone
proof
assume
A1: A1 is monotone;
per cases by A1,SETLIM_1:def 1;
suppose
A1 is non-ascending;
then A1 (\) A is non-ascending by Th30;
hence thesis by SETLIM_1:def 1;
end;
suppose
A1 is non-descending;
then A1 (\) A is non-descending by Th31;
hence thesis by SETLIM_1:def 1;
end;
end;
theorem Th33:
Intersection (A (/\) A1) = A /\ Intersection A1
proof
thus Intersection (A (/\) A1) c= A /\ Intersection A1
proof
let x be object;
assume
A1: x in Intersection (A (/\) A1);
A2: now
let k;
x in (A (/\) A1).k by A1,PROB_1:13;
then x in (A /\ A1.k) by Def5;
hence x in A & x in A1.k by XBOOLE_0:def 4;
end;
then x in Intersection A1 by PROB_1:13;
hence thesis by A2,XBOOLE_0:def 4;
end;
let x be object;
assume
A3: x in A /\ Intersection A1;
then
A4: x in Intersection A1 by XBOOLE_0:def 4;
now
let k;
x in A & x in A1.k by A3,A4,PROB_1:13,XBOOLE_0:def 4;
then x in A /\ A1.k by XBOOLE_0:def 4;
hence x in (A (/\) A1).k by Def5;
end;
hence thesis by PROB_1:13;
end;
theorem Th34:
Intersection (A (\/) A1) = A \/ Intersection A1
proof
thus Intersection (A (\/) A1) c= A \/ Intersection A1
proof
let x be object;
assume
A1: x in Intersection (A (\/) A1);
A2: now
let k;
x in (A (\/) A1).k by A1,PROB_1:13;
then x in (A \/ A1.k) by Def6;
hence x in A or x in A1.k by XBOOLE_0:def 3;
end;
per cases by A2;
suppose
x in A;
hence thesis by XBOOLE_0:def 3;
end;
suppose
x in A1.k;
then x in Intersection A1 by PROB_1:13;
hence thesis by XBOOLE_0:def 3;
end;
end;
let x be object;
assume
A3: x in A \/ Intersection A1;
per cases by A3,XBOOLE_0:def 3;
suppose
A4: x in A;
now
let k;
x in (A \/ A1.k) by A4,XBOOLE_0:def 3;
hence x in (A (\/) A1).k by Def6;
end;
hence thesis by PROB_1:13;
end;
suppose
A5: x in Intersection A1;
now
let k;
x in A1.k by A5,PROB_1:13;
then x in A \/ A1.k by XBOOLE_0:def 3;
hence x in (A (\/) A1).k by Def6;
end;
hence thesis by PROB_1:13;
end;
end;
theorem Th35:
Intersection (A (\) A1) c= A \ Intersection A1
proof
let x be object;
assume
A1: x in Intersection (A (\) A1);
A2: now
let k;
x in (A (\) A1).k by A1,PROB_1:13;
then x in (A \ A1.k) by Def7;
hence x in A & not x in A1.k by XBOOLE_0:def 5;
end;
then not x in A1.0;
then not x in Intersection A1 by PROB_1:13;
hence thesis by A2,XBOOLE_0:def 5;
end;
theorem Th36:
Intersection (A1 (\) A) = Intersection A1 \ A
proof
thus Intersection (A1 (\) A) c= Intersection A1 \ A
proof
let x be object;
assume
A1: x in Intersection (A1 (\) A);
A2: now
let k;
x in (A1 (\) A).k by A1,PROB_1:13;
then x in (A1.k \ A) by Def8;
hence x in A1.k & not x in A by XBOOLE_0:def 5;
end;
then x in Intersection A1 by PROB_1:13;
hence thesis by A2,XBOOLE_0:def 5;
end;
let x be object;
assume
A3: x in Intersection A1 \ A;
then
A4: x in Intersection A1 by XBOOLE_0:def 5;
now
let k;
x in A1.k & not x in A by A3,A4,PROB_1:13,XBOOLE_0:def 5;
then x in A1.k \ A by XBOOLE_0:def 5;
hence x in (A1 (\) A).k by Def8;
end;
hence thesis by PROB_1:13;
end;
theorem Th37:
Intersection (A (\+\) A1) c= A \+\ Intersection A1
proof
let x be object;
assume
A1: x in Intersection (A (\+\) A1);
A2: now
let n;
x in (A (\+\) A1).n by A1,PROB_1:13;
then x in A \+\ A1.n by Def9;
hence x in A & not x in A1.n or not x in A & x in A1.n by XBOOLE_0:1;
end;
assume not x in A \+\ Intersection A1;
then
A3: not x in A & not x in Intersection A1 or x in Intersection A1 & x in A
by XBOOLE_0:1;
per cases by A3,PROB_1:13;
suppose
not x in A & not for n holds x in A1.n;
hence contradiction by A2;
end;
suppose
A4: x in A & for n holds x in A1.n;
then x in A1.0;
hence contradiction by A2,A4;
end;
end;
theorem Th38:
Union (A (/\) A1) = A /\ Union A1
proof
thus Union (A (/\) A1) c= A /\ Union A1
proof
let x be object;
assume x in Union (A (/\) A1);
then consider n such that
A1: x in (A (/\) A1).n by PROB_1:12;
A2: x in A /\ A1.n by A1,Def5;
then x in A1.n by XBOOLE_0:def 4;
then
A3: x in Union A1 by PROB_1:12;
x in A by A2,XBOOLE_0:def 4;
hence thesis by A3,XBOOLE_0:def 4;
end;
let x be object;
assume
A4: x in A /\ Union A1;
then x in Union A1 by XBOOLE_0:def 4;
then consider n such that
A5: x in A1.n by PROB_1:12;
x in A by A4,XBOOLE_0:def 4;
then x in A /\ A1.n by A5,XBOOLE_0:def 4;
then x in (A (/\) A1).n by Def5;
hence thesis by PROB_1:12;
end;
theorem Th39:
Union (A (\/) A1) = A \/ Union A1
proof
thus Union (A (\/) A1) c= A \/ Union A1
proof
let x be object;
assume
A1: x in Union (A (\/) A1);
A2: x in A or ex k st x in A1.k
proof
consider k such that
A3: x in (A (\/) A1).k by A1,PROB_1:12;
x in (A \/ A1.k) by A3,Def6;
then x in A or x in A1.k by XBOOLE_0:def 3;
hence thesis;
end;
per cases by A2;
suppose
x in A;
hence thesis by XBOOLE_0:def 3;
end;
suppose
ex k st x in A1.k;
then x in Union A1 by PROB_1:12;
hence thesis by XBOOLE_0:def 3;
end;
end;
let x be object;
assume
A4: x in A \/ Union A1;
per cases by A4,XBOOLE_0:def 3;
suppose
x in A;
then x in (A \/ A1.1) by XBOOLE_0:def 3;
then x in (A (\/) A1).1 by Def6;
hence thesis by PROB_1:12;
end;
suppose
x in Union A1;
then consider k such that
A5: x in A1.k by PROB_1:12;
x in A \/ A1.k by A5,XBOOLE_0:def 3;
then x in (A (\/) A1).k by Def6;
hence thesis by PROB_1:12;
end;
end;
theorem Th40:
A \ Union A1 c= Union (A (\) A1)
proof
let x be object;
assume
A1: x in A \ Union A1;
then
A2: not x in Union A1 by XBOOLE_0:def 5;
now
let k;
x in A & not x in A1.k by A1,A2,PROB_1:12,XBOOLE_0:def 5;
then x in A \ A1.k by XBOOLE_0:def 5;
hence x in (A (\) A1).k by Def7;
end;
then x in (A (\) A1).1;
hence thesis by PROB_1:12;
end;
theorem Th41:
Union (A1 (\) A) = Union A1 \ A
proof
thus Union (A1 (\) A) c= Union A1 \ A
proof
let x be object;
assume
A1: x in Union (A1 (\) A);
A2: ex k st x in A1.k & not x in A
proof
consider k such that
A3: x in (A1 (\) A).k by A1,PROB_1:12;
x in A1.k \ A by A3,Def8;
then x in A1.k & not x in A by XBOOLE_0:def 5;
hence thesis;
end;
then x in Union A1 by PROB_1:12;
hence thesis by A2,XBOOLE_0:def 5;
end;
let x be object;
assume
A4: x in Union A1 \ A;
then
A5: not x in A by XBOOLE_0:def 5;
A6: x in Union A1 by A4,XBOOLE_0:def 5;
ex k st x in (A1 (\) A).k
proof
consider k such that
A7: x in A1.k by A6,PROB_1:12;
x in A1.k \ A by A5,A7,XBOOLE_0:def 5;
then x in (A1 (\) A).k by Def8;
hence thesis;
end;
hence thesis by PROB_1:12;
end;
theorem Th42:
A \+\ Union A1 c= Union (A (\+\) A1)
proof
let x be object;
assume
A1: x in A \+\ Union A1;
per cases by A1,XBOOLE_0:1;
suppose
A2: x in A & not x in Union A1;
then not x in A1.0 by PROB_1:12;
then x in A \+\ A1.0 by A2,XBOOLE_0:1;
then x in (A (\+\) A1).0 by Def9;
hence thesis by PROB_1:12;
end;
suppose
A3: not x in A & x in Union A1;
then consider n1 being Nat such that
A4: x in A1.n1 by PROB_1:12;
x in A \+\ A1.n1 by A3,A4,XBOOLE_0:1;
then x in (A (\+\) A1).n1 by Def9;
hence thesis by PROB_1:12;
end;
end;
theorem
(inferior_setsequence(A1 (/\) A2)).n = (inferior_setsequence A1).n /\
(inferior_setsequence A2).n
proof
(inferior_setsequence(A1 (/\) A2)).n = Intersection ((A1 (/\) A2) ^\n) by Th1
.= Intersection ((A1 ^\n) (/\) (A2 ^\n)) by Th4
.= Intersection (A1 ^\n) /\ Intersection (A2 ^\n) by Th12
.= (inferior_setsequence A1).n /\ Intersection (A2 ^\n) by Th1
.= (inferior_setsequence A1).n /\ (inferior_setsequence A2).n by Th1;
hence thesis;
end;
theorem
(inferior_setsequence A1).n \/ (inferior_setsequence A2).n c= (
inferior_setsequence(A1 (\/) A2)).n
proof
A1: Intersection ((A1 ^\n) (\/) (A2 ^\n)) = Intersection ((A1 (\/) A2) ^\n)
by Th5
.= (inferior_setsequence(A1 (\/) A2)).n by Th1;
(inferior_setsequence A1).n \/ (inferior_setsequence A2).n =
Intersection (A1 ^\n) \/ (inferior_setsequence A2).n by Th1
.= Intersection (A1 ^\n) \/ Intersection (A2 ^\n) by Th1;
hence thesis by A1,Th13;
end;
theorem
(inferior_setsequence(A1 (\) A2)).n c= (inferior_setsequence A1).n \ (
inferior_setsequence A2).n
proof
(inferior_setsequence(A1 (\) A2)).n = Intersection ((A1 (\) A2) ^\n) by Th1
.= Intersection ((A1 ^\n) (\) (A2 ^\n)) by Th6;
then (inferior_setsequence(A1 (\) A2)).n c= Intersection (A1 ^\n) \
Intersection (A2 ^\n) by Th14;
then (inferior_setsequence(A1 (\) A2)).n c= (inferior_setsequence A1).n \
Intersection (A2 ^\n) by Th1;
hence thesis by Th1;
end;
theorem
(superior_setsequence(A1 (/\) A2)).n c= (superior_setsequence A1).n /\
(superior_setsequence A2).n
proof
(superior_setsequence(A1 (/\) A2)).n = Union ((A1 (/\) A2) ^\n) by Th2
.= Union ((A1 ^\n) (/\) (A2 ^\n)) by Th4;
then
(superior_setsequence(A1 (/\) A2)).n c= Union (A1 ^\n) /\ Union (A2 ^\n)
by Th8;
then (superior_setsequence(A1 (/\) A2)).n c= (superior_setsequence A1).n /\
Union (A2 ^\n) by Th2;
hence thesis by Th2;
end;
theorem
(superior_setsequence(A1 (\/) A2)).n = (superior_setsequence A1).n \/
(superior_setsequence A2).n
proof
(superior_setsequence(A1 (\/) A2)).n = Union ((A1 (\/) A2) ^\n) by Th2
.= Union ((A1 ^\n) (\/) (A2 ^\n)) by Th5
.= Union (A1 ^\n) \/ Union (A2 ^\n) by Th9
.= (superior_setsequence A1).n \/ Union (A2 ^\n) by Th2;
hence thesis by Th2;
end;
theorem
(superior_setsequence A1).n \ (superior_setsequence A2).n c= (
superior_setsequence(A1 (\) A2)).n
proof
(superior_setsequence A1).n \ (superior_setsequence A2).n = Union (A1 ^\
n) \ (superior_setsequence A2).n by Th2
.= Union (A1 ^\n) \ Union (A2 ^\n) by Th2;
then
(superior_setsequence A1).n \ (superior_setsequence A2).n c= Union ((A1
^\n) (\) (A2 ^\n)) by Th10;
then
(superior_setsequence A1).n \ (superior_setsequence A2).n c= Union ((A1
(\) A2) ^\n) by Th6;
hence thesis by Th2;
end;
theorem
(superior_setsequence A1).n \+\ (superior_setsequence A2).n c= (
superior_setsequence(A1 (\+\) A2)).n
proof
(superior_setsequence A1).n \+\ (superior_setsequence A2).n = Union (A1
^\n) \+\ (superior_setsequence A2).n by Th2
.= Union (A1 ^\n) \+\ Union (A2 ^\n) by Th2;
then
(superior_setsequence A1).n \+\ (superior_setsequence A2).n c= Union ((
A1 ^\n) (\+\) (A2 ^\n)) by Th11;
then
(superior_setsequence A1).n \+\ (superior_setsequence A2).n c= Union ((
A1 (\+\) A2) ^\n) by Th7;
hence thesis by Th2;
end;
theorem Th50:
(inferior_setsequence(A (/\) A1)).n = A /\ (inferior_setsequence A1).n
proof
(inferior_setsequence(A (/\) A1)).n = Intersection ((A (/\) A1) ^\n) by Th1
.= Intersection (A (/\) (A1 ^\n)) by Th16
.= A /\ Intersection (A1 ^\n) by Th33
.= A /\ (inferior_setsequence A1).n by Th1;
hence thesis;
end;
theorem Th51:
(inferior_setsequence(A (\/) A1)).n = A \/ (inferior_setsequence A1).n
proof
(inferior_setsequence(A (\/) A1)).n = Intersection ((A (\/) A1) ^\n) by Th1
.= Intersection (A (\/) (A1 ^\n)) by Th17
.= A \/ Intersection (A1 ^\n) by Th34
.= A \/ (inferior_setsequence A1).n by Th1;
hence thesis;
end;
theorem
(inferior_setsequence(A (\) A1)).n c= A \ (inferior_setsequence A1).n
proof
(inferior_setsequence(A (\) A1)).n = Intersection ((A (\) A1) ^\n) by Th1
.= Intersection (A (\) (A1 ^\n)) by Th18;
then (inferior_setsequence(A (\) A1)).n c= A \ Intersection (A1 ^\n) by Th35;
hence thesis by Th1;
end;
theorem Th53:
(inferior_setsequence(A1 (\) A)).n = (inferior_setsequence A1).n \ A
proof
(inferior_setsequence(A1 (\) A)).n = Intersection ((A1 (\) A) ^\n) by Th1
.= Intersection ((A1 ^\n) (\) A) by Th19
.= Intersection (A1 ^\n) \ A by Th36
.= (inferior_setsequence A1).n \ A by Th1;
hence thesis;
end;
theorem
(inferior_setsequence(A (\+\) A1)).n c= A \+\ (inferior_setsequence A1 ).n
proof
(inferior_setsequence(A (\+\) A1)).n = Intersection ((A (\+\) A1) ^\n) by Th1
.= Intersection (A (\+\) (A1 ^\n)) by Th20;
then (inferior_setsequence(A (\+\) A1)).n c= A \+\ Intersection (A1 ^\n) by
Th37;
hence thesis by Th1;
end;
theorem Th55:
(superior_setsequence(A (/\) A1)).n = A /\ (superior_setsequence A1).n
proof
(superior_setsequence(A (/\) A1)).n = Union ((A (/\) A1) ^\n) by Th2
.= Union (A (/\) (A1 ^\n)) by Th16
.= A /\ Union (A1 ^\n) by Th38
.= A /\ (superior_setsequence A1).n by Th2;
hence thesis;
end;
theorem Th56:
(superior_setsequence(A (\/) A1)).n = A \/ (superior_setsequence A1).n
proof
(superior_setsequence(A (\/) A1)).n = Union ((A (\/) A1) ^\n) by Th2
.= Union (A (\/) (A1 ^\n)) by Th17
.= A \/ Union (A1 ^\n) by Th39
.= A \/ (superior_setsequence A1).n by Th2;
hence thesis;
end;
theorem
A \ (superior_setsequence A1).n c= (superior_setsequence(A (\) A1)).n
proof
A \ (superior_setsequence A1).n = A \ Union (A1 ^\n) by Th2;
then A \ (superior_setsequence A1).n c= Union (A (\) (A1 ^\n)) by Th40;
then A \ (superior_setsequence A1).n c= Union ((A (\) A1) ^\n) by Th18;
hence thesis by Th2;
end;
theorem Th58:
(superior_setsequence(A1 (\) A)).n = (superior_setsequence A1).n \ A
proof
reconsider X1 = (superior_setsequence(A1)) as SetSequence of X;
reconsider X2 = (superior_setsequence(A1 (\) A)) as SetSequence of X;
A1: X1.n \ A c= X2.n
proof
let x be object;
assume
A2: x in X1.n \ A;
then
A3: not x in A by XBOOLE_0:def 5;
A4: x in X1.n by A2,XBOOLE_0:def 5;
ex k st x in (A1 (\) A).(n+k)
proof
consider k such that
A5: x in A1.(n+k) by A4,SETLIM_1:20;
x in A1.(n+k) \ A by A3,A5,XBOOLE_0:def 5;
then x in (A1 (\) A).(n+k) by Def8;
hence thesis;
end;
hence thesis by SETLIM_1:20;
end;
X2.n c= X1.n \ A
proof
let x be object;
assume
A6: x in X2.n;
A7: ex k st x in A1.(n+k) & not x in A
proof
consider k such that
A8: x in (A1 (\) A).(n+k) by A6,SETLIM_1:20;
x in A1.(n+k) \ A by A8,Def8;
then x in A1.(n+k) & not x in A by XBOOLE_0:def 5;
hence thesis;
end;
then x in X1.n by SETLIM_1:20;
hence thesis by A7,XBOOLE_0:def 5;
end;
hence thesis by A1;
end;
theorem
A \+\ (superior_setsequence A1).n c= (superior_setsequence(A (\+\) A1) ).n
proof
A \+\ (superior_setsequence A1).n = A \+\ Union (A1 ^\n) by Th2;
then A \+\ (superior_setsequence A1).n c= Union (A (\+\) (A1 ^\n)) by Th42;
then A \+\ (superior_setsequence A1).n c= Union ((A (\+\) A1) ^\n) by Th20;
hence thesis by Th2;
end;
theorem Th60:
lim_inf (A1 (/\) A2) = lim_inf A1 /\ lim_inf A2
proof
(A1 (/\) A2).n = A1.n /\ A2.n by Def1;
hence thesis by KURATO_0:10;
end;
theorem Th61:
lim_inf A1 \/ lim_inf A2 c= lim_inf (A1 (\/) A2)
proof
(A1 (\/) A2).n = A1.n \/ A2.n by Def2;
hence thesis by KURATO_0:12;
end;
theorem Th62:
lim_inf (A1 (\) A2) c= lim_inf A1 \ lim_inf A2
proof
let x be object;
assume x in lim_inf (A1 (\) A2);
then consider n such that
A1: for k holds x in (A1 (\) A2).(n+k) by KURATO_0:4;
A2: now
let k;
x in (A1 (\) A2).(n+k) by A1;
then x in A1.(n+k) \ A2.(n+k) by Def3;
hence x in A1.(n+k) & not x in A2.(n+k) by XBOOLE_0:def 5;
end;
A3: not x in lim_inf A2
proof
assume x in lim_inf A2;
then consider n1 being Nat such that
A4: for k holds x in A2.(n1+k) by KURATO_0:4;
x in A2.(n1+n) by A4;
hence contradiction by A2;
end;
x in lim_inf A1 by A2,KURATO_0:4;
hence thesis by A3,XBOOLE_0:def 5;
end;
theorem Th63:
A1 is convergent or A2 is convergent implies lim_inf (A1 (\/) A2
) = lim_inf A1 \/ lim_inf A2
proof
A1: for A1,A2 st A1 is convergent holds lim_inf (A1 (\/) A2) = lim_inf A1 \/
lim_inf A2
proof
let A1,A2;
assume
A2: A1 is convergent;
thus lim_inf (A1 (\/) A2) c= lim_inf A1 \/ lim_inf A2
proof
let x be object;
assume x in lim_inf (A1 (\/) A2);
then consider n1 being Nat such that
A3: for k holds x in (A1 (\/) A2).(n1+k) by KURATO_0:4;
A4: now
let n;
x in (A1 (\/) A2).(n1+n) by A3;
then x in A1.(n1+n) \/ A2.(n1+n) by Def2;
hence x in A1.(n1+n) or x in A2.(n1+n) by XBOOLE_0:def 3;
end;
x in lim_inf A1 \/ lim_inf A2
proof
assume
A5: not x in lim_inf A1 \/ lim_inf A2;
then not x in lim_inf A1 by XBOOLE_0:def 3;
then not x in lim_sup A1 by A2,KURATO_0:def 5;
then consider n2 being Nat such that
A6: for k holds not x in A1.(n2+k) by KURATO_0:5;
not x in lim_inf A2 by A5,XBOOLE_0:def 3;
then consider k1 being Nat such that
A7: not x in A2.((n1+n2)+k1) by KURATO_0:4;
not x in A1.(n2+(n1+k1)) by A6;
then not x in A1.(n1+(n2+k1));
hence contradiction by A4,A7;
end;
hence thesis;
end;
thus thesis by Th61;
end;
assume
A8: A1 is convergent or A2 is convergent;
per cases by A8;
suppose
A1 is convergent;
hence thesis by A1;
end;
suppose
A2 is convergent;
hence thesis by A1;
end;
end;
theorem Th64:
A2 is convergent implies lim_inf (A1 (\) A2) = lim_inf A1 \ lim_inf A2
proof
assume
A1: A2 is convergent;
thus lim_inf (A1 (\) A2) c= lim_inf A1 \ lim_inf A2 by Th62;
thus lim_inf A1 \ lim_inf A2 c= lim_inf (A1 (\) A2)
proof
let x be object;
assume
A2: x in lim_inf A1 \ lim_inf A2;
then x in lim_inf A1 by XBOOLE_0:def 5;
then consider n0 being Nat such that
A3: for k holds x in A1.(n0+k) by KURATO_0:4;
not x in lim_inf A2 by A2,XBOOLE_0:def 5;
then not x in lim_sup A2 by A1,KURATO_0:def 5;
then consider n1 being Nat such that
A4: for k holds not x in A2.(n1+k) by KURATO_0:5;
now
let k;
x in A1.(n0+(n1+k)) & not x in A2.(n1+(n0+k)) by A3,A4;
then x in A1.((n0+n1)+k) \ A2.((n0+n1)+k) by XBOOLE_0:def 5;
hence x in (A1 (\) A2).((n0+n1)+k) by Def3;
end;
hence thesis by KURATO_0:4;
end;
end;
theorem Th65:
A1 is convergent or A2 is convergent implies lim_inf (A1 (\+\)
A2) c= lim_inf A1 \+\ lim_inf A2
proof
A1: for A1,A2 st A1 is convergent holds lim_inf (A1 (\+\) A2) c= lim_inf A1
\+\ lim_inf A2
proof
let A1,A2;
assume
A2: A1 is convergent;
thus lim_inf (A1 (\+\) A2) c= lim_inf A1 \+\ lim_inf A2
proof
let x be object;
assume x in lim_inf (A1 (\+\) A2);
then consider n1 being Nat such that
A3: for k holds x in (A1 (\+\) A2).(n1+k) by KURATO_0:4;
A4: now
let k;
x in (A1 (\+\) A2).(n1+k) by A3;
then x in A1.(n1+k) \+\ A2.(n1+k) by Def4;
hence x in A1.(n1+k) & not x in A2.(n1+k) or not x in A1.(n1+k) & x in
A2.(n1+k) by XBOOLE_0:1;
end;
assume
A5: not x in lim_inf A1 \+\ lim_inf A2;
per cases by A5,XBOOLE_0:1;
suppose
A6: not x in lim_inf A1 & not x in lim_inf A2;
then not x in lim_sup A1 by A2,KURATO_0:def 5;
then consider n2 being Nat such that
A7: for k holds not x in A1.(n2+k) by KURATO_0:5;
consider k1 being Nat such that
A8: not x in A2.((n1+n2)+k1) by A6,KURATO_0:4;
A9: x in A1.(n1+(n2+k1)) & not x in A2.(n1+(n2+k1)) or not x in A1.(
n1+(n2+k1)) & x in A2.(n1+(n2+k1)) by A4;
not x in A1.(n2+(n1+k1)) by A7;
hence contradiction by A8,A9;
end;
suppose
A10: x in lim_inf A1 & x in lim_inf A2;
then consider n3 being Nat such that
A11: for k holds x in A2.(n3+k) by KURATO_0:4;
consider n2 being Nat such that
A12: for k holds x in A1.(n2+k) by A10,KURATO_0:4;
A13: x in A1.(n1+(n2+n3)) & not x in A2.(n1+(n2+n3)) or not x in A1.(
n1+(n2+n3)) & x in A2.(n1+(n2+n3)) by A4;
A14: x in A2.(n3+(n1+n2)) by A11;
x in A1.(n2+(n1+n3)) by A12;
hence contradiction by A14,A13;
end;
end;
end;
assume
A15: A1 is convergent or A2 is convergent;
per cases by A15;
suppose
A1 is convergent;
hence thesis by A1;
end;
suppose
A2 is convergent;
hence thesis by A1;
end;
end;
theorem Th66:
A1 is convergent & A2 is convergent implies lim_inf (A1 (\+\) A2
) = lim_inf A1 \+\ lim_inf A2
proof
assume that
A1: A1 is convergent and
A2: A2 is convergent;
thus lim_inf (A1 (\+\) A2) c= lim_inf A1 \+\ lim_inf A2 by A1,Th65;
thus lim_inf A1 \+\ lim_inf A2 c= lim_inf (A1 (\+\) A2)
proof
let x be object;
assume
A3: x in lim_inf A1 \+\ lim_inf A2;
per cases by A3,XBOOLE_0:1;
suppose
A4: x in lim_inf A1 & not x in lim_inf A2;
then not x in lim_sup A2 by A2,KURATO_0:def 5;
then consider n2 being Nat such that
A5: for k holds not x in A2.(n2+k) by KURATO_0:5;
consider n1 being Nat such that
A6: for k holds x in A1.(n1+k) by A4,KURATO_0:4;
now
let k;
x in A1.(n1+(n2+k)) & not x in A2.(n2+(n1+k)) by A6,A5;
then x in A1.(n1+n2+k) \+\ A2.(n1+n2+k) by XBOOLE_0:1;
hence x in (A1 (\+\) A2). (n1+n2+k) by Def4;
end;
hence thesis by KURATO_0:4;
end;
suppose
A7: not x in lim_inf A1 & x in lim_inf A2;
then not x in lim_sup A1 by A1,KURATO_0:def 5;
then consider n3 being Nat such that
A8: for k holds not x in A1.(n3+k) by KURATO_0:5;
consider n4 being Nat such that
A9: for k holds x in A2.(n4+k) by A7,KURATO_0:4;
now
let k;
( not x in A1.(n3+(n4+k)))& x in A2.(n4+(n3+k)) by A8,A9;
then x in A1.(n3+n4+k) \+\ A2.(n3+n4+k) by XBOOLE_0:1;
hence x in (A1 (\+\) A2). (n3+n4+k) by Def4;
end;
hence thesis by KURATO_0:4;
end;
end;
end;
theorem Th67:
lim_sup (A1 (/\) A2) c= lim_sup A1 /\ lim_sup A2
proof
(A1 (/\) A2).n = A1.n /\ A2.n by Def1;
hence thesis by KURATO_0:13;
end;
theorem Th68:
lim_sup (A1 (\/) A2) = lim_sup A1 \/ lim_sup A2
proof
(A1 (\/) A2).n = A1.n \/ A2.n by Def2;
hence thesis by KURATO_0:11;
end;
theorem Th69:
lim_sup A1 \ lim_sup A2 c= lim_sup (A1 (\) A2)
proof
let x be object;
assume
A1: x in lim_sup A1 \ lim_sup A2;
then not x in lim_sup A2 by XBOOLE_0:def 5;
then consider n1 being Nat such that
A2: for k holds not x in A2.(n1+k) by KURATO_0:5;
assume not x in lim_sup (A1 (\) A2);
then consider n2 being Nat such that
A3: for k holds not x in (A1 (\) A2).(n2+k) by KURATO_0:5;
A4: now
let k;
not x in (A1 (\) A2).(n2+k) by A3;
then not x in A1.(n2+k) \ A2.(n2+k) by Def3;
hence not x in A1.(n2+k) or x in A2.(n2+k) by XBOOLE_0:def 5;
end;
x in lim_sup A1 by A1,XBOOLE_0:def 5;
then consider k1 being Nat such that
A5: x in A1.(n1+n2+k1) by KURATO_0:5;
A6: x in A1.(n2+(k1+n1)) by A5;
not x in A2.(n1+(n2+k1)) by A2;
hence contradiction by A4,A6;
end;
theorem
lim_sup A1 \+\ lim_sup A2 c= lim_sup (A1 (\+\) A2)
proof
let x be object;
A1: for A1,A2 st x in lim_sup A1 & not x in lim_sup A2 holds x in lim_sup (
A1 (\+\) A2)
proof
let A1,A2;
assume that
A2: x in lim_sup A1 and
A3: not x in lim_sup A2;
consider n1 being Nat such that
A4: for k holds not x in A2.(n1+k) by A3,KURATO_0:5;
now
let n;
consider k1 being Nat such that
A5: x in A1.((n+n1)+k1) by A2,KURATO_0:5;
not x in A2.(n1+(n+k1)) by A4;
then x in A1.(n+(n1+k1)) \+\ A2.(n+(n1+k1)) by A5,XBOOLE_0:1;
then x in (A1 (\+\) A2).(n+(n1+k1)) by Def4;
hence ex k st x in (A1 (\+\) A2).(n+k);
end;
hence thesis by KURATO_0:5;
end;
assume
A6: x in lim_sup A1 \+\ lim_sup A2;
per cases by A6,XBOOLE_0:1;
suppose
x in lim_sup A1 & not x in lim_sup A2;
hence thesis by A1;
end;
suppose
not x in lim_sup A1 & x in lim_sup A2;
hence thesis by A1;
end;
end;
theorem Th71:
A1 is convergent or A2 is convergent implies lim_sup (A1 (/\) A2
) = lim_sup A1 /\ lim_sup A2
proof
A1: for A1,A2 st A1 is convergent holds lim_sup (A1 (/\) A2) = lim_sup A1 /\
lim_sup A2
proof
let A1,A2;
assume
A2: A1 is convergent;
thus lim_sup (A1 (/\) A2) c= lim_sup A1 /\ lim_sup A2 by Th67;
thus lim_sup A1 /\ lim_sup A2 c= lim_sup (A1 (/\) A2)
proof
let x be object;
assume
A3: x in lim_sup A1 /\ lim_sup A2;
then x in lim_sup A1 by XBOOLE_0:def 4;
then x in lim_inf A1 by A2,KURATO_0:def 5;
then consider n1 being Nat such that
A4: for k holds x in A1.(n1+k) by KURATO_0:4;
A5: x in lim_sup A2 by A3,XBOOLE_0:def 4;
now
let n;
consider k1 being Nat such that
A6: x in A2.((n+n1)+k1) by A5,KURATO_0:5;
x in A1.(n1+(n+k1)) by A4;
then x in A1.(n+(n1+k1)) /\ A2.(n+(n1+k1)) by A6,XBOOLE_0:def 4;
then x in (A1 (/\) A2).(n+(n1+k1)) by Def1;
hence ex k st x in (A1 (/\) A2).(n+k);
end;
hence thesis by KURATO_0:5;
end;
end;
assume
A7: A1 is convergent or A2 is convergent;
per cases by A7;
suppose
A1 is convergent;
hence thesis by A1;
end;
suppose
A2 is convergent;
hence thesis by A1;
end;
end;
theorem Th72:
A2 is convergent implies lim_sup (A1 (\) A2) = lim_sup A1 \ lim_sup A2
proof
assume
A1: A2 is convergent;
thus lim_sup (A1 (\) A2) c= lim_sup A1 \ lim_sup A2
proof
let x be object;
assume
A2: x in lim_sup (A1 (\) A2);
A3: now
let n;
consider k1 being Nat such that
A4: x in (A1 (\) A2).(n+k1) by A2,KURATO_0:5;
x in A1.(n+k1) \ A2.(n+k1) by A4,Def3;
then x in A1.(n+k1) & not x in A2.(n+k1) by XBOOLE_0:def 5;
hence ex k st x in A1.(n+k) & not x in A2.(n+k);
end;
assume not x in lim_sup A1 \ lim_sup A2;
then
A5: not (x in lim_sup A1 & not x in lim_sup A2) by XBOOLE_0:def 5;
per cases by A1,A5,KURATO_0:def 5;
suppose
not x in lim_sup A1;
then consider n1 being Nat such that
A6: for k holds not x in A1.(n1+k) by KURATO_0:5;
ex k2 being Nat st x in A1.(n1+k2) & not x in A2.(n1+k2)
by A3;
hence contradiction by A6;
end;
suppose
x in lim_inf A2;
then consider n2 being Nat such that
A7: for k holds x in A2.(n2+k) by KURATO_0:4;
ex k3 being Nat st x in A1.(n2+k3) & not x in A2.(n2+k3)
by A3;
hence contradiction by A7;
end;
end;
thus thesis by Th69;
end;
theorem Th73:
A1 is convergent & A2 is convergent implies lim_sup (A1 (\+\) A2
) = lim_sup A1 \+\ lim_sup A2
proof
assume that
A1: A1 is convergent and
A2: A2 is convergent;
thus lim_sup (A1 (\+\) A2) = lim_sup ((A1 (\) A2) (\/) (A2 (\) A1)) by Th3
.= lim_sup (A1 (\) A2) \/ lim_sup (A2 (\) A1) by Th68
.= (lim_sup A1 \ lim_sup A2) \/ lim_sup (A2 (\) A1) by A2,Th72
.= lim_sup A1 \+\ lim_sup A2 by A1,Th72;
end;
theorem Th74:
lim_inf (A (/\) A1) = A /\ lim_inf A1
proof
reconsider X1 = (inferior_setsequence(A1)) as SetSequence of X;
reconsider X2 = (inferior_setsequence(A (/\) A1)) as SetSequence of X;
X2 = A (/\) X1
proof
let n be Element of NAT;
thus X2.n = A /\ X1.n by Th50
.= (A (/\) X1).n by Def5;
end;
then Union X2 = A /\ Union X1 by Th38;
then lim_inf (A (/\) A1) = A /\ Union X1 by SETLIM_1:def 4;
hence thesis by SETLIM_1:def 4;
end;
theorem Th75:
lim_inf (A (\/) A1) = A \/ lim_inf A1
proof
reconsider X1 = (inferior_setsequence(A1)) as SetSequence of X;
reconsider X2 = (inferior_setsequence(A (\/) A1)) as SetSequence of X;
X2 = A (\/) X1
proof
let n be Element of NAT;
thus X2.n = A \/ X1.n by Th51
.= (A (\/) X1).n by Def6;
end;
then Union X2 = A \/ Union X1 by Th39;
then lim_inf (A (\/) A1) = A \/ Union X1 by SETLIM_1:def 4;
hence thesis by SETLIM_1:def 4;
end;
theorem Th76:
lim_inf (A (\) A1) c= A \ lim_inf A1
proof
let x be object;
assume x in lim_inf (A (\) A1);
then consider n such that
A1: for k holds x in (A (\) A1).(n+k) by KURATO_0:4;
A2: now
let k;
x in (A (\) A1).(n+k) by A1;
then x in A \ A1.(n+k) by Def7;
hence x in A & not x in A1.(n+k) by XBOOLE_0:def 5;
end;
not x in lim_inf A1
proof
assume x in lim_inf A1;
then consider n1 being Nat such that
A3: for k holds x in A1.(n1+k) by KURATO_0:4;
x in A1.(n1+n) by A3;
hence contradiction by A2;
end;
hence thesis by A2,XBOOLE_0:def 5;
end;
theorem Th77:
lim_inf (A1 (\) A) = lim_inf A1 \ A
proof
reconsider X1 = (inferior_setsequence(A1)) as SetSequence of X;
reconsider X2 = (inferior_setsequence(A1 (\) A)) as SetSequence of X;
X2 = X1 (\) A
proof
let n be Element of NAT;
thus X2.n = X1.n \ A by Th53
.= (X1 (\) A).n by Def8;
end;
then Union X2 = Union X1 \ A by Th41;
then lim_inf (A1 (\) A) = Union X1 \ A by SETLIM_1:def 4;
hence thesis by SETLIM_1:def 4;
end;
theorem Th78:
lim_inf (A (\+\) A1) c= A \+\ lim_inf A1
proof
let x be object;
assume x in lim_inf (A (\+\) A1);
then consider n1 being Nat such that
A1: for k holds x in (A (\+\) A1).(n1+k) by KURATO_0:4;
A2: now
let k;
x in (A (\+\) A1).(n1+k) by A1;
then x in A \+\ A1.(n1+k) by Def9;
hence x in A & not x in A1.(n1+k) or not x in A & x in A1.(n1+k) by
XBOOLE_0:1;
end;
assume not x in A \+\ lim_inf A1;
then
A3: not x in A & not x in lim_inf A1 or x in lim_inf A1 & x in A by XBOOLE_0:1;
per cases by A3,KURATO_0:4;
suppose
A4: not x in A & not ex n st for k holds x in A1.(n+k);
then ex k1 being Nat st not x in A1.(n1+k1);
hence contradiction by A2,A4;
end;
suppose
A5: x in A & ex n st for k holds x in A1.(n+k);
then consider n2 being Nat such that
A6: for k holds x in A1.(n2+k);
x in A1.(n2+n1) by A6;
hence contradiction by A2,A5;
end;
end;
theorem Th79:
A1 is convergent implies lim_inf (A (\) A1) = A \ lim_inf A1
proof
assume
A1: A1 is convergent;
thus lim_inf (A (\) A1) c= A \ lim_inf A1 by Th76;
thus A \ lim_inf A1 c= lim_inf (A (\) A1)
proof
let x be object;
assume
A2: x in A \ lim_inf A1;
then x in A \ lim_sup A1 by A1,KURATO_0:def 5;
then not x in lim_sup A1 by XBOOLE_0:def 5;
then consider n1 being Nat such that
A3: for k holds not x in A1.(n1+k) by KURATO_0:5;
assume
A4: not x in lim_inf (A (\) A1);
A5: for n holds not x in A or ex k st x in A1.(n+k)
proof
let n;
consider k such that
A6: not x in (A (\) A1).(n+k) by A4,KURATO_0:4;
not x in A \ A1.(n+k) by A6,Def7;
then not ( x in A & not x in A1.(n+k)) by XBOOLE_0:def 5;
hence thesis;
end;
per cases by A5;
suppose
not x in A;
hence contradiction by A2,XBOOLE_0:def 5;
end;
suppose
ex k st x in A1.(n1+k);
hence contradiction by A3;
end;
end;
end;
theorem Th80:
A1 is convergent implies lim_inf (A (\+\) A1) = A \+\ lim_inf A1
proof
assume
A1: A1 is convergent;
thus lim_inf (A (\+\) A1) c= A \+\ lim_inf A1 by Th78;
thus A \+\ lim_inf A1 c= lim_inf (A (\+\) A1)
proof
let x be object;
assume
A2: x in A \+\ lim_inf A1;
per cases by A2,XBOOLE_0:1;
suppose
A3: x in A & not x in lim_inf A1;
then not x in lim_sup A1 by A1,KURATO_0:def 5;
then consider n1 being Nat such that
A4: for k holds not x in A1.(n1+k) by KURATO_0:5;
now
let k;
not x in A1.(n1+k) by A4;
then x in A \+\ A1.(n1+k) by A3,XBOOLE_0:1;
hence x in (A (\+\) A1).(n1+k) by Def9;
end;
hence thesis by KURATO_0:4;
end;
suppose
A5: not x in A & x in lim_inf A1;
then consider n2 being Nat such that
A6: for k holds x in A1.(n2+k) by KURATO_0:4;
now
let k;
x in A1.(n2+k) by A6;
then x in A \+\ A1.(n2+k) by A5,XBOOLE_0:1;
hence x in (A (\+\) A1).(n2+k) by Def9;
end;
hence thesis by KURATO_0:4;
end;
end;
end;
theorem Th81:
lim_sup (A (/\) A1) = A /\ lim_sup A1
proof
reconsider X1 = (superior_setsequence(A1)) as SetSequence of X;
reconsider X2 = (superior_setsequence(A (/\) A1)) as SetSequence of X;
X2 = A (/\) X1
proof
let n be Element of NAT;
thus X2.n = A /\ X1.n by Th55
.= (A (/\) X1).n by Def5;
end;
then Intersection X2 = A /\ Intersection X1 by Th33;
then lim_sup (A (/\) A1) = A /\ Intersection X1 by SETLIM_1:def 5;
hence thesis by SETLIM_1:def 5;
end;
theorem Th82:
lim_sup (A (\/) A1) = A \/ lim_sup A1
proof
reconsider X1 = (superior_setsequence(A1)) as SetSequence of X;
reconsider X2 = (superior_setsequence(A (\/) A1)) as SetSequence of X;
X2 = A (\/) X1
proof
let n be Element of NAT;
thus X2.n = A \/ X1.n by Th56
.= (A (\/) X1).n by Def6;
end;
then Intersection X2 = A \/ Intersection X1 by Th34;
then lim_sup (A (\/) A1) = A \/ Intersection X1 by SETLIM_1:def 5;
hence thesis by SETLIM_1:def 5;
end;
theorem Th83:
A \ lim_sup A1 c= lim_sup (A (\) A1)
proof
let x be object;
assume
A1: x in A \ lim_sup A1;
then not x in lim_sup A1 by XBOOLE_0:def 5;
then consider n1 being Nat such that
A2: for k holds not x in A1.(n1+k) by KURATO_0:5;
assume not x in lim_sup (A (\) A1);
then consider n such that
A3: for k holds not x in (A (\) A1).(n+k) by KURATO_0:5;
A4: now
let k;
not x in (A (\) A1).(n+k) by A3;
then not x in A \ A1.(n+k) by Def7;
hence not x in A or x in A1.(n+k) by XBOOLE_0:def 5;
end;
per cases by A4;
suppose
not x in A;
hence contradiction by A1,XBOOLE_0:def 5;
end;
suppose
A5: x in A1.(n+k);
not x in A1.(n1+n) by A2;
hence contradiction by A5;
end;
end;
theorem Th84:
lim_sup (A1 (\) A) = lim_sup A1 \ A
proof
reconsider X1 = (superior_setsequence(A1)) as SetSequence of X;
reconsider X2 = (superior_setsequence(A1 (\) A)) as SetSequence of X;
X2 = X1 (\) A
proof
let n be Element of NAT;
thus X2.n = X1.n \ A by Th58
.= (X1 (\) A).n by Def8;
end;
then Intersection X2 = Intersection X1 \ A by Th36;
then lim_sup (A1 (\) A) = Intersection X1 \ A by SETLIM_1:def 5;
hence thesis by SETLIM_1:def 5;
end;
theorem Th85:
A \+\ lim_sup A1 c= lim_sup (A (\+\) A1)
proof
(A (\+\) A1).n = A \+\ A1.n by Def9;
hence thesis by KURATO_0:17;
end;
theorem Th86:
A1 is convergent implies lim_sup (A (\) A1) = A \ lim_sup A1
proof
assume
A1: A1 is convergent;
thus lim_sup (A (\) A1) c= A \ lim_sup A1
proof
let x be object;
assume
A2: x in lim_sup (A (\) A1);
A3: for n ex k st x in A & not x in A1.(n+k)
proof
let n;
consider k such that
A4: x in (A (\) A1).(n+k) by A2,KURATO_0:5;
x in A \ A1.(n+k) by A4,Def7;
then x in A & not x in A1.(n+k) by XBOOLE_0:def 5;
hence thesis;
end;
A5: x in A
proof
A6: for n holds ex k st x in A
proof
let n;
ex k st x in A & not x in A1.(n+k) by A3;
hence thesis;
end;
assume not x in A;
then for n holds not x in A;
hence contradiction by A6;
end;
for n holds ex k st not x in A1.(n+k)
proof
let n;
ex k st x in A & not x in A1.(n+k) by A3;
hence thesis;
end;
then not x in lim_inf A1 by KURATO_0:4;
then not x in lim_sup A1 by A1,KURATO_0:def 5;
hence thesis by A5,XBOOLE_0:def 5;
end;
thus thesis by Th83;
end;
theorem Th87:
A1 is convergent implies lim_sup (A (\+\) A1) = A \+\ lim_sup A1
proof
assume
A1: A1 is convergent;
thus lim_sup (A (\+\) A1) c= A \+\ lim_sup A1
proof
let x be object;
assume
A2: x in lim_sup (A (\+\) A1);
A3: now
let n;
consider k1 being Nat such that
A4: x in (A (\+\) A1).(n+k1) by A2,KURATO_0:5;
x in A \+\ A1.(n+k1) by A4,Def9;
then x in A & not x in A1.(n+k1) or not x in A & x in A1.(n+k1) by
XBOOLE_0:1;
hence ex k st x in A & not x in A1.(n+k) or not x in A & x in A1.(n+k);
end;
assume
A5: not x in A \+\ lim_sup A1;
per cases by A5,XBOOLE_0:1;
suppose
A6: not x in A & not x in lim_sup A1;
then consider n1 being Nat such that
A7: for k holds not x in A1.(n1+k) by KURATO_0:5;
ex k1 being Nat st ( x in A & not x in A1.(n1+k1 ) or not
x in A & x in A1.(n1+k1)) by A3;
hence contradiction by A6,A7;
end;
suppose
A8: x in A & x in lim_sup A1;
then x in lim_inf A1 by A1,KURATO_0:def 5;
then consider n2 being Nat such that
A9: for k holds x in A1.(n2+k) by KURATO_0:4;
ex k2 being Nat st ( x in A & not x in A1.(n2+k2 ) or not
x in A & x in A1.(n2+k2)) by A3;
hence contradiction by A8,A9;
end;
end;
thus thesis by Th85;
end;
theorem
A1 is convergent & A2 is convergent implies (A1 (/\) A2) is convergent
& lim (A1 (/\) A2) = lim A1 /\ lim A2
proof
assume that
A1: A1 is convergent and
A2: A2 is convergent;
A3: lim_sup (A1 (/\) A2) = lim A1 /\ lim A2 by A1,Th71;
lim_inf (A1 (/\) A2) = lim_inf A1 /\ lim_inf A2 by Th60
.= lim A1 /\ lim_inf A2 by A1,KURATO_0:def 5
.= lim A1 /\ lim A2 by A2,KURATO_0:def 5;
hence thesis by A3,KURATO_0:def 5;
end;
theorem
A1 is convergent & A2 is convergent implies (A1 (\/) A2) is convergent
& lim (A1 (\/) A2) = lim A1 \/ lim A2
proof
assume that
A1: A1 is convergent and
A2: A2 is convergent;
A3: lim_sup (A1 (\/) A2) = lim A1 \/ lim A2 by Th68;
lim_inf (A1 (\/) A2) = lim_inf A1 \/ lim_inf A2 by A1,Th63
.= lim A1 \/ lim_inf A2 by A1,KURATO_0:def 5
.= lim A1 \/ lim A2 by A2,KURATO_0:def 5;
hence thesis by A3,KURATO_0:def 5;
end;
theorem
A1 is convergent & A2 is convergent implies (A1 (\) A2) is convergent
& lim (A1 (\) A2) = lim A1 \ lim A2
proof
assume that
A1: A1 is convergent and
A2: A2 is convergent;
A3: lim_sup (A1 (\) A2) = lim A1 \ lim A2 by A2,Th72;
lim_inf (A1 (\) A2) = lim_inf A1 \ lim_inf A2 by A2,Th64
.= lim A1 \ lim_inf A2 by A1,KURATO_0:def 5
.= lim A1 \ lim A2 by A2,KURATO_0:def 5;
hence thesis by A3,KURATO_0:def 5;
end;
theorem
A1 is convergent & A2 is convergent implies (A1 (\+\) A2) is
convergent & lim (A1 (\+\) A2) = lim A1 \+\ lim A2
proof
assume that
A1: A1 is convergent and
A2: A2 is convergent;
A3: lim_sup (A1 (\+\) A2) = lim A1 \+\ lim A2 by A1,A2,Th73;
lim_inf (A1 (\+\) A2) = lim_inf A1 \+\ lim_inf A2 by A1,A2,Th66
.= lim A1 \+\ lim_inf A2 by A1,KURATO_0:def 5
.= lim A1 \+\ lim A2 by A2,KURATO_0:def 5;
hence thesis by A3,KURATO_0:def 5;
end;
theorem
A1 is convergent implies (A (/\) A1) is convergent & lim (A (/\) A1) =
A /\ lim A1
proof
assume
A1: A1 is convergent;
A2: lim_inf (A (/\) A1) = A /\ lim_inf A1 by Th74
.= A /\ lim A1 by A1,KURATO_0:def 5;
then lim_sup (A (/\) A1) = lim_inf (A (/\) A1) by Th81;
hence thesis by A2,KURATO_0:def 5;
end;
theorem
A1 is convergent implies (A (\/) A1) is convergent & lim (A (\/) A1) =
A \/ lim A1
proof
assume
A1: A1 is convergent;
A2: lim_inf (A (\/) A1) = A \/ lim_inf A1 by Th75
.= A \/ lim A1 by A1,KURATO_0:def 5;
then lim_sup (A (\/) A1) = lim_inf (A (\/) A1) by Th82;
hence thesis by A2,KURATO_0:def 5;
end;
theorem
A1 is convergent implies (A (\) A1) is convergent & lim (A (\) A1) = A
\ lim A1
proof
assume
A1: A1 is convergent;
then
A2: lim_inf (A (\) A1) = A \ lim_inf A1 by Th79
.= A \ lim A1 by A1,KURATO_0:def 5;
then lim_sup (A (\) A1) = lim_inf (A (\) A1) by A1,Th86;
hence thesis by A2,KURATO_0:def 5;
end;
theorem
A1 is convergent implies (A1 (\) A) is convergent & lim (A1 (\) A) =
lim A1 \ A
proof
assume
A1: A1 is convergent;
A2: lim_inf (A1 (\) A) = lim_inf A1 \ A by Th77
.= lim A1 \ A by A1,KURATO_0:def 5;
then lim_sup (A1 (\) A) = lim_inf (A1 (\) A) by Th84;
hence thesis by A2,KURATO_0:def 5;
end;
theorem
A1 is convergent implies (A (\+\) A1) is convergent & lim (A (\+\) A1)
= A \+\ lim A1
proof
assume
A1: A1 is convergent;
then
A2: lim_inf (A (\+\) A1) = A \+\ lim_inf A1 by Th80
.= A \+\ lim A1 by A1,KURATO_0:def 5;
then lim_sup (A (\+\) A1) = lim_inf (A (\+\) A1) by A1,Th87;
hence thesis by A2,KURATO_0:def 5;
end;