:: On the {K}uratowski Limit Operators :: by Adam Grabowski :: :: Received August 12, 2003 :: Copyright (c) 2003-2016 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;