:: On the {K}uratowski Limit Operators I
:: by Adam Grabowski
::
:: Received August 12, 2003
:: Copyright (c) 2003-2021 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies NUMBERS, FUNCT_1, RELAT_1, SETFAM_1, TARSKI, XBOOLE_0, ZFMISC_1,
PROB_1, SUBSET_1, FUNCOP_1, CARD_3, ORDINAL2, NAT_1, ARYTM_3, CARD_1,
XXREAL_0, SEQ_2, KURATO_2;
notations TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, ZFMISC_1,
XXREAL_0, REAL_1, NAT_1, SETFAM_1, MCART_1, DOMAIN_1, RELAT_1, FUNCT_1,
INT_1, FINSEQ_1, RELSET_1, FUNCT_2, FUNCOP_1, CARD_3, PROB_1, VALUED_0,
FUNCT_6;
constructors SETFAM_1, REAL_1, PROB_1, LIMFUNC1, FUNCT_6, FINSEQ_1, DOMAIN_1,
NAT_1, RELSET_1;
registrations XBOOLE_0, SUBSET_1, RELAT_1, ORDINAL1, FUNCT_2, XREAL_0, NAT_1,
FUNCOP_1, RELSET_1;
requirements SUBSET, BOOLE, NUMERALS, ARITHM;
begin
theorem :: KURATO_0:1
for F being Function, i being set st i in dom F holds meet F c= F.i;
theorem :: KURATO_0:2
for A, B, C, D being set st A meets B & C meets D
holds [: A, C :] meets [: B, D :];
registration
let X be set;
cluster -> non empty for SetSequence of X;
end;
registration
let T be non empty set;
cluster non-empty for SetSequence of T;
end;
definition
let X be set, F be SetSequence of X;
redefine func Union F -> Subset of X;
redefine func meet F -> Subset of X;
end;
begin :: Lower and Upper Limit of Sequences of Subsets
definition
let X be set, F be SetSequence of X;
func lim_inf F -> Subset of X means
:: KURATO_0:def 1
ex f being SetSequence of X st it
= Union f & for n being Nat holds f.n = meet (F ^\ n);
func lim_sup F -> Subset of X means
:: KURATO_0:def 2
ex f being SetSequence of X st it
= meet f & for n being Nat holds f.n = Union (F ^\ n);
end;
theorem :: KURATO_0:3
for X being set, F being SetSequence of X, x being object
holds x in meet F iff for z being Nat holds x in F.z;
theorem :: KURATO_0:4
for X being set, F being SetSequence of X, x being object holds x in
lim_inf F iff ex n being Nat st for k being Nat holds x
in F.(n+k);
theorem :: KURATO_0:5
for X being set, F being SetSequence of X, x being object holds x in
lim_sup F iff for n being Nat ex k being Nat st x in F.(n
+k);
theorem :: KURATO_0:6
for X being set, F being SetSequence of X holds lim_inf F c= lim_sup F;
theorem :: KURATO_0:7
for X being set, F being SetSequence of X holds meet F c= lim_inf F;
theorem :: KURATO_0:8
for X being set, F being SetSequence of X holds lim_sup F c= Union F;
theorem :: KURATO_0:9
for X being set, F being SetSequence of X
holds lim_inf F = (lim_sup Complement F)`;
theorem :: KURATO_0:10
for X being set, A, B, C being SetSequence of X
st for n being Nat holds C.n = A.n /\ B.n
holds lim_inf C = lim_inf A /\ lim_inf B;
theorem :: KURATO_0:11
for X being set, A, B, C being SetSequence of X
st for n being Nat holds C.n = A.n \/ B.n
holds lim_sup C = lim_sup A \/ lim_sup B;
theorem :: KURATO_0:12
for X being set, A, B, C being SetSequence of X
st for n being Nat holds C.n = A.n \/ B.n
holds lim_inf A \/ lim_inf B c= lim_inf C;
theorem :: KURATO_0:13
for X being set, A, B, C being SetSequence of X st (for n being
Nat holds C.n = A.n /\ B.n) holds lim_sup C c= lim_sup A /\ lim_sup
B;
theorem :: KURATO_0:14
for X being set, A being SetSequence of X, B being Subset of X
st (for n being Nat holds A.n = B) holds lim_sup A = B;
theorem :: KURATO_0:15
for X being set, A being SetSequence of X, B being Subset of X
st (for n being Nat holds A.n = B) holds lim_inf A = B;
theorem :: KURATO_0:16
for X being set, A, B being SetSequence of X, C being Subset of X st (
for n being Nat holds B.n = C \+\ A.n) holds C \+\ lim_inf A c=
lim_sup B;
theorem :: KURATO_0:17
for X being set, A, B being SetSequence of X, C being Subset of X st (
for n being Nat holds B.n = C \+\ A.n) holds C \+\ lim_sup A c=
lim_sup B;
begin :: Ascending and Descending Families of Subsets
theorem :: KURATO_0:18
for f being Function st (for i being Nat holds f.(i+1
) c= f.i) for i, j being Nat st i <= j holds f.j c= f.i;
definition
let T be set, S be SetSequence of T;
redefine attr S is non-ascending means
:: KURATO_0:def 3
for i being Nat holds S.(i+1) c= S.i;
redefine attr S is non-descending means
:: KURATO_0:def 4
for i being Nat holds S.i c= S.(i+1);
end;
theorem :: KURATO_0:19
for T being set, F being SetSequence of T, x being object st F is
non-ascending & ex k being Nat st for n being Nat st n >
k holds x in F.n holds x in meet F;
theorem :: KURATO_0:20
for T being set, F being SetSequence of T st F is non-ascending holds
lim_inf F = meet F;
theorem :: KURATO_0:21
for T being set, F being SetSequence of T st F is non-descending holds
lim_sup F = Union F;
begin :: Constant and Convergent Sequences
definition
let T be set, S be SetSequence of T;
attr S is convergent means
:: KURATO_0:def 5
lim_sup S = lim_inf S;
end;
theorem :: KURATO_0:22
for T being set, S being SetSequence of T st S is constant holds
the_value_of S is Subset of T;
registration
let T be set;
cluster constant -> convergent non-descending non-ascending for
SetSequence of T;
end;
registration
let T be set;
cluster constant non empty for SetSequence of T;
end;
notation
let T be set, S be convergent SetSequence of T;
synonym Lim_K S for lim_sup S;
end;
theorem :: KURATO_0:23
for X being set, F being convergent SetSequence of X, x being set
holds x in Lim_K F iff ex n being Nat st for k being Nat
holds x in F.(n+k);