:: On the {K}uratowski Limit Operators
:: by Adam Grabowski
::
:: Received August 12, 2003
:: Copyright (c) 2003-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 NUMBERS, FUNCT_1, RELAT_1, SETFAM_1, TARSKI, XBOOLE_0, ZFMISC_1,
PROB_1, SUBSET_1, STRUCT_0, CARD_3, ORDINAL2, NAT_1, ARYTM_3, CARD_1,
XXREAL_0, SEQ_2, FINSEQ_1, EUCLID, TOPREAL1, RCOMP_1, PRE_TOPC, METRIC_1,
REAL_1, COMPLEX1, ARYTM_1, SEQ_1, INT_1, PCOMPS_1, FRECHET, RLVECT_3,
YELLOW_8, CONNSP_2, TOPS_1, JORDAN2C, XXREAL_2, VALUED_0, MCART_1,
TOPREAL2, JORDAN9, GOBOARD9, WAYBEL_7, KURATO_2;
notations TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, ZFMISC_1,
XXREAL_0, XREAL_0, REAL_1, SETFAM_1, XTUPLE_0, MCART_1, DOMAIN_1,
KURATO_0, RELAT_1, FUNCT_1, INT_1, FINSEQ_1, RELSET_1, FUNCT_2, NAT_1,
STRUCT_0, PRE_TOPC, TOPS_1, TOPS_2, COMPTS_1, METRIC_1, TBSP_1, PCOMPS_1,
RLVECT_1, RLTOPSP1, EUCLID, BORSUK_1, CARD_3, PROB_1, CONNSP_2, TOPREAL1,
TOPREAL2, JORDAN2C, VALUED_0, GOBOARD9, YELLOW_8, FRECHET, FRECHET2,
TOPRNS_1, JORDAN9;
constructors REAL_1, TOPS_1, BORSUK_1, TBSP_1, MONOID_0, TOPRNS_1, TOPREAL2,
GOBOARD9, FUNCSDOM, FRECHET, JORDAN2C, FRECHET2, JORDAN9, YELLOW_8,
TOPS_2, KURATO_0, XTUPLE_0, JORDAN11;
registrations SUBSET_1, RELAT_1, ORDINAL1, FUNCT_2, XREAL_0, NAT_1, INT_1,
STRUCT_0, TOPS_1, METRIC_1, PCOMPS_1, BORSUK_1, MONOID_0, EUCLID,
TOPREAL2, TOPREAL5, JORDAN2C, VALUED_0, PRE_TOPC, SPPOL_1, RELSET_1;
requirements REAL, SUBSET, BOOLE, NUMERALS, ARITHM;
begin
definition
let T be 1-sorted;
mode SetSequence of T is SetSequence of the carrier of T;
end;
begin :: Topological Lemmas
reserve n for Nat;
registration
let f be FinSequence of the carrier of TOP-REAL 2;
cluster L~f -> closed;
end;
theorem :: KURATO_2:1
for x being Point of Euclid n, r being Real holds Ball (x
, r) is open Subset of TOP-REAL n;
theorem :: KURATO_2:2
for p being Point of Euclid n, x, p9 being Point of TOP-REAL n,
r being Real st p = p9 & x in Ball (p, r) holds |. x - p9 .| < r;
theorem :: KURATO_2:3
for p being Point of Euclid n, x, p9 being Point of TOP-REAL n,
r being Real st p = p9 & |. x - p9 .| < r holds x in Ball (p, r);
theorem :: KURATO_2:4
for n being Nat, r being Point of TOP-REAL n, X being
Subset of TOP-REAL n st r in Cl X holds ex seq being Real_Sequence of n st rng
seq c= X & seq is convergent & lim seq = r;
registration
let M be non empty MetrSpace;
cluster TopSpaceMetr M -> first-countable;
end;
theorem :: KURATO_2:5
for T being non empty TopSpace holds T is first-countable iff
the TopStruct of T is first-countable;
registration
let n be Nat;
cluster TOP-REAL n -> first-countable;
end;
theorem :: KURATO_2:6
for A being Subset of TOP-REAL n, p being Point of TOP-REAL n, p9
being Point of Euclid n st p = p9 holds p in Cl A iff for r being Real
st r > 0 holds Ball (p9, r) meets A;
theorem :: KURATO_2:7
for x, y being Point of TOP-REAL n, x9 being Point of Euclid n st x9 =
x & x <> y ex r being Real st not y in Ball (x9, r);
theorem :: KURATO_2:8
for S being Subset of TOP-REAL n holds S is non bounded iff
for r being Real st r > 0
ex x, y being Point of Euclid n st x in S & y in S & dist (x, y) > r;
theorem :: KURATO_2:9
for a, b being Real, x, y being Point of Euclid n st Ball
(x, a) meets Ball (y, b) holds dist (x, y) < a + b;
theorem :: KURATO_2:10
for a, b, c being Real, x, y, z being Point of Euclid n
st Ball (x, a) meets Ball (z, c) & Ball (z, c) meets Ball (y, b) holds dist (x,
y) < a + b + 2*c;
theorem :: KURATO_2:11
for X, Y being non empty TopSpace, x being Point of X, y being
Point of Y, V being Subset of [: X, Y :] holds V is a_neighborhood of [: {x}, {
y} :] iff V is a_neighborhood of [ x, y ];
begin :: Subsequences
theorem :: KURATO_2:12
for T being non empty 1-sorted, F, G being SetSequence of the
carrier of T, A being Subset of T st G is subsequence of F & for i being Nat
holds F.i = A holds G = F;
theorem :: KURATO_2:13
for T being non empty 1-sorted, S being SetSequence of the carrier of
T, R being subsequence of S, n being Nat holds ex m being Element of
NAT st m >= n & R.n = S.m;
begin :: Lower Topological Limit
definition
let T be non empty TopSpace;
let S be SetSequence of the carrier of T;
func Lim_inf S -> Subset of T means
:: KURATO_2:def 1
for p being Point of T holds p
in it iff for G being a_neighborhood of p ex k being Nat st for m
being Nat st m > k holds S.m meets G;
end;
theorem :: KURATO_2:14
for S being SetSequence of the carrier of TOP-REAL n, p being
Point of TOP-REAL n, p9 being Point of Euclid n st p = p9 holds p in Lim_inf S
iff for r being Real st r > 0 ex k being Nat st for m being
Nat st m > k holds S.m meets Ball (p9, r);
theorem :: KURATO_2:15
for T being non empty TopSpace, S being SetSequence of the
carrier of T holds Cl Lim_inf S = Lim_inf S;
registration
let T be non empty TopSpace, S be SetSequence of the carrier of T;
cluster Lim_inf S -> closed;
end;
theorem :: KURATO_2:16
for T being non empty TopSpace, R, S being SetSequence of the carrier
of T st R is subsequence of S holds Lim_inf S c= Lim_inf R;
theorem :: KURATO_2:17
for T being non empty TopSpace, A, B being SetSequence of the
carrier of T st for i being Nat holds A.i c= B.i holds Lim_inf A c=
Lim_inf B;
theorem :: KURATO_2:18
for T being non empty TopSpace, A, B, C being SetSequence of the
carrier of T st for i being Nat holds C.i = A.i \/ B.i holds Lim_inf
A \/ Lim_inf B c= Lim_inf C;
theorem :: KURATO_2:19
for T being non empty TopSpace, A, B, C being SetSequence of the
carrier of T st for i being Nat holds C.i = A.i /\ B.i holds Lim_inf
C c= Lim_inf A /\ Lim_inf B;
theorem :: KURATO_2:20
for T being non empty TopSpace, F, G being SetSequence of the
carrier of T st for i being Nat holds G.i = Cl (F.i) holds Lim_inf G
= Lim_inf F;
theorem :: KURATO_2:21
for S being SetSequence of the carrier of TOP-REAL n, p being Point of
TOP-REAL n holds (ex s being Real_Sequence of n st s is convergent & (for x
being Nat holds s.x in S.x) & p = lim s) implies p in Lim_inf S;
theorem :: KURATO_2:22
for T being non empty TopSpace, P being Subset of T, s being
SetSequence of the carrier of T st (for i being Nat holds s.i c= P) holds
Lim_inf s c= Cl P;
theorem :: KURATO_2:23
for T being non empty TopSpace, F being SetSequence of the
carrier of T, A being Subset of T st for i being Nat holds F.i = A holds
Lim_inf F = Cl A;
theorem :: KURATO_2:24
for T being non empty TopSpace, F being SetSequence of the carrier of
T, A being closed Subset of T st for i being Nat holds F.i = A holds Lim_inf F
= A;
theorem :: KURATO_2:25
for S being SetSequence of the carrier of TOP-REAL n, P being
Subset of TOP-REAL n st P is bounded & (for i being Nat holds S.i c=
P) holds Lim_inf S is bounded;
theorem :: KURATO_2:26
for S being SetSequence of the carrier of TOP-REAL 2, P being Subset
of TOP-REAL 2 st P is bounded & (for i being Nat holds S.i c= P)
holds Lim_inf S is compact;
theorem :: KURATO_2:27
for A, B being SetSequence of the carrier of TOP-REAL n, C being
SetSequence of the carrier of [: TOP-REAL n, TOP-REAL n :] st for i being
Nat holds C.i = [:A.i, B.i:] holds [: Lim_inf A, Lim_inf B :] =
Lim_inf C;
theorem :: KURATO_2:28
for S being SetSequence of TOP-REAL 2 holds lim_inf S c= Lim_inf S;
theorem :: KURATO_2:29
for C being Simple_closed_curve, i being Nat holds Fr (UBD
L~Cage (C,i))` = L~Cage (C,i);
begin :: Upper Topological Limit
definition
let T be non empty TopSpace;
let S be SetSequence of the carrier of T;
func Lim_sup S -> Subset of T means
:: KURATO_2:def 2
for x being object holds x in it
iff ex A being subsequence of S st x in Lim_inf A;
end;
theorem :: KURATO_2:30
for N being Nat, F being sequence of TOP-REAL N, x being
Point of TOP-REAL N, x9 being Point of Euclid N st x = x9 holds
x is_a_cluster_point_of F iff for r being Real, n being Nat st
r > 0 holds ex m being Nat st n <= m & F.m in Ball (x9, r);
theorem :: KURATO_2:31
for T being non empty TopSpace, A being SetSequence of the
carrier of T holds Lim_inf A c= Lim_sup A;
theorem :: KURATO_2:32
for A, B, C being SetSequence of the carrier of TOP-REAL 2 st (
for i being Nat holds A.i c= B.i) & C is subsequence of A holds ex D
being subsequence of B st for i being Nat holds C.i c= D.i;
theorem :: KURATO_2:33
for A, B, C being SetSequence of the carrier of TOP-REAL 2 st (for i
being Nat holds A.i c= B.i) & C is subsequence of B holds ex D being
subsequence of A st for i being Nat holds D.i c= C.i;
theorem :: KURATO_2:34 :: (2)
for A, B being SetSequence of the carrier of TOP-REAL 2 st for i
being Nat holds A.i c= B.i holds Lim_sup A c= Lim_sup B;
theorem :: KURATO_2:35 :: (3)
for A, B, C being SetSequence of the carrier of TOP-REAL 2 st for i
being Nat holds C.i = A.i \/ B.i holds Lim_sup A \/ Lim_sup B c=
Lim_sup C;
theorem :: KURATO_2:36 :: (4)
for A, B, C being SetSequence of the carrier of TOP-REAL 2 st for i
being Nat holds C.i = A.i /\ B.i holds Lim_sup C c= Lim_sup A /\
Lim_sup B;
theorem :: KURATO_2:37
for A, B being SetSequence of the carrier of TOP-REAL 2, C, C1
being SetSequence of the carrier of [: TOP-REAL 2, TOP-REAL 2 :] st (for i
being Nat holds C.i = [: A.i, B.i :]) & C1 is subsequence of C holds
ex A1, B1 being SetSequence of the carrier of TOP-REAL 2 st A1 is subsequence
of A & B1 is subsequence of B & for i being Nat holds C1.i = [: A1.i
, B1.i :];
theorem :: KURATO_2:38
for A, B being SetSequence of the carrier of TOP-REAL 2, C being
SetSequence of the carrier of [: TOP-REAL 2, TOP-REAL 2 :] st for i being
Nat holds C.i = [: A.i, B.i :] holds Lim_sup C c= [: Lim_sup A,
Lim_sup B :];
::$N Kuratowski convergence
theorem :: KURATO_2:39
for T being non empty TopSpace, F being SetSequence of the
carrier of T, A being Subset of T st for i being Nat holds F.i = A holds
Lim_inf F = Lim_sup F;
theorem :: KURATO_2:40
for F being SetSequence of the carrier of TOP-REAL 2, A being Subset
of TOP-REAL 2 st for i being Nat holds F.i = A holds Lim_sup F = Cl A;
theorem :: KURATO_2:41
for F, G being SetSequence of the carrier of TOP-REAL 2 st for i being
Nat holds G.i = Cl (F.i) holds Lim_sup G = Lim_sup F;