:: On the {K}uratowski Limit Operators :: by Adam Grabowski :: :: Received August 12, 2003 :: Copyright (c) 2003-2017 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; definitions XBOOLE_0, TARSKI, FRECHET, YELLOW_8; equalities XBOOLE_0, SUBSET_1, STRUCT_0, XCMPLX_0; expansions XBOOLE_0, TARSKI, FRECHET, YELLOW_8; theorems FRECHET, METRIC_1, TOPREAL3, TOPMETR, CONNSP_2, GOBOARD6, XBOOLE_1, PRE_TOPC, SUBSET_1, NAT_1, FUNCT_2, RELSET_1, TOPRNS_1, XBOOLE_0, FUNCT_1, INT_1, SPPOL_1, TOPS_1, TOPREAL6, JORDAN2C, TBSP_1, METRIC_6, ZFMISC_1, RELAT_1, GOBRD14, SEQM_3, MCART_1, BORSUK_1, FRECHET2, XREAL_1, XXREAL_0, ORDINAL1, VALUED_0, EUCLID, YELLOW_8, TOPS_2, KURATO_0, TARSKI; schemes XBOOLE_0, FUNCT_1, SUBSET_1; 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; coherence; end; theorem Th1: for x being Point of Euclid n, r being Real holds Ball (x , r) is open Subset of TOP-REAL n by TOPREAL3:8,GOBOARD6:3; theorem Th2: 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 proof let p be Point of Euclid n, x, p9 be Point of TOP-REAL n, r be Real; reconsider x9 = x as Point of Euclid n by TOPREAL3:8; assume that A1: p = p9 and A2: x in Ball (p, r); dist (x9, p) < r by A2,METRIC_1:11; hence thesis by A1,SPPOL_1:39; end; theorem Th3: 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) proof let p be Point of Euclid n, x, p9 be Point of TOP-REAL n, r be Real; reconsider x9 = x as Point of Euclid n by TOPREAL3:8; assume p = p9 & |. x - p9 .| < r; then dist (x9, p) < r by SPPOL_1:39; hence thesis by METRIC_1:11; end; theorem 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 proof let n be Nat, r be Point of TOP-REAL n, X be Subset of TOP-REAL n; reconsider r9 = r as Point of Euclid n by TOPREAL3:8; defpred P[object,object] means ex z being Nat st \$1 = z & \$2 = the Element of X /\ Ball (r9, 1/(z+1)); assume A1: r in Cl X; A2: now let x be object; assume x in NAT; then reconsider k = x as Nat; set n1 = k+1; set oi = Ball (r9, 1/n1); reconsider oi as open Subset of TOP-REAL n by Th1; reconsider u = the Element of X /\ oi as object; take u; dist (r9,r9) < 1/n1 by METRIC_1:1; then r in oi by METRIC_1:11; then X meets oi by A1,PRE_TOPC:24; then X /\ oi is non empty; then u in X /\ oi; hence u in the carrier of TOP-REAL n; thus P[x,u]; end; consider seq being Function such that A3: dom seq = NAT & rng seq c= the carrier of TOP-REAL n and A4: for x being object st x in NAT holds P[x,seq.x] from FUNCT_1:sch 6(A2); reconsider seq as Real_Sequence of n by A3,FUNCT_2:def 1,RELSET_1:4; take seq; thus rng seq c= X proof let y be object; assume y in rng seq; then consider x being object such that A5: x in dom seq and A6: seq.x = y by FUNCT_1:def 3; consider k being Nat such that x = k and A7: seq.x = the Element of X /\ Ball (r9,1/(k+1)) by A4,A5; set n1 = k+1; reconsider oi = Ball (r9,1/n1) as open Subset of TOP-REAL n by Th1; dist (r9,r9) < 1/n1 by METRIC_1:1; then r in oi by METRIC_1:11; then X meets oi by A1,PRE_TOPC:24; then X /\ oi is non empty; hence thesis by A6,A7,XBOOLE_0:def 4; end; A8: now let p be Real; set cp = [/ 1/p \]; A9: 1/p <= cp by INT_1:def 7; assume A10: 0 < p; then A11: 0 < cp by INT_1:def 7; then reconsider cp as Element of NAT by INT_1:3; reconsider cp as Nat; take k = cp; k < k+1 by NAT_1:13; then A12: 1/(k+1) < 1/k by A11,XREAL_1:88; 1/(1/p) >= 1/cp by A10,A9,XREAL_1:85; then A13: 1/(k+1) < p by A12,XXREAL_0:2; let m be Nat; assume k <= m; then A14: k+1 <= m+1 by XREAL_1:6; set m1 = m+1; 1/m1 <= 1/(k+1) by A14,XREAL_1:85; then A15: 1/m1 < p by A13,XXREAL_0:2; set oi = Ball (r9,1/m1); reconsider oi as open Subset of TOP-REAL n by Th1; dist (r9,r9) < 1/m1 by METRIC_1:1; then r in oi by METRIC_1:11; then X meets oi by A1,PRE_TOPC:24; then A16: X /\ oi is non empty; m in NAT by ORDINAL1:def 12; then ex m9 being Nat st m9 = m & seq.m = the Element of X /\ Ball (r9,1 /(m9+1)) by A4; then seq.m in oi by A16,XBOOLE_0:def 4; hence |. seq.m - r .| < p by A15,Th2,XXREAL_0:2; end; hence seq is convergent by TOPRNS_1:def 8; hence thesis by A8,TOPRNS_1:def 9; end; registration let M be non empty MetrSpace; cluster TopSpaceMetr M -> first-countable; coherence by FRECHET:20; end; Lm1: for T being non empty TopSpace, x being Point of T, y being Point of the TopStruct of T, A being set st x = y holds A is Basis of x iff A is Basis of y proof let T be non empty TopSpace, x be Point of T, y be Point of the TopStruct of T, A being set such that A1: x = y; thus A is Basis of x implies A is Basis of y proof assume A2: A is Basis of x; then reconsider A as Subset-Family of the TopStruct of T; A is Basis of y proof A c= the topology of the TopStruct of T by A2,TOPS_2:64; then A3: A is open by TOPS_2:64; A is y-quasi_basis by A1,A2,YELLOW_8:def 1,PRE_TOPC:30; hence thesis by A3; end; hence thesis; end; assume A4: A is Basis of y; then reconsider A as Subset-Family of T; A is Basis of x proof A c= the topology of T by A4,TOPS_2:64; then A5: A is open by TOPS_2:64; A is x-quasi_basis by A1,A4,YELLOW_8:def 1,PRE_TOPC:30; hence thesis by A5; end; hence thesis; end; theorem Th5: for T being non empty TopSpace holds T is first-countable iff the TopStruct of T is first-countable proof let T be non empty TopSpace; thus T is first-countable implies the TopStruct of T is first-countable proof assume A1: T is first-countable; let x be Point of the TopStruct of T; reconsider y = x as Point of T; consider C being Basis of y such that A2: C is countable by A1; reconsider B = C as Basis of x by Lm1; take B; thus B is countable by A2; end; assume A3: the TopStruct of T is first-countable; let x be Point of T; reconsider y = x as Point of the TopStruct of T; consider C being Basis of y such that A4: C is countable by A3; reconsider B = C as Basis of x by Lm1; take B; thus B is countable by A4; end; registration let n be Nat; cluster TOP-REAL n -> first-countable; coherence proof the TopStruct of TOP-REAL n = TopSpaceMetr Euclid n by EUCLID:def 8; hence thesis by Th5; end; end; theorem 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 proof let A be Subset of TOP-REAL n, p be Point of TOP-REAL n, p9 be Point of Euclid n; assume A1: p = p9; hereby assume A2: p in Cl A; let r be Real; reconsider B = Ball (p9, r) as Subset of TOP-REAL n by TOPREAL3:8; assume r > 0; then B is a_neighborhood of p by A1,GOBOARD6:2; hence Ball (p9, r) meets A by A2,CONNSP_2:27; end; assume A3: for r being Real st r > 0 holds Ball (p9, r) meets A; for G being a_neighborhood of p holds G meets A proof let G be a_neighborhood of p; p in Int G by CONNSP_2:def 1; then ex r being Real st r > 0 & Ball (p9, r) c= G by A1,GOBOARD6:5; hence thesis by A3,XBOOLE_1:63; end; hence thesis by CONNSP_2:27; end; theorem 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) proof let x, y be Point of TOP-REAL n, x9 be Point of Euclid n; reconsider y9 = y as Point of Euclid n by TOPREAL3:8; reconsider r = dist (x9, y9)/2 as Real; assume x9 = x & x <> y; then A1: dist (x9, y9) <> 0 by METRIC_1:2; take r; dist (x9, y9) >= 0 by METRIC_1:5; then dist (x9, y9) > r by A1,XREAL_1:216; hence thesis by METRIC_1:11; end; theorem Th8: 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 proof let S be Subset of TOP-REAL n; reconsider S9 = S as Subset of Euclid n by TOPREAL3:8; hereby assume S is non bounded; then S9 is non bounded by JORDAN2C:11; hence 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 by TBSP_1:def 7; end; assume A1: 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; S is non bounded proof assume S is bounded; then S is bounded Subset of Euclid n by JORDAN2C:11; hence thesis by A1,TBSP_1:def 7; end; hence thesis; end; theorem Th9: 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 proof let a, b be Real, x, y be Point of Euclid n; assume Ball (x, a) meets Ball (y, b); then consider z being object such that A1: z in Ball (x, a) and A2: z in Ball (y, b) by XBOOLE_0:3; reconsider z as Point of Euclid n by A1; dist (y, z) < b by A2,METRIC_1:11; then A3: dist (x, z) + dist (y, z) < dist (x, z) + b by XREAL_1:8; A4: dist (x, z) + dist (y, z) >= dist (x, y) by METRIC_1:4; dist (x, z) < a by A1,METRIC_1:11; then dist (x, z) + b < a + b by XREAL_1:8; then dist (x, z) + dist (y, z) < a + b by A3,XXREAL_0:2; hence thesis by A4,XXREAL_0:2; end; theorem Th10: 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 proof let a, b, c be Real, x, y, z be Point of Euclid n; assume Ball (x, a) meets Ball (z, c) & Ball (z, c) meets Ball (y, b); then dist (x, z) + dist (z, y) < (a + c) + dist (z, y) & (a + c) + dist (z, y ) < (a + c) + (c + b) by Th9,XREAL_1:8; then A1: dist (x, z) + dist (z, y) < (a + c) + (c + b) by XXREAL_0:2; dist (x, y) <= dist (x, z) + dist (z, y) by METRIC_1:4; hence thesis by A1,XXREAL_0:2; end; theorem Th11: 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 ] proof let X, Y be non empty TopSpace, x be Point of X, y be Point of Y, V be Subset of [: X, Y :]; hereby assume V is a_neighborhood of [: {x}, {y} :]; then V is a_neighborhood of { [x, y] } by ZFMISC_1:29; hence V is a_neighborhood of [ x, y ] by CONNSP_2:8; end; assume V is a_neighborhood of [ x, y ]; then V is a_neighborhood of { [ x, y ] } by CONNSP_2:8; hence thesis by ZFMISC_1:29; end; begin :: Subsequences theorem Th12: 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 proof let T be non empty 1-sorted, F, G be SetSequence of the carrier of T, A be Subset of T; assume that A1: G is subsequence of F and A2: for i being Nat holds F.i = A; consider NS being increasing sequence of NAT such that A3: G = F * NS by A1,VALUED_0:def 17; for i being Nat holds G.i = F.i proof let i be Nat; reconsider i as Element of NAT by ORDINAL1:def 12; dom NS = NAT by FUNCT_2:def 1; then G.i = F.(NS.i) by A3,FUNCT_1:13 .= A by A2 .= F.i by A2; hence thesis; end; then A4: for x being object st x in dom F holds F.x = G.x; NAT = dom G & NAT = dom F by FUNCT_2:def 1; hence thesis by A4,FUNCT_1:2; end; theorem 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 proof let T being non empty 1-sorted, S being SetSequence of the carrier of T, R being subsequence of S, n being Nat; consider NS being increasing sequence of NAT such that A1: R = S * NS by VALUED_0:def 17; reconsider m = NS.n as Element of NAT; take m; thus m >= n by SEQM_3:14; n in NAT by ORDINAL1:def 12; then n in dom NS by FUNCT_2:def 1; hence thesis by A1,FUNCT_1:13; end; 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 :Def1: 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; existence proof defpred P[Point of T] means for G being a_neighborhood of \$1 ex k being Nat st for m being Nat st m > k holds S.m meets G; thus ex IT being Subset of T st for p being Point of T holds p in IT iff P [p] from SUBSET_1:sch 3; end; uniqueness proof defpred P[Point of T] means for G being a_neighborhood of \$1 ex k being Nat st for m being Nat st m > k holds S.m meets G; let a,b be Subset of T such that A1: for p being Point of T holds p in a iff P[p] and A2: for p being Point of T holds p in b iff P[p]; thus a=b from SUBSET_1:sch 2(A1,A2); end; end; theorem Th14: 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) proof let S be SetSequence of the carrier of TOP-REAL n, p be Point of TOP-REAL n, p9 be Point of Euclid n; assume A1: p = p9; hereby assume A2: p in Lim_inf S; let r be Real; assume r > 0; then reconsider G = Ball (p9, r) as a_neighborhood of p by A1,GOBOARD6:2; ex k being Nat st for m being Nat st m > k holds S.m meets G by A2,Def1; hence ex k being Nat st for m being Nat st m > k holds S.m meets Ball (p9, r); end; assume A3: 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); now let G be a_neighborhood of p; A4: the TopStruct of TOP-REAL n = TopSpaceMetr Euclid n by EUCLID:def 8; then reconsider G9 = Int G as Subset of TopSpaceMetr Euclid n; A5: p9 in G9 by A1,CONNSP_2:def 1; G9 is open by A4,PRE_TOPC:30; then consider r being Real such that A6: r > 0 and A7: Ball (p9, r) c= G9 by A5,TOPMETR:15; consider k being Nat such that A8: for m being Nat st m > k holds S.m meets Ball (p9, r) by A3,A6; take k; let m be Nat; assume m > k; then G9 c= G & S.m meets Ball (p9, r) by A8,TOPS_1:16; hence S.m meets G by A7,XBOOLE_1:1,63; end; hence thesis by Def1; end; theorem Th15: for T being non empty TopSpace, S being SetSequence of the carrier of T holds Cl Lim_inf S = Lim_inf S proof let T be non empty TopSpace; let S be SetSequence of the carrier of T; thus Cl Lim_inf S c= Lim_inf S proof let x be object; assume A1: x in Cl Lim_inf S; then reconsider x9 = x as Point of T; now let G be a_neighborhood of x9; set H = Int G; x9 in H by CONNSP_2:def 1; then Lim_inf S meets H by A1,PRE_TOPC:24; then consider z being object such that A2: z in Lim_inf S and A3: z in H by XBOOLE_0:3; reconsider z as Point of T by A2; z in Int H by A3; then H is a_neighborhood of z by CONNSP_2:def 1; then consider k being Nat such that A4: for m being Nat st m > k holds S.m meets H by A2,Def1; take k; let m be Nat; assume m > k; then S.m meets H by A4; hence S.m meets G by TOPS_1:16,XBOOLE_1:63; end; hence thesis by Def1; end; thus thesis by PRE_TOPC:18; end; registration let T be non empty TopSpace, S be SetSequence of the carrier of T; cluster Lim_inf S -> closed; coherence proof Lim_inf S = Cl Lim_inf S by Th15; hence thesis; end; end; theorem 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 proof let T be non empty TopSpace, R, S be SetSequence of the carrier of T; assume R is subsequence of S; then consider Nseq being increasing sequence of NAT such that A1: R = S * Nseq by VALUED_0:def 17; let x be object; assume A2: x in Lim_inf S; then reconsider p = x as Point of T; for G being a_neighborhood of p ex k being Nat st for m being Nat st m > k holds R.m meets G proof let G be a_neighborhood of p; consider k being Nat such that A3: for m being Nat st m > k holds S.m meets G by A2,Def1; take k; let m1 be Nat; A4: m1 in NAT by ORDINAL1:def 12; A5: m1 <= Nseq.m1 by SEQM_3:14; assume m1 > k; then A6: Nseq.m1 > k by A5,XXREAL_0:2; dom Nseq = NAT by FUNCT_2:def 1; then R.m1 = S.(Nseq.m1) by A1,FUNCT_1:13,A4; hence thesis by A3,A6; end; hence thesis by Def1; end; theorem Th17: 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 proof let T be non empty TopSpace, A, B be SetSequence of the carrier of T; assume A1: for i being Nat holds A.i c= B.i; let x be object; assume A2: x in Lim_inf A; then reconsider p = x as Point of T; for G being a_neighborhood of p ex k being Nat st for m being Nat st m > k holds B.m meets G proof let G be a_neighborhood of p; consider k being Nat such that A3: for m being Nat st m > k holds A.m meets G by A2,Def1; take k; let m1 be Nat; assume m1 > k; then A.m1 meets G by A3; hence thesis by A1,XBOOLE_1:63; end; hence thesis by Def1; end; theorem 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 proof let T be non empty TopSpace, A, B, C be SetSequence of the carrier of T; assume A1: for i being Nat holds C.i = A.i \/ B.i; let x be object; assume A2: x in Lim_inf A \/ Lim_inf B; then reconsider p = x as Point of T; per cases by A2,XBOOLE_0:def 3; suppose A3: x in Lim_inf A; for H being a_neighborhood of p ex k being Nat st for m being Nat st m > k holds C.m meets H proof let H be a_neighborhood of p; consider k being Nat such that A4: for m being Nat st m > k holds A.m meets H by A3,Def1; take k; let m be Nat; assume m > k; then A5: A.m meets H by A4; C.m = A.m \/ B.m by A1; hence thesis by A5,XBOOLE_1:7,63; end; hence thesis by Def1; end; suppose A6: x in Lim_inf B; for H being a_neighborhood of p ex k being Nat st for m being Nat st m > k holds C.m meets H proof let H be a_neighborhood of p; consider k being Nat such that A7: for m being Nat st m > k holds B.m meets H by A6,Def1; take k; let m be Nat; assume m > k; then A8: B.m meets H by A7; C.m = A.m \/ B.m by A1; hence thesis by A8,XBOOLE_1:7,63; end; hence thesis by Def1; end; end; theorem 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 proof let T be non empty TopSpace, A, B, C be SetSequence of the carrier of T; assume A1: for i being Nat holds C.i = A.i /\ B.i; let x be object; assume A2: x in Lim_inf C; then reconsider p = x as Point of T; for H being a_neighborhood of p ex k being Nat st for m being Nat st m > k holds B.m meets H proof let H be a_neighborhood of p; consider k being Nat such that A3: for m being Nat st m > k holds C.m meets H by A2,Def1; take k; let m be Nat; assume m > k; then A4: C.m meets H by A3; C.m = A.m /\ B.m by A1; hence thesis by A4,XBOOLE_1:17,63; end; then A5: x in Lim_inf B by Def1; for H being a_neighborhood of p ex k being Nat st for m being Nat st m > k holds A.m meets H proof let H be a_neighborhood of p; consider k being Nat such that A6: for m being Nat st m > k holds C.m meets H by A2,Def1; take k; let m be Nat; assume m > k; then A7: C.m meets H by A6; C.m = A.m /\ B.m by A1; hence thesis by A7,XBOOLE_1:17,63; end; then x in Lim_inf A by Def1; hence thesis by A5,XBOOLE_0:def 4; end; theorem Th20: 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 proof let T be non empty TopSpace, F, G be SetSequence of the carrier of T; assume A1: for i being Nat holds G.i = Cl (F.i); thus Lim_inf G c= Lim_inf F proof let x be object; assume A2: x in Lim_inf G; then reconsider p = x as Point of T; for H being a_neighborhood of p ex k being Nat st for m being Nat st m > k holds F.m meets H proof let H be a_neighborhood of p; consider H1 being non empty Subset of T such that A3: H1 is a_neighborhood of p and A4: H1 is open and A5: H1 c= H by CONNSP_2:5; consider k being Nat such that A6: for m being Nat st m > k holds G.m meets H1 by A2,A3,Def1; take k; let m be Nat; assume m > k; then G.m meets H1 by A6; then consider y being object such that A7: y in G.m and A8: y in H1 by XBOOLE_0:3; reconsider y as Point of T by A7; H1 is a_neighborhood of y by A4,A8,CONNSP_2:3; then consider H9 being non empty Subset of T such that A9: H9 is a_neighborhood of y and H9 is open and A10: H9 c= H1 by CONNSP_2:5; y in Cl (F.m) by A1,A7; then H9 meets F.m by A9,CONNSP_2:27; then H1 meets F.m by A10,XBOOLE_1:63; hence thesis by A5,XBOOLE_1:63; end; hence thesis by Def1; end; for i being Nat holds F.i c= G.i proof let i be Nat; G.i = Cl (F.i) by A1; hence thesis by PRE_TOPC:18; end; hence Lim_inf F c= Lim_inf G by Th17; end; theorem 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 proof let S be SetSequence of the carrier of TOP-REAL n, p be Point of TOP-REAL n; reconsider p9 = p as Point of Euclid n by TOPREAL3:8; given s being Real_Sequence of n such that A1: s is convergent and A2: for x being Nat holds s.x in S.x and A3: p = lim s; 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) proof let r be Real; reconsider r9 = r as Real; assume r > 0; then consider l being Nat such that A4: for m being Nat st l <= m holds |. s.m - p .| < r9 by A1,A3, TOPRNS_1:def 9; reconsider v = max (0, l) as Nat by TARSKI:1; take v; let m be Nat; assume v < m; then l <= m by XXREAL_0:30; then |. s.m - p .| < r9 by A4; then A5: s.m in Ball (p9, r) by Th3; s.m in S.m by A2; hence thesis by A5,XBOOLE_0:3; end; hence thesis by Th14; end; theorem Th22: 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 proof let T be non empty TopSpace, P be Subset of T, s be SetSequence of the carrier of T; assume A1: for i being Nat holds s.i c= P; let x be object; assume A2: x in Lim_inf s; then reconsider p = x as Point of T; for G being Subset of T st G is open holds p in G implies P meets G proof let G be Subset of T; assume A3: G is open; assume p in G; then reconsider G9 = G as a_neighborhood of p by A3,CONNSP_2:3; consider k being Nat such that A4: for m being Nat st m > k holds s.m meets G9 by A2,Def1; set m = k + 1; m > k by NAT_1:13; then s.m meets G9 by A4; hence thesis by A1,XBOOLE_1:63; end; hence thesis by PRE_TOPC:def 7; end; theorem Th23: 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 proof let T be non empty TopSpace, F be SetSequence of the carrier of T, A be Subset of T; assume A1: for i being Nat holds F.i = A; then for i being Nat holds F.i c= A; hence Lim_inf F c= Cl A by Th22; thus Cl A c= Lim_inf F proof let x be object; assume A2: x in Cl A; then reconsider p = x as Point of T; for G being a_neighborhood of p ex k being Nat st for m being Nat st m > k holds F.m meets G proof let G being a_neighborhood of p; take k = 1; let m be Nat; assume m > k; F.m = A by A1; hence thesis by A2,CONNSP_2:27; end; hence thesis by Def1; end; end; theorem 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 proof let T be non empty TopSpace, F be SetSequence of the carrier of T, A be closed Subset of T; assume for i being Nat holds F.i = A; then Lim_inf F = Cl A by Th23; hence thesis by PRE_TOPC:22; end; theorem Th25: 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 proof let S be SetSequence of the carrier of TOP-REAL n; let P be Subset of TOP-REAL n; assume that A1: P is bounded and A2: for i being Nat holds S.i c= P; reconsider P9= P as bounded Subset of Euclid n by A1,JORDAN2C:11; consider t being Real, z being Point of Euclid n such that A3: 0 < t and A4: P9 c= Ball (z,t) by METRIC_6:def 3; set r = 1, R = r + r + 3*t; assume Lim_inf S is non bounded; then consider x, y being Point of Euclid n such that A5: x in Lim_inf S and A6: y in Lim_inf S and A7: dist (x, y) > R by A3,Th8; consider k1 being Nat such that A8: for m being Nat st m > k1 holds S.m meets Ball (x, r) by A5,Th14; consider k2 being Nat such that A9: for m being Nat st m > k2 holds S.m meets Ball (y, r) by A6,Th14; set k = max (k1, k2) + 1; S.k c= P9 by A2; then A10: S.k c= Ball (z,t) by A4; 2*t < 3*t by A3,XREAL_1:68; then A11: r + r + 2*t < r + r + 3*t by XREAL_1:8; max (k1,k2) >= k2 by XXREAL_0:25; then k > k2 by NAT_1:13; then A12: Ball (z,t) meets Ball (y, r) by A9,A10,XBOOLE_1:63; max (k1,k2) >= k1 by XXREAL_0:25; then k > k1 by NAT_1:13; then Ball (z,t) meets Ball (x, r) by A8,A10,XBOOLE_1:63; hence thesis by A7,A12,A11,Th10,XXREAL_0:2; end; theorem 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 by Th25,TOPREAL6:79; theorem Th27: 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 proof let A, B be SetSequence of the carrier of TOP-REAL n, C be SetSequence of the carrier of [: TOP-REAL n, TOP-REAL n :]; assume A1: for i being Nat holds C.i = [:A.i, B.i:]; thus [: Lim_inf A, Lim_inf B :] c= Lim_inf C proof let x be object; assume A2: x in [: Lim_inf A, Lim_inf B :]; then consider x1, x2 being object such that A3: x1 in Lim_inf A and A4: x2 in Lim_inf B and A5: x = [x1,x2] by ZFMISC_1:def 2; reconsider p = x as Point of [: TOP-REAL n, TOP-REAL n :] by A2; reconsider x1, x2 as Point of TOP-REAL n by A3,A4; for G being a_neighborhood of p ex k being Nat st for m being Nat st m > k holds C.m meets G proof let G be a_neighborhood of p; G is a_neighborhood of [:{x1},{x2}:] by A5,Th11; then consider V being a_neighborhood of {x1}, W being a_neighborhood of x2 such that A6: [:V,W:] c= G by BORSUK_1:25; consider k2 being Nat such that A7: for m being Nat st m > k2 holds B.m meets W by A4,Def1; V is a_neighborhood of x1 by CONNSP_2:8; then consider k1 being Nat such that A8: for m being Nat st m > k1 holds A.m meets V by A3,Def1; reconsider k = max (k1, k2) as Nat by TARSKI:1; take k; let m be Nat; assume A9: m > k; k >= k2 by XXREAL_0:25; then m > k2 by A9,XXREAL_0:2; then A10: B.m meets W by A7; k >= k1 by XXREAL_0:25; then m > k1 by A9,XXREAL_0:2; then A.m meets V by A8; then [: A.m, B.m :] meets [: V, W :] by A10,KURATO_0:2; then C.m meets [: V, W :] by A1; hence thesis by A6,XBOOLE_1:63; end; hence thesis by Def1; end; thus Lim_inf C c= [: Lim_inf A, Lim_inf B :] proof let x be object; assume A11: x in Lim_inf C; then x in the carrier of [: TOP-REAL n, TOP-REAL n :]; then A12: x in [: the carrier of TOP-REAL n, the carrier of TOP-REAL n :] by BORSUK_1:def 2; then reconsider p1 = x`1, p2 = x`2 as Point of TOP-REAL n by MCART_1:10; set H = the a_neighborhood of p2; set F = the a_neighborhood of p1; A13: x = [p1,p2] by A12,MCART_1:21; for G being a_neighborhood of p2 ex k being Nat st for m being Nat st m > k holds B.m meets G proof let G be a_neighborhood of p2; consider k being Nat such that A14: for m being Nat st m > k holds C.m meets [: F, G :] by A11,A13,Def1; take k; let m be Nat; assume m > k; then C.m meets [: F, G :] by A14; then consider y being object such that A15: y in C.m and A16: y in [: F, G :] by XBOOLE_0:3; y in [:A.m, B.m:] by A1,A15; then A17: y`2 in B.m by MCART_1:10; y`2 in G by A16,MCART_1:10; hence thesis by A17,XBOOLE_0:3; end; then A18: p2 in Lim_inf B by Def1; for G being a_neighborhood of p1 ex k being Nat st for m being Nat st m > k holds A.m meets G proof let G be a_neighborhood of p1; consider k being Nat such that A19: for m being Nat st m > k holds C.m meets [: G, H :] by A11,A13,Def1; take k; let m be Nat; assume m > k; then C.m meets [: G, H :] by A19; then consider y being object such that A20: y in C.m and A21: y in [: G, H :] by XBOOLE_0:3; y in [:A.m, B.m:] by A1,A20; then A22: y`1 in A.m by MCART_1:10; y`1 in G by A21,MCART_1:10; hence thesis by A22,XBOOLE_0:3; end; then p1 in Lim_inf A by Def1; hence thesis by A13,A18,ZFMISC_1:87; end; end; theorem for S being SetSequence of TOP-REAL 2 holds lim_inf S c= Lim_inf S proof let S be SetSequence of TOP-REAL 2; let x be object; assume A1: x in lim_inf S; then reconsider p = x as Point of Euclid 2 by TOPREAL3:8; reconsider y = x as Point of TOP-REAL 2 by A1; consider k being Nat such that A2: for n being Nat holds x in S.(k+n) by A1,KURATO_0:4; for r being Real st r > 0 ex k being Nat st for m being Nat st m > k holds S.m meets Ball (p, r) proof let r be Real; assume r > 0; then A3: x in Ball (p, r) by GOBOARD6:1; reconsider k as Nat; take k; let m be Nat; assume m > k; then consider h being Nat such that A4: m = k + h by NAT_1:10; x in S.m by A2,A4; hence thesis by A3,XBOOLE_0:3; end; then y in Lim_inf S by Th14; hence thesis; end; theorem for C being Simple_closed_curve, i being Nat holds Fr (UBD L~Cage (C,i))` = L~Cage (C,i) proof let C be Simple_closed_curve, i be Nat; set K = (UBD L~Cage (C,i))`; set R = L~Cage (C,i); A1: (BDD R) \/ (BDD R)` = [#] TOP-REAL 2 by PRE_TOPC:2; UBD R c= R` by JORDAN2C:26; then A2: UBD R misses R by SUBSET_1:23; UBD R misses BDD R by JORDAN2C:24; then A3: UBD R misses (BDD R) \/ R by A2,XBOOLE_1:70; [#] TOP-REAL 2 = R` \/ R by PRE_TOPC:2 .= (BDD R) \/ (UBD R) \/ R by JORDAN2C:27; then A4: K = ((UBD R) \/ ((BDD R) \/ R)) \ UBD R by XBOOLE_1:4 .= R \/ BDD R by A3,XBOOLE_1:88; ((BDD R) \/ (UBD R))` = R`` by JORDAN2C:27; then (BDD R)` /\ (UBD R)` = R by XBOOLE_1:53; then (BDD R) \/ R = ((BDD R) \/ (BDD R)`) /\ ((BDD R) \/ K) by XBOOLE_1:24 .= (BDD R) \/ K by A1,XBOOLE_1:28 .= K by A4,XBOOLE_1:7,12; then A5: Cl K = (BDD L~Cage (C,i)) \/ L~Cage (C,i) by PRE_TOPC:22; A6: K` = LeftComp Cage (C,i) by GOBRD14:36; BDD L~Cage (C,i) misses UBD L~Cage (C,i) by JORDAN2C:24; then A7: (BDD L~Cage (C,i)) /\ (UBD L~Cage (C,i)) = {}; Fr K = Cl K /\ Cl K` by TOPS_1:def 2 .= ((BDD L~Cage (C,i)) \/ L~Cage (C,i)) /\ ((UBD L~Cage (C,i)) \/ L~Cage (C,i)) by A5,A6,GOBRD14:22 .= ((BDD L~Cage (C,i)) /\ (UBD L~Cage (C,i))) \/ L~Cage (C,i) by XBOOLE_1:24 .= L~Cage (C,i) by A7; hence thesis; end; 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 :Def2: for x being object holds x in it iff ex A being subsequence of S st x in Lim_inf A; existence proof defpred P[object] means ex A being subsequence of S st \$1 in Lim_inf A; consider X being set such that A1: for x being object holds x in X iff x in the carrier of T & P[x] from XBOOLE_0:sch 1; X c= the carrier of T by A1; then reconsider X as Subset of T; take X; thus thesis by A1; end; uniqueness proof defpred P[object] means ex A being subsequence of S st \$1 in Lim_inf A; let A1, A2 be Subset of T; assume that A2: for x being object holds x in A1 iff P[x] and A3: for x being object holds x in A2 iff P[x]; A1 = A2 from XBOOLE_0:sch 2(A2, A3); hence thesis; end; end; theorem 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) proof let N be Nat, F be sequence of TOP-REAL N, x be Point of TOP-REAL N, x9 be Point of Euclid N; assume A1: x = x9; hereby assume A2: x is_a_cluster_point_of F; let r be Real, n be Nat; reconsider O = Ball (x9, r) as open Subset of TOP-REAL N by Th1; assume r > 0; then x in O by A1,GOBOARD6:1; then consider m being Element of NAT such that A3: n <= m & F.m in O by A2,FRECHET2:def 3; reconsider m as Nat; take m; thus n <= m & F.m in Ball (x9, r) by A3; end; assume A4: for r being Real, n being Nat st r > 0 holds ex m being Nat st n <= m & F.m in Ball (x9, r); for O being Subset of TOP-REAL N, n being Nat st O is open & x in O ex m being Element of NAT st n <= m & F.m in O proof let O be Subset of TOP-REAL N, n be Nat; assume that A5: O is open and A6: x in O; reconsider n9=n as Nat; A7: the TopStruct of TOP-REAL N = TopSpaceMetr Euclid N by EUCLID:def 8; then reconsider G9 = O as Subset of TopSpaceMetr Euclid N; G9 is open by A5,A7,PRE_TOPC:30; then consider r being Real such that A8: r > 0 and A9: Ball (x9, r) c= G9 by A1,A6,TOPMETR:15; consider m being Nat such that A10: n9 <= m & F.m in Ball (x9, r) by A4,A8; reconsider m as Element of NAT by ORDINAL1:def 12; take m; thus thesis by A9,A10; end; hence thesis by FRECHET2:def 3; end; theorem Th31: for T being non empty TopSpace, A being SetSequence of the carrier of T holds Lim_inf A c= Lim_sup A proof let T be non empty TopSpace, A be SetSequence of the carrier of T; let x be object; assume A1: x in Lim_inf A; ex K being subsequence of A st x in Lim_inf K proof reconsider B = A as subsequence of A by VALUED_0:19; take B; thus thesis by A1; end; hence thesis by Def2; end; theorem Th32: 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 proof let A, B, C be SetSequence of the carrier of TOP-REAL 2; assume that A1: for i being Nat holds A.i c= B.i and A2: C is subsequence of A; consider NS being increasing sequence of NAT such that A3: C = A * NS by A2,VALUED_0:def 17; set D = B * NS; reconsider D as SetSequence of TOP-REAL 2; reconsider D as subsequence of B; take D; for i being Nat holds C.i c= D.i proof let i be Nat; A4: dom NS = NAT by FUNCT_2:def 1; C.i c= D.i proof let x be object; A5: i in NAT by ORDINAL1:def 12; assume x in C.i; then A6: x in A.(NS.i) by A3,A4,FUNCT_1:13,A5; A.(NS.i) c= B.(NS.i) by A1; then x in B.(NS.i) by A6; hence thesis by A4,FUNCT_1:13,A5; end; hence thesis; end; hence thesis; end; theorem 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 proof let A, B, C be SetSequence of the carrier of TOP-REAL 2; assume that A1: for i being Nat holds A.i c= B.i and A2: C is subsequence of B; consider NS being increasing sequence of NAT such that A3: C = B * NS by A2,VALUED_0:def 17; set D = A * NS; reconsider D as SetSequence of TOP-REAL 2; reconsider D as subsequence of A; take D; for i being Nat holds D.i c= C.i proof let i be Nat; A4: dom NS = NAT by FUNCT_2:def 1; D.i c= C.i proof let x be object; A5: i in NAT by ORDINAL1:def 12; assume x in D.i; then A6: x in A.(NS.i) by A4,FUNCT_1:13,A5; A.(NS.i) c= B.(NS.i) by A1; then x in B.(NS.i) by A6; hence thesis by A3,A4,FUNCT_1:13,A5; end; hence thesis; end; hence thesis; end; theorem Th34: :: (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 proof let A, B be SetSequence of the carrier of TOP-REAL 2; assume A1: for i being Nat holds A.i c= B.i; Lim_sup A c= Lim_sup B proof let x be object; assume x in Lim_sup A; then consider A1 being subsequence of A such that A2: x in Lim_inf A1 by Def2; consider D being subsequence of B such that A3: for i being Nat holds A1.i c= D.i by A1,Th32; Lim_inf A1 c= Lim_inf D by A3,Th17; hence thesis by A2,Def2; end; hence thesis; end; theorem :: (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 proof let A, B, C be SetSequence of the carrier of TOP-REAL 2; assume A1: for i being Nat holds C.i = A.i \/ B.i; A2: for i being Nat holds B.i c= C.i proof let i be Nat; C.i = A.i \/ B.i by A1; hence thesis by XBOOLE_1:7; end; A3: for i being Nat holds A.i c= C.i proof let i be Nat; C.i = A.i \/ B.i by A1; hence thesis by XBOOLE_1:7; end; thus Lim_sup A \/ Lim_sup B c= Lim_sup C proof let x be object; assume A4: x in Lim_sup A \/ Lim_sup B; per cases by A4,XBOOLE_0:def 3; suppose x in Lim_sup A; then consider A1 being subsequence of A such that A5: x in Lim_inf A1 by Def2; consider C1 being subsequence of C such that A6: for i being Nat holds A1.i c= C1.i by A3,Th32; Lim_inf A1 c= Lim_inf C1 by A6,Th17; hence thesis by A5,Def2; end; suppose x in Lim_sup B; then consider B1 being subsequence of B such that A7: x in Lim_inf B1 by Def2; consider C1 being subsequence of C such that A8: for i being Nat holds B1.i c= C1.i by A2,Th32; Lim_inf B1 c= Lim_inf C1 by A8,Th17; hence thesis by A7,Def2; end; end; end; theorem :: (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 proof let A, B, C be SetSequence of the carrier of TOP-REAL 2; assume A1: for i being Nat holds C.i = A.i /\ B.i; let x be object; assume x in Lim_sup C; then consider C1 being subsequence of C such that A2: x in Lim_inf C1 by Def2; for i being Nat holds C.i c= B.i proof let i be Nat; C.i = A.i /\ B.i by A1; hence thesis by XBOOLE_1:17; end; then consider E1 being subsequence of B such that A3: for i being Nat holds C1.i c= E1.i by Th32; Lim_inf C1 c= Lim_inf E1 by A3,Th17; then A4: x in Lim_sup B by A2,Def2; for i being Nat holds C.i c= A.i proof let i be Nat; C.i = A.i /\ B.i by A1; hence thesis by XBOOLE_1:17; end; then consider D1 being subsequence of A such that A5: for i being Nat holds C1.i c= D1.i by Th32; Lim_inf C1 c= Lim_inf D1 by A5,Th17; then x in Lim_sup A by A2,Def2; hence thesis by A4,XBOOLE_0:def 4; end; theorem Th37: 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 :] proof let A, B be SetSequence of the carrier of TOP-REAL 2, C, C1 be SetSequence of the carrier of [: TOP-REAL 2, TOP-REAL 2 :]; assume that A1: for i being Nat holds C.i = [: A.i, B.i :] and A2: C1 is subsequence of C; consider NS being increasing sequence of NAT such that A3: C1 = C * NS by A2,VALUED_0:def 17; set B1 = B * NS; set A1 = A * NS; reconsider A1 as SetSequence of TOP-REAL 2; reconsider B1 as SetSequence of TOP-REAL 2; take A1, B1; for i being Nat holds C1.i = [: A1.i, B1.i :] proof let i be Nat; A4: i in NAT by ORDINAL1:def 12; A5: dom NS = NAT by FUNCT_2:def 1; then A6: A1.i = A.(NS.i) & B1.i = B.(NS.i) by FUNCT_1:13,A4; C1.i = C.(NS.i) by A3,A5,FUNCT_1:13,A4 .= [: A1.i, B1.i :] by A1,A6; hence thesis; end; hence thesis; end; theorem 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 :] proof let A, B be SetSequence of the carrier of TOP-REAL 2, C be SetSequence of the carrier of [: TOP-REAL 2, TOP-REAL 2 :]; assume A1: for i being Nat holds C.i = [: A.i, B.i :]; let x be object; assume x in Lim_sup C; then consider C1 being subsequence of C such that A2: x in Lim_inf C1 by Def2; x in the carrier of [: TOP-REAL 2, TOP-REAL 2 :] by A2; then x in [: the carrier of TOP-REAL 2, the carrier of TOP-REAL 2 :] by BORSUK_1:def 2; then consider x1, x2 being object such that A3: x = [x1, x2] by RELAT_1:def 1; consider A1, B1 being SetSequence of the carrier of TOP-REAL 2 such that A4: A1 is subsequence of A and A5: B1 is subsequence of B and A6: for i being Nat holds C1.i = [: A1.i, B1.i :] by A1,Th37; A7: x in [: Lim_inf A1, Lim_inf B1 :] by A2,A6,Th27; then x2 in Lim_inf B1 by A3,ZFMISC_1:87; then A8: x2 in Lim_sup B by A5,Def2; x1 in Lim_inf A1 by A3,A7,ZFMISC_1:87; then x1 in Lim_sup A by A4,Def2; hence thesis by A3,A8,ZFMISC_1:87; end; ::\$N Kuratowski convergence theorem Th39: 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 proof let T be non empty TopSpace, F be SetSequence of the carrier of T, A be Subset of T; assume A1: for i being Nat holds F.i = A; thus Lim_inf F c= Lim_sup F by Th31; thus Lim_sup F c= Lim_inf F proof let x be object; assume x in Lim_sup F; then ex G being subsequence of F st x in Lim_inf G by Def2; hence thesis by A1,Th12; end; end; theorem 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 proof let F be SetSequence of the carrier of TOP-REAL 2, A be Subset of TOP-REAL 2; assume A1: for i being Nat holds F.i = A; then Lim_inf F = Lim_sup F by Th39; hence thesis by A1,Th23; end; theorem 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 proof let F, G be SetSequence of the carrier of TOP-REAL 2; assume A1: for i being Nat holds G.i = Cl (F.i); thus Lim_sup G c= Lim_sup F proof let x be object; assume x in Lim_sup G; then consider H being subsequence of G such that A2: x in Lim_inf H by Def2; consider NS being increasing sequence of NAT such that A3: H = G * NS by VALUED_0:def 17; set P = F * NS; reconsider P as SetSequence of TOP-REAL 2; reconsider P as subsequence of F; for i being Nat holds H.i = Cl (P.i) proof let i be Nat; A4: i in NAT by ORDINAL1:def 12; A5: dom NS = NAT by FUNCT_2:def 1; then H.i = G.(NS.i) by A3,FUNCT_1:13,A4 .= Cl (F.(NS.i)) by A1 .= Cl (P.i) by A5,FUNCT_1:13,A4; hence thesis; end; then Lim_inf H = Lim_inf P by Th20; hence thesis by A2,Def2; end; for i being Nat holds F.i c= G.i proof let i be Nat; G.i = Cl (F.i) by A1; hence thesis by PRE_TOPC:18; end; hence thesis by Th34; end;