:: KURATO_2 semantic presentation begin definition let T be 1-sorted ; mode SetSequence of T is SetSequence of the carrier of T; end; begin registration let f be FinSequence of the carrier of (TOP-REAL 2); cluster L~ f -> closed ; coherence L~ f is closed ; end; theorem Th1: :: KURATO_2:1 for n being Element of NAT for x being Point of (Euclid n) for r being real number holds Ball (x,r) is open Subset of (TOP-REAL n) proof let n be Element of NAT ; ::_thesis: for x being Point of (Euclid n) for r being real number holds Ball (x,r) is open Subset of (TOP-REAL n) let x be Point of (Euclid n); ::_thesis: for r being real number holds Ball (x,r) is open Subset of (TOP-REAL n) let r be real number ; ::_thesis: Ball (x,r) is open Subset of (TOP-REAL n) reconsider A = Ball (x,r) as Subset of (TOP-REAL n) by TOPREAL3:8; reconsider A = A as Subset of (TOP-REAL n) ; r is Real by XREAL_0:def_1; then A is open by GOBOARD6:3; hence Ball (x,r) is open Subset of (TOP-REAL n) ; ::_thesis: verum end; theorem Th2: :: KURATO_2:2 for n being Element of NAT for p being Point of (Euclid n) for x, p9 being Point of (TOP-REAL n) for r being real number st p = p9 & x in Ball (p,r) holds |.(x - p9).| < r proof let n be Element of NAT ; ::_thesis: for p being Point of (Euclid n) for x, p9 being Point of (TOP-REAL n) for r being real number st p = p9 & x in Ball (p,r) holds |.(x - p9).| < r let p be Point of (Euclid n); ::_thesis: for x, p9 being Point of (TOP-REAL n) for r being real number st p = p9 & x in Ball (p,r) holds |.(x - p9).| < r let x, p9 be Point of (TOP-REAL n); ::_thesis: for r being real number st p = p9 & x in Ball (p,r) holds |.(x - p9).| < r let r be real number ; ::_thesis: ( p = p9 & x in Ball (p,r) implies |.(x - p9).| < r ) reconsider x9 = x as Point of (Euclid n) by TOPREAL3:8; assume that A1: p = p9 and A2: x in Ball (p,r) ; ::_thesis: |.(x - p9).| < r dist (x9,p) < r by A2, METRIC_1:11; hence |.(x - p9).| < r by A1, SPPOL_1:39; ::_thesis: verum end; theorem Th3: :: KURATO_2:3 for n being Element of NAT for p being Point of (Euclid n) for x, p9 being Point of (TOP-REAL n) for r being real number st p = p9 & |.(x - p9).| < r holds x in Ball (p,r) proof let n be Element of NAT ; ::_thesis: for p being Point of (Euclid n) for x, p9 being Point of (TOP-REAL n) for r being real number st p = p9 & |.(x - p9).| < r holds x in Ball (p,r) let p be Point of (Euclid n); ::_thesis: for x, p9 being Point of (TOP-REAL n) for r being real number st p = p9 & |.(x - p9).| < r holds x in Ball (p,r) let x, p9 be Point of (TOP-REAL n); ::_thesis: for r being real number st p = p9 & |.(x - p9).| < r holds x in Ball (p,r) let r be real number ; ::_thesis: ( p = p9 & |.(x - p9).| < r implies x in Ball (p,r) ) reconsider x9 = x as Point of (Euclid n) by TOPREAL3:8; assume ( p = p9 & |.(x - p9).| < r ) ; ::_thesis: x in Ball (p,r) then dist (x9,p) < r by SPPOL_1:39; hence x in Ball (p,r) by METRIC_1:11; ::_thesis: verum end; theorem :: KURATO_2:4 for n being Element of NAT for r being Point of (TOP-REAL n) for 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 Element of NAT ; ::_thesis: for r being Point of (TOP-REAL n) for 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 ) let r be Point of (TOP-REAL n); ::_thesis: for 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 ) let X be Subset of (TOP-REAL n); ::_thesis: ( r in Cl X implies ex seq being Real_Sequence of n st ( rng seq c= X & seq is convergent & lim seq = r ) ) reconsider r9 = r as Point of (Euclid n) by TOPREAL3:8; defpred S1[ set , set ] means ex z being Element of NAT st ( \$1 = z & \$2 = choose (X /\ (Ball (r9,(1 / (z + 1))))) ); assume A1: r in Cl X ; ::_thesis: ex seq being Real_Sequence of n st ( rng seq c= X & seq is convergent & lim seq = r ) A2: now__::_thesis:_for_x_being_set_st_x_in_NAT_holds_ ex_u_being_set_st_ (_u_in_the_carrier_of_(TOP-REAL_n)_&_S1[x,u]_) let x be set ; ::_thesis: ( x in NAT implies ex u being set st ( u in the carrier of (TOP-REAL n) & S1[x,u] ) ) assume x in NAT ; ::_thesis: ex u being set st ( u in the carrier of (TOP-REAL n) & S1[x,u] ) then reconsider k = x as Element of NAT ; set n1 = k + 1; set oi = Ball (r9,(1 / (k + 1))); reconsider oi = Ball (r9,(1 / (k + 1))) as open Subset of (TOP-REAL n) by Th1; reconsider u = choose (X /\ oi) as set ; take u = u; ::_thesis: ( u in the carrier of (TOP-REAL n) & S1[x,u] ) dist (r9,r9) < 1 / (k + 1) by METRIC_1:1; then r in oi by METRIC_1:11; then X meets oi by A1, PRE_TOPC:24; then not X /\ oi is empty by XBOOLE_0:def_7; then u in X /\ oi ; hence u in the carrier of (TOP-REAL n) ; ::_thesis: S1[x,u] thus S1[x,u] ; ::_thesis: verum 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 set st x in NAT holds S1[x,seq . x] from FUNCT_1:sch_5(A2); reconsider seq = seq as Real_Sequence of n by A3, FUNCT_2:def_1, RELSET_1:4; take seq ; ::_thesis: ( rng seq c= X & seq is convergent & lim seq = r ) thus rng seq c= X ::_thesis: ( seq is convergent & lim seq = r ) proof let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng seq or y in X ) assume y in rng seq ; ::_thesis: y in X then consider x being set such that A5: x in dom seq and A6: seq . x = y by FUNCT_1:def_3; consider k being Element of NAT such that x = k and A7: seq . x = choose (X /\ (Ball (r9,(1 / (k + 1))))) by A4, A5; set n1 = k + 1; reconsider oi = Ball (r9,(1 / (k + 1))) as open Subset of (TOP-REAL n) by Th1; dist (r9,r9) < 1 / (k + 1) by METRIC_1:1; then r in oi by METRIC_1:11; then X meets oi by A1, PRE_TOPC:24; then not X /\ oi is empty by XBOOLE_0:def_7; hence y in X by A6, A7, XBOOLE_0:def_4; ::_thesis: verum end; A8: now__::_thesis:_for_p_being_Real_st_0_<_p_holds_ ex_k_being_Element_of_NAT_st_ for_m_being_Element_of_NAT_st_k_<=_m_holds_ |.((seq_._m)_-_r).|_<_p let p be Real; ::_thesis: ( 0 < p implies ex k being Element of NAT st for m being Element of NAT st k <= m holds |.((seq . m) - r).| < p ) set cp = [/(1 / p)\]; A9: 1 / p <= [/(1 / p)\] by INT_1:def_7; assume A10: 0 < p ; ::_thesis: ex k being Element of NAT st for m being Element of NAT st k <= m holds |.((seq . m) - r).| < p then A11: 0 < [/(1 / p)\] by INT_1:def_7; then reconsider cp = [/(1 / p)\] as Element of NAT by INT_1:3; take k = cp; ::_thesis: for m being Element of NAT st k <= m holds |.((seq . m) - r).| < p 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 Element of NAT ; ::_thesis: ( k <= m implies |.((seq . m) - r).| < p ) assume k <= m ; ::_thesis: |.((seq . m) - r).| < p then A14: k + 1 <= m + 1 by XREAL_1:6; set m1 = m + 1; 1 / (m + 1) <= 1 / (k + 1) by A14, XREAL_1:85; then A15: 1 / (m + 1) < p by A13, XXREAL_0:2; set oi = Ball (r9,(1 / (m + 1))); reconsider oi = Ball (r9,(1 / (m + 1))) as open Subset of (TOP-REAL n) by Th1; dist (r9,r9) < 1 / (m + 1) by METRIC_1:1; then r in oi by METRIC_1:11; then X meets oi by A1, PRE_TOPC:24; then A16: not X /\ oi is empty by XBOOLE_0:def_7; ex m9 being Element of NAT st ( m9 = m & seq . m = choose (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; ::_thesis: verum end; hence seq is convergent by TOPRNS_1:def_8; ::_thesis: lim seq = r hence lim seq = r by A8, TOPRNS_1:def_9; ::_thesis: verum end; registration let M be non empty MetrSpace; cluster TopSpaceMetr M -> first-countable ; coherence TopSpaceMetr M is first-countable by FRECHET:20; end; Lm1: for T being non empty TopSpace for x being Point of T for y being Point of TopStruct(# the carrier of T, the topology of T #) for A being set st x = y holds ( A is Basis of iff A is Basis of ) proof let T be non empty TopSpace; ::_thesis: for x being Point of T for y being Point of TopStruct(# the carrier of T, the topology of T #) for A being set st x = y holds ( A is Basis of iff A is Basis of ) let x be Point of T; ::_thesis: for y being Point of TopStruct(# the carrier of T, the topology of T #) for A being set st x = y holds ( A is Basis of iff A is Basis of ) let y be Point of TopStruct(# the carrier of T, the topology of T #); ::_thesis: for A being set st x = y holds ( A is Basis of iff A is Basis of ) let A be set ; ::_thesis: ( x = y implies ( A is Basis of iff A is Basis of ) ) assume A1: x = y ; ::_thesis: ( A is Basis of iff A is Basis of ) thus ( A is Basis of implies A is Basis of ) ::_thesis: ( A is Basis of implies A is Basis of ) proof assume A2: A is Basis of ; ::_thesis: A is Basis of then reconsider A = A as Subset-Family of TopStruct(# the carrier of T, the topology of T #) ; A is Basis of proof A c= the topology of TopStruct(# the carrier of T, the topology of T #) by A2, TOPS_2:64; then A3: A is open by TOPS_2:64; A is y -quasi_basis proof thus y in Intersect A by A1, A2, YELLOW_8:def_1; :: according to YELLOW_8:def_1 ::_thesis: for b1 being Element of bool the carrier of TopStruct(# the carrier of T, the topology of T #) holds ( not b1 is open or not y in b1 or ex b2 being Element of bool the carrier of TopStruct(# the carrier of T, the topology of T #) st ( b2 in A & b2 c= b1 ) ) let S be Subset of TopStruct(# the carrier of T, the topology of T #); ::_thesis: ( not S is open or not y in S or ex b1 being Element of bool the carrier of TopStruct(# the carrier of T, the topology of T #) st ( b1 in A & b1 c= S ) ) reconsider SS = S as Subset of T ; assume that A4: S is open and A5: y in S ; ::_thesis: ex b1 being Element of bool the carrier of TopStruct(# the carrier of T, the topology of T #) st ( b1 in A & b1 c= S ) SS is open by A4, PRE_TOPC:30; then consider W being Subset of T such that A6: ( W in A & W c= SS ) by A1, A2, A5, YELLOW_8:def_1; reconsider V = W as Subset of TopStruct(# the carrier of T, the topology of T #) ; take V ; ::_thesis: ( V in A & V c= S ) thus ( V in A & V c= S ) by A6; ::_thesis: verum end; hence A is Basis of by A3; ::_thesis: verum end; hence A is Basis of ; ::_thesis: verum end; assume A7: A is Basis of ; ::_thesis: A is Basis of then reconsider A = A as Subset-Family of T ; A is Basis of proof A c= the topology of T by A7, TOPS_2:64; then A8: A is open by TOPS_2:64; A is x -quasi_basis proof thus x in Intersect A by A1, A7, YELLOW_8:def_1; :: according to YELLOW_8:def_1 ::_thesis: for b1 being Element of bool the carrier of T holds ( not b1 is open or not x in b1 or ex b2 being Element of bool the carrier of T st ( b2 in A & b2 c= b1 ) ) let S be Subset of T; ::_thesis: ( not S is open or not x in S or ex b1 being Element of bool the carrier of T st ( b1 in A & b1 c= S ) ) reconsider SS = S as Subset of TopStruct(# the carrier of T, the topology of T #) ; assume that A9: S is open and A10: x in S ; ::_thesis: ex b1 being Element of bool the carrier of T st ( b1 in A & b1 c= S ) SS is open by A9, PRE_TOPC:30; then consider W being Subset of TopStruct(# the carrier of T, the topology of T #) such that A11: ( W in A & W c= SS ) by A1, A7, A10, YELLOW_8:def_1; reconsider V = W as Subset of T ; take V ; ::_thesis: ( V in A & V c= S ) thus ( V in A & V c= S ) by A11; ::_thesis: verum end; hence A is Basis of by A8; ::_thesis: verum end; hence A is Basis of ; ::_thesis: verum end; theorem Th5: :: KURATO_2:5 for T being non empty TopSpace holds ( T is first-countable iff TopStruct(# the carrier of T, the topology of T #) is first-countable ) proof let T be non empty TopSpace; ::_thesis: ( T is first-countable iff TopStruct(# the carrier of T, the topology of T #) is first-countable ) thus ( T is first-countable implies TopStruct(# the carrier of T, the topology of T #) is first-countable ) ::_thesis: ( TopStruct(# the carrier of T, the topology of T #) is first-countable implies T is first-countable ) proof assume A1: T is first-countable ; ::_thesis: TopStruct(# the carrier of T, the topology of T #) is first-countable let x be Point of TopStruct(# the carrier of T, the topology of T #); :: according to FRECHET:def_2 ::_thesis: ex b1 being Element of bool (bool the carrier of TopStruct(# the carrier of T, the topology of T #)) st b1 is countable reconsider y = x as Point of T ; consider C being Basis of such that A2: C is countable by A1, FRECHET:def_2; reconsider B = C as Basis of by Lm1; take B ; ::_thesis: B is countable thus B is countable by A2; ::_thesis: verum end; assume A3: TopStruct(# the carrier of T, the topology of T #) is first-countable ; ::_thesis: T is first-countable let x be Point of T; :: according to FRECHET:def_2 ::_thesis: ex b1 being Element of bool (bool the carrier of T) st b1 is countable reconsider y = x as Point of TopStruct(# the carrier of T, the topology of T #) ; consider C being Basis of such that A4: C is countable by A3, FRECHET:def_2; reconsider B = C as Basis of by Lm1; take B ; ::_thesis: B is countable thus B is countable by A4; ::_thesis: verum end; registration let n be Element of NAT ; cluster TOP-REAL n -> first-countable ; coherence TOP-REAL n is first-countable proof TopStruct(# the carrier of (TOP-REAL n), the topology of (TOP-REAL n) #) = TopSpaceMetr (Euclid n) by EUCLID:def_8; hence TOP-REAL n is first-countable by Th5; ::_thesis: verum end; end; theorem :: KURATO_2:6 for n being Element of NAT for A being Subset of (TOP-REAL n) for p being Point of (TOP-REAL n) for p9 being Point of (Euclid n) st p = p9 holds ( p in Cl A iff for r being real number st r > 0 holds Ball (p9,r) meets A ) proof let n be Element of NAT ; ::_thesis: for A being Subset of (TOP-REAL n) for p being Point of (TOP-REAL n) for p9 being Point of (Euclid n) st p = p9 holds ( p in Cl A iff for r being real number st r > 0 holds Ball (p9,r) meets A ) let A be Subset of (TOP-REAL n); ::_thesis: for p being Point of (TOP-REAL n) for p9 being Point of (Euclid n) st p = p9 holds ( p in Cl A iff for r being real number st r > 0 holds Ball (p9,r) meets A ) let p be Point of (TOP-REAL n); ::_thesis: for p9 being Point of (Euclid n) st p = p9 holds ( p in Cl A iff for r being real number st r > 0 holds Ball (p9,r) meets A ) let p9 be Point of (Euclid n); ::_thesis: ( p = p9 implies ( p in Cl A iff for r being real number st r > 0 holds Ball (p9,r) meets A ) ) assume A1: p = p9 ; ::_thesis: ( p in Cl A iff for r being real number st r > 0 holds Ball (p9,r) meets A ) hereby ::_thesis: ( ( for r being real number st r > 0 holds Ball (p9,r) meets A ) implies p in Cl A ) assume A2: p in Cl A ; ::_thesis: for r being real number st r > 0 holds Ball (p9,r) meets A let r be real number ; ::_thesis: ( r > 0 implies Ball (p9,r) meets A ) reconsider B = Ball (p9,r) as Subset of (TOP-REAL n) by TOPREAL3:8; assume r > 0 ; ::_thesis: Ball (p9,r) meets A then B is a_neighborhood of p by A1, GOBOARD6:2; hence Ball (p9,r) meets A by A2, CONNSP_2:27; ::_thesis: verum end; assume A3: for r being real number st r > 0 holds Ball (p9,r) meets A ; ::_thesis: p in Cl A for G being a_neighborhood of p holds G meets A proof let G be a_neighborhood of p; ::_thesis: G meets A p in Int G by CONNSP_2:def_1; then ex r being real number st ( r > 0 & Ball (p9,r) c= G ) by A1, GOBOARD6:5; hence G meets A by A3, XBOOLE_1:63; ::_thesis: verum end; hence p in Cl A by CONNSP_2:27; ::_thesis: verum end; theorem :: KURATO_2:7 for n being Element of NAT for x, y being Point of (TOP-REAL n) for x9 being Point of (Euclid n) st x9 = x & x <> y holds ex r being Real st not y in Ball (x9,r) proof let n be Element of NAT ; ::_thesis: for x, y being Point of (TOP-REAL n) for x9 being Point of (Euclid n) st x9 = x & x <> y holds ex r being Real st not y in Ball (x9,r) let x, y be Point of (TOP-REAL n); ::_thesis: for x9 being Point of (Euclid n) st x9 = x & x <> y holds ex r being Real st not y in Ball (x9,r) let x9 be Point of (Euclid n); ::_thesis: ( x9 = x & x <> y implies ex r being Real st not y in Ball (x9,r) ) reconsider y9 = y as Point of (Euclid n) by TOPREAL3:8; reconsider r = (dist (x9,y9)) / 2 as Real ; assume ( x9 = x & x <> y ) ; ::_thesis: not for r being Real holds y in Ball (x9,r) then A1: dist (x9,y9) <> 0 by METRIC_1:2; take r ; ::_thesis: not y in Ball (x9,r) dist (x9,y9) >= 0 by METRIC_1:5; then dist (x9,y9) > r by A1, XREAL_1:216; hence not y in Ball (x9,r) by METRIC_1:11; ::_thesis: verum end; theorem Th8: :: KURATO_2:8 for n being Element of NAT for S being Subset of (TOP-REAL n) holds ( not S is bounded iff for r being Real st r > 0 holds ex x, y being Point of (Euclid n) st ( x in S & y in S & dist (x,y) > r ) ) proof let n be Element of NAT ; ::_thesis: for S being Subset of (TOP-REAL n) holds ( not S is bounded iff for r being Real st r > 0 holds ex x, y being Point of (Euclid n) st ( x in S & y in S & dist (x,y) > r ) ) let S be Subset of (TOP-REAL n); ::_thesis: ( not S is bounded iff for r being Real st r > 0 holds ex x, y being Point of (Euclid n) st ( x in S & y in S & dist (x,y) > r ) ) reconsider S9 = S as Subset of (Euclid n) by TOPREAL3:8; hereby ::_thesis: ( ( for r being Real st r > 0 holds ex x, y being Point of (Euclid n) st ( x in S & y in S & dist (x,y) > r ) ) implies not S is bounded ) assume not S is bounded ; ::_thesis: for r being Real st r > 0 holds ex x, y being Point of (Euclid n) st ( x in S & y in S & dist (x,y) > r ) then not S9 is bounded by JORDAN2C:11; hence for r being Real st r > 0 holds ex x, y being Point of (Euclid n) st ( x in S & y in S & dist (x,y) > r ) by TBSP_1:def_7; ::_thesis: verum end; assume A1: for r being Real st r > 0 holds ex x, y being Point of (Euclid n) st ( x in S & y in S & dist (x,y) > r ) ; ::_thesis: not S is bounded not S is bounded proof assume S is bounded ; ::_thesis: contradiction then S is bounded Subset of (Euclid n) by JORDAN2C:11; hence contradiction by A1, TBSP_1:def_7; ::_thesis: verum end; hence not S is bounded ; ::_thesis: verum end; theorem Th9: :: KURATO_2:9 for n being Element of NAT for a, b being real number for x, y being Point of (Euclid n) st Ball (x,a) meets Ball (y,b) holds dist (x,y) < a + b proof let n be Element of NAT ; ::_thesis: for a, b being real number for x, y being Point of (Euclid n) st Ball (x,a) meets Ball (y,b) holds dist (x,y) < a + b let a, b be real number ; ::_thesis: for x, y being Point of (Euclid n) st Ball (x,a) meets Ball (y,b) holds dist (x,y) < a + b let x, y be Point of (Euclid n); ::_thesis: ( Ball (x,a) meets Ball (y,b) implies dist (x,y) < a + b ) assume Ball (x,a) meets Ball (y,b) ; ::_thesis: dist (x,y) < a + b then consider z being set such that A1: z in Ball (x,a) and A2: z in Ball (y,b) by XBOOLE_0:3; reconsider z = 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 dist (x,y) < a + b by A4, XXREAL_0:2; ::_thesis: verum end; theorem Th10: :: KURATO_2:10 for n being Element of NAT for a, b, c being real number for 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 n be Element of NAT ; ::_thesis: for a, b, c being real number for 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) let a, b, c be real number ; ::_thesis: for 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) let x, y, z be Point of (Euclid n); ::_thesis: ( Ball (x,a) meets Ball (z,c) & Ball (z,c) meets Ball (y,b) implies dist (x,y) < (a + b) + (2 * c) ) assume ( Ball (x,a) meets Ball (z,c) & Ball (z,c) meets Ball (y,b) ) ; ::_thesis: dist (x,y) < (a + b) + (2 * c) 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 dist (x,y) < (a + b) + (2 * c) by A1, XXREAL_0:2; ::_thesis: verum end; theorem Th11: :: KURATO_2:11 for X, Y being non empty TopSpace for x being Point of X for y being Point of Y for 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; ::_thesis: for x being Point of X for y being Point of Y for V being Subset of [:X,Y:] holds ( V is a_neighborhood of [:{x},{y}:] iff V is a_neighborhood of [x,y] ) let x be Point of X; ::_thesis: for y being Point of Y for V being Subset of [:X,Y:] holds ( V is a_neighborhood of [:{x},{y}:] iff V is a_neighborhood of [x,y] ) let y be Point of Y; ::_thesis: for V being Subset of [:X,Y:] holds ( V is a_neighborhood of [:{x},{y}:] iff V is a_neighborhood of [x,y] ) let V be Subset of [:X,Y:]; ::_thesis: ( V is a_neighborhood of [:{x},{y}:] iff V is a_neighborhood of [x,y] ) hereby ::_thesis: ( V is a_neighborhood of [x,y] implies V is a_neighborhood of [:{x},{y}:] ) assume V is a_neighborhood of [:{x},{y}:] ; ::_thesis: 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; ::_thesis: verum end; assume V is a_neighborhood of [x,y] ; ::_thesis: V is a_neighborhood of [:{x},{y}:] then V is a_neighborhood of {[x,y]} by CONNSP_2:8; hence V is a_neighborhood of [:{x},{y}:] by ZFMISC_1:29; ::_thesis: verum end; begin theorem Th12: :: KURATO_2:12 for T being non empty 1-sorted for F, G being SetSequence of the carrier of T for 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 ; ::_thesis: for F, G being SetSequence of the carrier of T for A being Subset of T st G is subsequence of F & ( for i being Nat holds F . i = A ) holds G = F let F, G be SetSequence of the carrier of T; ::_thesis: for A being Subset of T st G is subsequence of F & ( for i being Nat holds F . i = A ) holds G = F let A be Subset of T; ::_thesis: ( G is subsequence of F & ( for i being Nat holds F . i = A ) implies G = F ) assume that A1: G is subsequence of F and A2: for i being Nat holds F . i = A ; ::_thesis: G = F consider NS being increasing sequence of NAT such that A3: G = F * NS by A1, VALUED_0:def_17; for i being Element of NAT holds G . i = F . i proof let i be Element of NAT ; ::_thesis: G . i = F . i 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 G . i = F . i ; ::_thesis: verum end; then A4: for x being set st x in dom F holds F . x = G . x ; ( NAT = dom G & NAT = dom F ) by FUNCT_2:def_1; hence G = F by A4, FUNCT_1:2; ::_thesis: verum end; theorem :: KURATO_2:13 for T being non empty 1-sorted for S being SetSequence of the carrier of T for R being subsequence of S for n being Element of NAT ex m being Element of NAT st ( m >= n & R . n = S . m ) proof let T be non empty 1-sorted ; ::_thesis: for S being SetSequence of the carrier of T for R being subsequence of S for n being Element of NAT ex m being Element of NAT st ( m >= n & R . n = S . m ) let S be SetSequence of the carrier of T; ::_thesis: for R being subsequence of S for n being Element of NAT ex m being Element of NAT st ( m >= n & R . n = S . m ) let R be subsequence of S; ::_thesis: for n being Element of NAT ex m being Element of NAT st ( m >= n & R . n = S . m ) let n be Element of NAT ; ::_thesis: ex m being Element of NAT st ( m >= n & R . n = S . m ) consider NS being increasing sequence of NAT such that A1: R = S * NS by VALUED_0:def_17; take m = NS . n; ::_thesis: ( m >= n & R . n = S . m ) thus m >= n by SEQM_3:14; ::_thesis: R . n = S . m n in NAT ; then n in dom NS by FUNCT_2:def_1; hence R . n = S . m by A1, FUNCT_1:13; ::_thesis: verum end; begin 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: :: 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 Element of NAT st for m being Element of NAT st m > k holds S . m meets G ); existence ex b1 being Subset of T st for p being Point of T holds ( p in b1 iff for G being a_neighborhood of p ex k being Element of NAT st for m being Element of NAT st m > k holds S . m meets G ) proof defpred S1[ Point of T] means for G being a_neighborhood of \$1 ex k being Element of NAT st for m being Element of 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 S1[p] ) from SUBSET_1:sch_3(); ::_thesis: verum end; uniqueness for b1, b2 being Subset of T st ( for p being Point of T holds ( p in b1 iff for G being a_neighborhood of p ex k being Element of NAT st for m being Element of NAT st m > k holds S . m meets G ) ) & ( for p being Point of T holds ( p in b2 iff for G being a_neighborhood of p ex k being Element of NAT st for m being Element of NAT st m > k holds S . m meets G ) ) holds b1 = b2 proof defpred S1[ Point of T] means for G being a_neighborhood of \$1 ex k being Element of NAT st for m being Element of NAT st m > k holds S . m meets G; let a, b be Subset of T; ::_thesis: ( ( for p being Point of T holds ( p in a iff for G being a_neighborhood of p ex k being Element of NAT st for m being Element of NAT st m > k holds S . m meets G ) ) & ( for p being Point of T holds ( p in b iff for G being a_neighborhood of p ex k being Element of NAT st for m being Element of NAT st m > k holds S . m meets G ) ) implies a = b ) assume that A1: for p being Point of T holds ( p in a iff S1[p] ) and A2: for p being Point of T holds ( p in b iff S1[p] ) ; ::_thesis: a = b thus a = b from SUBSET_1:sch_2(A1, A2); ::_thesis: verum end; end; :: deftheorem Def1 defines Lim_inf KURATO_2:def_1_:_ for T being non empty TopSpace for S being SetSequence of the carrier of T for b3 being Subset of T holds ( b3 = Lim_inf S iff for p being Point of T holds ( p in b3 iff for G being a_neighborhood of p ex k being Element of NAT st for m being Element of NAT st m > k holds S . m meets G ) ); theorem Th14: :: KURATO_2:14 for n being Element of NAT for S being SetSequence of the carrier of (TOP-REAL n) for p being Point of (TOP-REAL n) for p9 being Point of (Euclid n) st p = p9 holds ( p in Lim_inf S iff for r being real number st r > 0 holds ex k being Element of NAT st for m being Element of NAT st m > k holds S . m meets Ball (p9,r) ) proof let n be Element of NAT ; ::_thesis: for S being SetSequence of the carrier of (TOP-REAL n) for p being Point of (TOP-REAL n) for p9 being Point of (Euclid n) st p = p9 holds ( p in Lim_inf S iff for r being real number st r > 0 holds ex k being Element of NAT st for m being Element of NAT st m > k holds S . m meets Ball (p9,r) ) let S be SetSequence of the carrier of (TOP-REAL n); ::_thesis: for p being Point of (TOP-REAL n) for p9 being Point of (Euclid n) st p = p9 holds ( p in Lim_inf S iff for r being real number st r > 0 holds ex k being Element of NAT st for m being Element of NAT st m > k holds S . m meets Ball (p9,r) ) let p be Point of (TOP-REAL n); ::_thesis: for p9 being Point of (Euclid n) st p = p9 holds ( p in Lim_inf S iff for r being real number st r > 0 holds ex k being Element of NAT st for m being Element of NAT st m > k holds S . m meets Ball (p9,r) ) let p9 be Point of (Euclid n); ::_thesis: ( p = p9 implies ( p in Lim_inf S iff for r being real number st r > 0 holds ex k being Element of NAT st for m being Element of NAT st m > k holds S . m meets Ball (p9,r) ) ) assume A1: p = p9 ; ::_thesis: ( p in Lim_inf S iff for r being real number st r > 0 holds ex k being Element of NAT st for m being Element of NAT st m > k holds S . m meets Ball (p9,r) ) hereby ::_thesis: ( ( for r being real number st r > 0 holds ex k being Element of NAT st for m being Element of NAT st m > k holds S . m meets Ball (p9,r) ) implies p in Lim_inf S ) assume A2: p in Lim_inf S ; ::_thesis: for r being real number st r > 0 holds ex k being Element of NAT st for m being Element of NAT st m > k holds S . m meets Ball (p9,r) let r be real number ; ::_thesis: ( r > 0 implies ex k being Element of NAT st for m being Element of NAT st m > k holds S . m meets Ball (p9,r) ) assume r > 0 ; ::_thesis: ex k being Element of NAT st for m being Element of NAT st m > k holds S . m meets Ball (p9,r) then reconsider G = Ball (p9,r) as a_neighborhood of p by A1, GOBOARD6:2; ex k being Element of NAT st for m being Element of NAT st m > k holds S . m meets G by A2, Def1; hence ex k being Element of NAT st for m being Element of NAT st m > k holds S . m meets Ball (p9,r) ; ::_thesis: verum end; assume A3: for r being real number st r > 0 holds ex k being Element of NAT st for m being Element of NAT st m > k holds S . m meets Ball (p9,r) ; ::_thesis: p in Lim_inf S now__::_thesis:_for_G_being_a_neighborhood_of_p_ex_k_being_Element_of_NAT_st_ for_m_being_Element_of_NAT_st_m_>_k_holds_ S_._m_meets_G let G be a_neighborhood of p; ::_thesis: ex k being Element of NAT st for m being Element of NAT st m > k holds S . m meets G A4: TopStruct(# the carrier of (TOP-REAL n), the topology 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 number such that A6: r > 0 and A7: Ball (p9,r) c= G9 by A5, TOPMETR:15; consider k being Element of NAT such that A8: for m being Element of NAT st m > k holds S . m meets Ball (p9,r) by A3, A6; take k = k; ::_thesis: for m being Element of NAT st m > k holds S . m meets G let m be Element of NAT ; ::_thesis: ( m > k implies S . m meets G ) assume m > k ; ::_thesis: S . m meets G 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, XBOOLE_1:63; ::_thesis: verum end; hence p in Lim_inf S by Def1; ::_thesis: verum end; theorem Th15: :: KURATO_2:15 for T being non empty TopSpace for S being SetSequence of the carrier of T holds Cl (Lim_inf S) = Lim_inf S proof let T be non empty TopSpace; ::_thesis: for S being SetSequence of the carrier of T holds Cl (Lim_inf S) = Lim_inf S let S be SetSequence of the carrier of T; ::_thesis: Cl (Lim_inf S) = Lim_inf S thus Cl (Lim_inf S) c= Lim_inf S :: according to XBOOLE_0:def_10 ::_thesis: Lim_inf S c= Cl (Lim_inf S) proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Cl (Lim_inf S) or x in Lim_inf S ) assume A1: x in Cl (Lim_inf S) ; ::_thesis: x in Lim_inf S then reconsider x9 = x as Point of T ; now__::_thesis:_for_G_being_a_neighborhood_of_x9_ex_k_being_Element_of_NAT_st_ for_m_being_Element_of_NAT_st_m_>_k_holds_ S_._m_meets_G let G be a_neighborhood of x9; ::_thesis: ex k being Element of NAT st for m being Element of NAT st m > k holds S . m meets G set H = Int G; x9 in Int G by CONNSP_2:def_1; then Lim_inf S meets Int G by A1, PRE_TOPC:24; then consider z being set such that A2: z in Lim_inf S and A3: z in Int G by XBOOLE_0:3; reconsider z = z as Point of T by A2; z in Int (Int G) by A3; then Int G is a_neighborhood of z by CONNSP_2:def_1; then consider k being Element of NAT such that A4: for m being Element of NAT st m > k holds S . m meets Int G by A2, Def1; take k = k; ::_thesis: for m being Element of NAT st m > k holds S . m meets G let m be Element of NAT ; ::_thesis: ( m > k implies S . m meets G ) assume m > k ; ::_thesis: S . m meets G then S . m meets Int G by A4; hence S . m meets G by TOPS_1:16, XBOOLE_1:63; ::_thesis: verum end; hence x in Lim_inf S by Def1; ::_thesis: verum end; thus Lim_inf S c= Cl (Lim_inf S) by PRE_TOPC:18; ::_thesis: verum end; registration let T be non empty TopSpace; let S be SetSequence of the carrier of T; cluster Lim_inf S -> closed ; coherence Lim_inf S is closed proof Lim_inf S = Cl (Lim_inf S) by Th15; hence Lim_inf S is closed ; ::_thesis: verum end; end; theorem :: KURATO_2:16 for T being non empty TopSpace for 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; ::_thesis: for R, S being SetSequence of the carrier of T st R is subsequence of S holds Lim_inf S c= Lim_inf R let R, S be SetSequence of the carrier of T; ::_thesis: ( R is subsequence of S implies Lim_inf S c= Lim_inf R ) assume R is subsequence of S ; ::_thesis: Lim_inf S c= Lim_inf R then consider Nseq being increasing sequence of NAT such that A1: R = S * Nseq by VALUED_0:def_17; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Lim_inf S or x in Lim_inf R ) assume A2: x in Lim_inf S ; ::_thesis: x in Lim_inf R then reconsider p = x as Point of T ; for G being a_neighborhood of p ex k being Element of NAT st for m being Element of NAT st m > k holds R . m meets G proof let G be a_neighborhood of p; ::_thesis: ex k being Element of NAT st for m being Element of NAT st m > k holds R . m meets G consider k being Element of NAT such that A3: for m being Element of NAT st m > k holds S . m meets G by A2, Def1; take k ; ::_thesis: for m being Element of NAT st m > k holds R . m meets G let m1 be Element of NAT ; ::_thesis: ( m1 > k implies R . m1 meets G ) A4: m1 <= Nseq . m1 by SEQM_3:14; assume m1 > k ; ::_thesis: R . m1 meets G then A5: Nseq . m1 > k by A4, XXREAL_0:2; dom Nseq = NAT by FUNCT_2:def_1; then R . m1 = S . (Nseq . m1) by A1, FUNCT_1:13; hence R . m1 meets G by A3, A5; ::_thesis: verum end; hence x in Lim_inf R by Def1; ::_thesis: verum end; theorem Th17: :: KURATO_2:17 for T being non empty TopSpace for A, B being SetSequence of the carrier of T st ( for i being Element of NAT holds A . i c= B . i ) holds Lim_inf A c= Lim_inf B proof let T be non empty TopSpace; ::_thesis: for A, B being SetSequence of the carrier of T st ( for i being Element of NAT holds A . i c= B . i ) holds Lim_inf A c= Lim_inf B let A, B be SetSequence of the carrier of T; ::_thesis: ( ( for i being Element of NAT holds A . i c= B . i ) implies Lim_inf A c= Lim_inf B ) assume A1: for i being Element of NAT holds A . i c= B . i ; ::_thesis: Lim_inf A c= Lim_inf B let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Lim_inf A or x in Lim_inf B ) assume A2: x in Lim_inf A ; ::_thesis: x in Lim_inf B then reconsider p = x as Point of T ; for G being a_neighborhood of p ex k being Element of NAT st for m being Element of NAT st m > k holds B . m meets G proof let G be a_neighborhood of p; ::_thesis: ex k being Element of NAT st for m being Element of NAT st m > k holds B . m meets G consider k being Element of NAT such that A3: for m being Element of NAT st m > k holds A . m meets G by A2, Def1; take k ; ::_thesis: for m being Element of NAT st m > k holds B . m meets G let m1 be Element of NAT ; ::_thesis: ( m1 > k implies B . m1 meets G ) assume m1 > k ; ::_thesis: B . m1 meets G then A . m1 meets G by A3; hence B . m1 meets G by A1, XBOOLE_1:63; ::_thesis: verum end; hence x in Lim_inf B by Def1; ::_thesis: verum end; theorem :: KURATO_2:18 for T being non empty TopSpace for A, B, C being SetSequence of the carrier of T st ( for i being Element of 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; ::_thesis: for A, B, C being SetSequence of the carrier of T st ( for i being Element of NAT holds C . i = (A . i) \/ (B . i) ) holds (Lim_inf A) \/ (Lim_inf B) c= Lim_inf C let A, B, C be SetSequence of the carrier of T; ::_thesis: ( ( for i being Element of NAT holds C . i = (A . i) \/ (B . i) ) implies (Lim_inf A) \/ (Lim_inf B) c= Lim_inf C ) assume A1: for i being Element of NAT holds C . i = (A . i) \/ (B . i) ; ::_thesis: (Lim_inf A) \/ (Lim_inf B) c= Lim_inf C let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (Lim_inf A) \/ (Lim_inf B) or x in Lim_inf C ) assume A2: x in (Lim_inf A) \/ (Lim_inf B) ; ::_thesis: x in Lim_inf C then reconsider p = x as Point of T ; percases ( x in Lim_inf A or x in Lim_inf B ) by A2, XBOOLE_0:def_3; supposeA3: x in Lim_inf A ; ::_thesis: x in Lim_inf C for H being a_neighborhood of p ex k being Element of NAT st for m being Element of NAT st m > k holds C . m meets H proof let H be a_neighborhood of p; ::_thesis: ex k being Element of NAT st for m being Element of NAT st m > k holds C . m meets H consider k being Element of NAT such that A4: for m being Element of NAT st m > k holds A . m meets H by A3, Def1; take k ; ::_thesis: for m being Element of NAT st m > k holds C . m meets H let m be Element of NAT ; ::_thesis: ( m > k implies C . m meets H ) assume m > k ; ::_thesis: C . m meets H then A5: A . m meets H by A4; C . m = (A . m) \/ (B . m) by A1; hence C . m meets H by A5, XBOOLE_1:7, XBOOLE_1:63; ::_thesis: verum end; hence x in Lim_inf C by Def1; ::_thesis: verum end; supposeA6: x in Lim_inf B ; ::_thesis: x in Lim_inf C for H being a_neighborhood of p ex k being Element of NAT st for m being Element of NAT st m > k holds C . m meets H proof let H be a_neighborhood of p; ::_thesis: ex k being Element of NAT st for m being Element of NAT st m > k holds C . m meets H consider k being Element of NAT such that A7: for m being Element of NAT st m > k holds B . m meets H by A6, Def1; take k ; ::_thesis: for m being Element of NAT st m > k holds C . m meets H let m be Element of NAT ; ::_thesis: ( m > k implies C . m meets H ) assume m > k ; ::_thesis: C . m meets H then A8: B . m meets H by A7; C . m = (A . m) \/ (B . m) by A1; hence C . m meets H by A8, XBOOLE_1:7, XBOOLE_1:63; ::_thesis: verum end; hence x in Lim_inf C by Def1; ::_thesis: verum end; end; end; theorem :: KURATO_2:19 for T being non empty TopSpace for A, B, C being SetSequence of the carrier of T st ( for i being Element of 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; ::_thesis: for A, B, C being SetSequence of the carrier of T st ( for i being Element of NAT holds C . i = (A . i) /\ (B . i) ) holds Lim_inf C c= (Lim_inf A) /\ (Lim_inf B) let A, B, C be SetSequence of the carrier of T; ::_thesis: ( ( for i being Element of NAT holds C . i = (A . i) /\ (B . i) ) implies Lim_inf C c= (Lim_inf A) /\ (Lim_inf B) ) assume A1: for i being Element of NAT holds C . i = (A . i) /\ (B . i) ; ::_thesis: Lim_inf C c= (Lim_inf A) /\ (Lim_inf B) let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Lim_inf C or x in (Lim_inf A) /\ (Lim_inf B) ) assume A2: x in Lim_inf C ; ::_thesis: x in (Lim_inf A) /\ (Lim_inf B) then reconsider p = x as Point of T ; for H being a_neighborhood of p ex k being Element of NAT st for m being Element of NAT st m > k holds B . m meets H proof let H be a_neighborhood of p; ::_thesis: ex k being Element of NAT st for m being Element of NAT st m > k holds B . m meets H consider k being Element of NAT such that A3: for m being Element of NAT st m > k holds C . m meets H by A2, Def1; take k ; ::_thesis: for m being Element of NAT st m > k holds B . m meets H let m be Element of NAT ; ::_thesis: ( m > k implies B . m meets H ) assume m > k ; ::_thesis: B . m meets H then A4: C . m meets H by A3; C . m = (A . m) /\ (B . m) by A1; hence B . m meets H by A4, XBOOLE_1:17, XBOOLE_1:63; ::_thesis: verum end; then A5: x in Lim_inf B by Def1; for H being a_neighborhood of p ex k being Element of NAT st for m being Element of NAT st m > k holds A . m meets H proof let H be a_neighborhood of p; ::_thesis: ex k being Element of NAT st for m being Element of NAT st m > k holds A . m meets H consider k being Element of NAT such that A6: for m being Element of NAT st m > k holds C . m meets H by A2, Def1; take k ; ::_thesis: for m being Element of NAT st m > k holds A . m meets H let m be Element of NAT ; ::_thesis: ( m > k implies A . m meets H ) assume m > k ; ::_thesis: A . m meets H then A7: C . m meets H by A6; C . m = (A . m) /\ (B . m) by A1; hence A . m meets H by A7, XBOOLE_1:17, XBOOLE_1:63; ::_thesis: verum end; then x in Lim_inf A by Def1; hence x in (Lim_inf A) /\ (Lim_inf B) by A5, XBOOLE_0:def_4; ::_thesis: verum end; theorem Th20: :: KURATO_2:20 for T being non empty TopSpace for F, G being SetSequence of the carrier of T st ( for i being Element of NAT holds G . i = Cl (F . i) ) holds Lim_inf G = Lim_inf F proof let T be non empty TopSpace; ::_thesis: for F, G being SetSequence of the carrier of T st ( for i being Element of NAT holds G . i = Cl (F . i) ) holds Lim_inf G = Lim_inf F let F, G be SetSequence of the carrier of T; ::_thesis: ( ( for i being Element of NAT holds G . i = Cl (F . i) ) implies Lim_inf G = Lim_inf F ) assume A1: for i being Element of NAT holds G . i = Cl (F . i) ; ::_thesis: Lim_inf G = Lim_inf F thus Lim_inf G c= Lim_inf F :: according to XBOOLE_0:def_10 ::_thesis: Lim_inf F c= Lim_inf G proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Lim_inf G or x in Lim_inf F ) assume A2: x in Lim_inf G ; ::_thesis: x in Lim_inf F then reconsider p = x as Point of T ; for H being a_neighborhood of p ex k being Element of NAT st for m being Element of NAT st m > k holds F . m meets H proof let H be a_neighborhood of p; ::_thesis: ex k being Element of NAT st for m being Element of NAT st m > k holds F . m meets H 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 Element of NAT such that A6: for m being Element of NAT st m > k holds G . m meets H1 by A2, A3, Def1; take k ; ::_thesis: for m being Element of NAT st m > k holds F . m meets H let m be Element of NAT ; ::_thesis: ( m > k implies F . m meets H ) assume m > k ; ::_thesis: F . m meets H then G . m meets H1 by A6; then consider y being set such that A7: y in G . m and A8: y in H1 by XBOOLE_0:3; reconsider y = 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 F . m meets H by A5, XBOOLE_1:63; ::_thesis: verum end; hence x in Lim_inf F by Def1; ::_thesis: verum end; for i being Element of NAT holds F . i c= G . i proof let i be Element of NAT ; ::_thesis: F . i c= G . i G . i = Cl (F . i) by A1; hence F . i c= G . i by PRE_TOPC:18; ::_thesis: verum end; hence Lim_inf F c= Lim_inf G by Th17; ::_thesis: verum end; theorem :: KURATO_2:21 for n being Element of NAT for S being SetSequence of the carrier of (TOP-REAL n) for p being Point of (TOP-REAL n) st ex s being Real_Sequence of n st ( s is convergent & ( for x being Element of NAT holds s . x in S . x ) & p = lim s ) holds p in Lim_inf S proof let n be Element of NAT ; ::_thesis: for S being SetSequence of the carrier of (TOP-REAL n) for p being Point of (TOP-REAL n) st ex s being Real_Sequence of n st ( s is convergent & ( for x being Element of NAT holds s . x in S . x ) & p = lim s ) holds p in Lim_inf S let S be SetSequence of the carrier of (TOP-REAL n); ::_thesis: for p being Point of (TOP-REAL n) st ex s being Real_Sequence of n st ( s is convergent & ( for x being Element of NAT holds s . x in S . x ) & p = lim s ) holds p in Lim_inf S let p be Point of (TOP-REAL n); ::_thesis: ( ex s being Real_Sequence of n st ( s is convergent & ( for x being Element of NAT holds s . x in S . x ) & p = lim s ) implies p in Lim_inf S ) 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 Element of NAT holds s . x in S . x and A3: p = lim s ; ::_thesis: p in Lim_inf S for r being real number st r > 0 holds ex k being Element of NAT st for m being Element of NAT st m > k holds S . m meets Ball (p9,r) proof let r be real number ; ::_thesis: ( r > 0 implies ex k being Element of NAT st for m being Element of NAT st m > k holds S . m meets Ball (p9,r) ) reconsider r9 = r as Real by XREAL_0:def_1; assume r > 0 ; ::_thesis: ex k being Element of NAT st for m being Element of NAT st m > k holds S . m meets Ball (p9,r) then consider l being Element of NAT such that A4: for m being Element of NAT st l <= m holds |.((s . m) - p).| < r9 by A1, A3, TOPRNS_1:def_9; take v = max (0,l); ::_thesis: for m being Element of NAT st m > v holds S . m meets Ball (p9,r) let m be Element of NAT ; ::_thesis: ( m > v implies S . m meets Ball (p9,r) ) assume v < m ; ::_thesis: S . m meets Ball (p9,r) 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 S . m meets Ball (p9,r) by A5, XBOOLE_0:3; ::_thesis: verum end; hence p in Lim_inf S by Th14; ::_thesis: verum end; theorem Th22: :: KURATO_2:22 for T being non empty TopSpace for P being Subset of T for 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; ::_thesis: for P being Subset of T for 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 let P be Subset of T; ::_thesis: for 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 let s be SetSequence of the carrier of T; ::_thesis: ( ( for i being Nat holds s . i c= P ) implies Lim_inf s c= Cl P ) assume A1: for i being Nat holds s . i c= P ; ::_thesis: Lim_inf s c= Cl P let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Lim_inf s or x in Cl P ) assume A2: x in Lim_inf s ; ::_thesis: x in Cl P then reconsider p = x as Point of T ; for G being Subset of T st G is open & p in G holds P meets G proof let G be Subset of T; ::_thesis: ( G is open & p in G implies P meets G ) assume A3: G is open ; ::_thesis: ( not p in G or P meets G ) assume p in G ; ::_thesis: P meets G then reconsider G9 = G as a_neighborhood of p by A3, CONNSP_2:3; consider k being Element of NAT such that A4: for m being Element of NAT st m > k holds s . m meets G9 by A2, Def1; set m = k + 1; k + 1 > k by NAT_1:13; then s . (k + 1) meets G9 by A4; hence P meets G by A1, XBOOLE_1:63; ::_thesis: verum end; hence x in Cl P by PRE_TOPC:def_7; ::_thesis: verum end; theorem Th23: :: KURATO_2:23 for T being non empty TopSpace for F being SetSequence of the carrier of T for 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; ::_thesis: for F being SetSequence of the carrier of T for A being Subset of T st ( for i being Nat holds F . i = A ) holds Lim_inf F = Cl A let F be SetSequence of the carrier of T; ::_thesis: for A being Subset of T st ( for i being Nat holds F . i = A ) holds Lim_inf F = Cl A let A be Subset of T; ::_thesis: ( ( for i being Nat holds F . i = A ) implies Lim_inf F = Cl A ) assume A1: for i being Nat holds F . i = A ; ::_thesis: Lim_inf F = Cl A then for i being Nat holds F . i c= A ; hence Lim_inf F c= Cl A by Th22; :: according to XBOOLE_0:def_10 ::_thesis: Cl A c= Lim_inf F thus Cl A c= Lim_inf F ::_thesis: verum proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Cl A or x in Lim_inf F ) assume A2: x in Cl A ; ::_thesis: x in Lim_inf F then reconsider p = x as Point of T ; for G being a_neighborhood of p ex k being Element of NAT st for m being Element of NAT st m > k holds F . m meets G proof let G be a_neighborhood of p; ::_thesis: ex k being Element of NAT st for m being Element of NAT st m > k holds F . m meets G take k = 1; ::_thesis: for m being Element of NAT st m > k holds F . m meets G let m be Element of NAT ; ::_thesis: ( m > k implies F . m meets G ) assume m > k ; ::_thesis: F . m meets G F . m = A by A1; hence F . m meets G by A2, CONNSP_2:27; ::_thesis: verum end; hence x in Lim_inf F by Def1; ::_thesis: verum end; end; theorem :: KURATO_2:24 for T being non empty TopSpace for F being SetSequence of the carrier of T for 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; ::_thesis: for F being SetSequence of the carrier of T for A being closed Subset of T st ( for i being Nat holds F . i = A ) holds Lim_inf F = A let F be SetSequence of the carrier of T; ::_thesis: for A being closed Subset of T st ( for i being Nat holds F . i = A ) holds Lim_inf F = A let A be closed Subset of T; ::_thesis: ( ( for i being Nat holds F . i = A ) implies Lim_inf F = A ) assume for i being Nat holds F . i = A ; ::_thesis: Lim_inf F = A then Lim_inf F = Cl A by Th23; hence Lim_inf F = A by PRE_TOPC:22; ::_thesis: verum end; theorem Th25: :: KURATO_2:25 for n being Element of NAT for S being SetSequence of the carrier of (TOP-REAL n) for P being Subset of (TOP-REAL n) st P is bounded & ( for i being Element of NAT holds S . i c= P ) holds Lim_inf S is bounded proof let n be Element of NAT ; ::_thesis: for S being SetSequence of the carrier of (TOP-REAL n) for P being Subset of (TOP-REAL n) st P is bounded & ( for i being Element of NAT holds S . i c= P ) holds Lim_inf S is bounded let S be SetSequence of the carrier of (TOP-REAL n); ::_thesis: for P being Subset of (TOP-REAL n) st P is bounded & ( for i being Element of NAT holds S . i c= P ) holds Lim_inf S is bounded let P be Subset of (TOP-REAL n); ::_thesis: ( P is bounded & ( for i being Element of NAT holds S . i c= P ) implies Lim_inf S is bounded ) assume that A1: P is bounded and A2: for i being Element of NAT holds S . i c= P ; ::_thesis: Lim_inf S is bounded 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; set R = (1 + 1) + (3 * t); assume not Lim_inf S is bounded ; ::_thesis: contradiction 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) > (1 + 1) + (3 * t) by A3, Th8; consider k1 being Element of NAT such that A8: for m being Element of NAT st m > k1 holds S . m meets Ball (x,1) by A5, Th14; consider k2 being Element of NAT such that A9: for m being Element of NAT st m > k2 holds S . m meets Ball (y,1) by A6, Th14; set k = (max (k1,k2)) + 1; S . ((max (k1,k2)) + 1) c= P9 by A2; then A10: S . ((max (k1,k2)) + 1) c= Ball (z,t) by A4, XBOOLE_1:1; 2 * t < 3 * t by A3, XREAL_1:68; then A11: (1 + 1) + (2 * t) < (1 + 1) + (3 * t) by XREAL_1:8; max (k1,k2) >= k2 by XXREAL_0:25; then (max (k1,k2)) + 1 > k2 by NAT_1:13; then A12: Ball (z,t) meets Ball (y,1) by A9, A10, XBOOLE_1:63; max (k1,k2) >= k1 by XXREAL_0:25; then (max (k1,k2)) + 1 > k1 by NAT_1:13; then Ball (z,t) meets Ball (x,1) by A8, A10, XBOOLE_1:63; hence contradiction by A7, A12, A11, Th10, XXREAL_0:2; ::_thesis: verum end; theorem :: KURATO_2:26 for S being SetSequence of the carrier of (TOP-REAL 2) for P being Subset of (TOP-REAL 2) st P is bounded & ( for i being Element of NAT holds S . i c= P ) holds Lim_inf S is compact by Th25, TOPREAL6:79; theorem Th27: :: KURATO_2:27 for n being Element of NAT for A, B being SetSequence of the carrier of (TOP-REAL n) for C being SetSequence of the carrier of [:(TOP-REAL n),(TOP-REAL n):] st ( for i being Element of NAT holds C . i = [:(A . i),(B . i):] ) holds [:(Lim_inf A),(Lim_inf B):] = Lim_inf C proof let n be Element of NAT ; ::_thesis: for A, B being SetSequence of the carrier of (TOP-REAL n) for C being SetSequence of the carrier of [:(TOP-REAL n),(TOP-REAL n):] st ( for i being Element of NAT holds C . i = [:(A . i),(B . i):] ) holds [:(Lim_inf A),(Lim_inf B):] = Lim_inf C let A, B be SetSequence of the carrier of (TOP-REAL n); ::_thesis: for C being SetSequence of the carrier of [:(TOP-REAL n),(TOP-REAL n):] st ( for i being Element of NAT holds C . i = [:(A . i),(B . i):] ) holds [:(Lim_inf A),(Lim_inf B):] = Lim_inf C let C be SetSequence of the carrier of [:(TOP-REAL n),(TOP-REAL n):]; ::_thesis: ( ( for i being Element of NAT holds C . i = [:(A . i),(B . i):] ) implies [:(Lim_inf A),(Lim_inf B):] = Lim_inf C ) assume A1: for i being Element of NAT holds C . i = [:(A . i),(B . i):] ; ::_thesis: [:(Lim_inf A),(Lim_inf B):] = Lim_inf C thus [:(Lim_inf A),(Lim_inf B):] c= Lim_inf C :: according to XBOOLE_0:def_10 ::_thesis: Lim_inf C c= [:(Lim_inf A),(Lim_inf B):] proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in [:(Lim_inf A),(Lim_inf B):] or x in Lim_inf C ) assume A2: x in [:(Lim_inf A),(Lim_inf B):] ; ::_thesis: x in Lim_inf C then consider x1, x2 being set 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 = x1, x2 = x2 as Point of (TOP-REAL n) by A3, A4; for G being a_neighborhood of p ex k being Element of NAT st for m being Element of NAT st m > k holds C . m meets G proof let G be a_neighborhood of p; ::_thesis: ex k being Element of NAT st for m being Element of NAT st m > k holds C . m meets G 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 Element of NAT such that A7: for m being Element of 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 Element of NAT such that A8: for m being Element of NAT st m > k1 holds A . m meets V by A3, Def1; take k = max (k1,k2); ::_thesis: for m being Element of NAT st m > k holds C . m meets G let m be Element of NAT ; ::_thesis: ( m > k implies C . m meets G ) assume A9: m > k ; ::_thesis: C . m meets G 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 C . m meets G by A6, XBOOLE_1:63; ::_thesis: verum end; hence x in Lim_inf C by Def1; ::_thesis: verum end; thus Lim_inf C c= [:(Lim_inf A),(Lim_inf B):] ::_thesis: verum proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Lim_inf C or x in [:(Lim_inf A),(Lim_inf B):] ) assume A11: x in Lim_inf C ; ::_thesis: x in [:(Lim_inf A),(Lim_inf B):] 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 Element of NAT st for m being Element of NAT st m > k holds B . m meets G proof let G be a_neighborhood of p2; ::_thesis: ex k being Element of NAT st for m being Element of NAT st m > k holds B . m meets G consider k being Element of NAT such that A14: for m being Element of NAT st m > k holds C . m meets [: the a_neighborhood of p1,G:] by A11, A13, Def1; take k ; ::_thesis: for m being Element of NAT st m > k holds B . m meets G let m be Element of NAT ; ::_thesis: ( m > k implies B . m meets G ) assume m > k ; ::_thesis: B . m meets G then C . m meets [: the a_neighborhood of p1,G:] by A14; then consider y being set such that A15: y in C . m and A16: y in [: the a_neighborhood of p1,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 B . m meets G by A17, XBOOLE_0:3; ::_thesis: verum end; then A18: p2 in Lim_inf B by Def1; for G being a_neighborhood of p1 ex k being Element of NAT st for m being Element of NAT st m > k holds A . m meets G proof let G be a_neighborhood of p1; ::_thesis: ex k being Element of NAT st for m being Element of NAT st m > k holds A . m meets G consider k being Element of NAT such that A19: for m being Element of NAT st m > k holds C . m meets [:G, the a_neighborhood of p2:] by A11, A13, Def1; take k ; ::_thesis: for m being Element of NAT st m > k holds A . m meets G let m be Element of NAT ; ::_thesis: ( m > k implies A . m meets G ) assume m > k ; ::_thesis: A . m meets G then C . m meets [:G, the a_neighborhood of p2:] by A19; then consider y being set such that A20: y in C . m and A21: y in [:G, the a_neighborhood of p2:] 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 A . m meets G by A22, XBOOLE_0:3; ::_thesis: verum end; then p1 in Lim_inf A by Def1; hence x in [:(Lim_inf A),(Lim_inf B):] by A13, A18, ZFMISC_1:87; ::_thesis: verum end; end; theorem :: KURATO_2:28 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); ::_thesis: lim_inf S c= Lim_inf S let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in lim_inf S or x in Lim_inf S ) assume A1: x in lim_inf S ; ::_thesis: 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 Element of NAT such that A2: for n being Element of NAT holds x in S . (k + n) by A1, KURATO_0:4; for r being real number st r > 0 holds ex k being Element of NAT st for m being Element of NAT st m > k holds S . m meets Ball (p,r) proof let r be real number ; ::_thesis: ( r > 0 implies ex k being Element of NAT st for m being Element of NAT st m > k holds S . m meets Ball (p,r) ) assume r > 0 ; ::_thesis: ex k being Element of NAT st for m being Element of NAT st m > k holds S . m meets Ball (p,r) then A3: x in Ball (p,r) by GOBOARD6:1; take k ; ::_thesis: for m being Element of NAT st m > k holds S . m meets Ball (p,r) let m be Element of NAT ; ::_thesis: ( m > k implies S . m meets Ball (p,r) ) assume m > k ; ::_thesis: S . m meets Ball (p,r) then consider h being Nat such that A4: m = k + h by NAT_1:10; h in NAT by ORDINAL1:def_12; then x in S . m by A2, A4; hence S . m meets Ball (p,r) by A3, XBOOLE_0:3; ::_thesis: verum end; then y in Lim_inf S by Th14; hence x in Lim_inf S ; ::_thesis: verum end; theorem :: KURATO_2:29 for C being Simple_closed_curve for i being Element of NAT holds Fr ((UBD (L~ (Cage (C,i)))) `) = L~ (Cage (C,i)) proof let C be Simple_closed_curve; ::_thesis: for i being Element of NAT holds Fr ((UBD (L~ (Cage (C,i)))) `) = L~ (Cage (C,i)) let i be Element of NAT ; ::_thesis: Fr ((UBD (L~ (Cage (C,i)))) `) = L~ (Cage (C,i)) set K = (UBD (L~ (Cage (C,i)))) ` ; set R = L~ (Cage (C,i)); A1: (BDD (L~ (Cage (C,i)))) \/ ((BDD (L~ (Cage (C,i)))) `) = [#] (TOP-REAL 2) by PRE_TOPC:2; UBD (L~ (Cage (C,i))) c= (L~ (Cage (C,i))) ` by JORDAN2C:26; then A2: UBD (L~ (Cage (C,i))) misses L~ (Cage (C,i)) by SUBSET_1:23; UBD (L~ (Cage (C,i))) misses BDD (L~ (Cage (C,i))) by JORDAN2C:24; then A3: UBD (L~ (Cage (C,i))) misses (BDD (L~ (Cage (C,i)))) \/ (L~ (Cage (C,i))) by A2, XBOOLE_1:70; [#] (TOP-REAL 2) = ((L~ (Cage (C,i))) `) \/ (L~ (Cage (C,i))) by PRE_TOPC:2 .= ((BDD (L~ (Cage (C,i)))) \/ (UBD (L~ (Cage (C,i))))) \/ (L~ (Cage (C,i))) by JORDAN2C:27 ; then A4: (UBD (L~ (Cage (C,i)))) ` = ((UBD (L~ (Cage (C,i)))) \/ ((BDD (L~ (Cage (C,i)))) \/ (L~ (Cage (C,i))))) \ (UBD (L~ (Cage (C,i)))) by XBOOLE_1:4 .= (L~ (Cage (C,i))) \/ (BDD (L~ (Cage (C,i)))) by A3, XBOOLE_1:88 ; ((BDD (L~ (Cage (C,i)))) \/ (UBD (L~ (Cage (C,i))))) ` = ((L~ (Cage (C,i))) `) ` by JORDAN2C:27; then ((BDD (L~ (Cage (C,i)))) `) /\ ((UBD (L~ (Cage (C,i)))) `) = L~ (Cage (C,i)) by XBOOLE_1:53; then (BDD (L~ (Cage (C,i)))) \/ (L~ (Cage (C,i))) = ((BDD (L~ (Cage (C,i)))) \/ ((BDD (L~ (Cage (C,i)))) `)) /\ ((BDD (L~ (Cage (C,i)))) \/ ((UBD (L~ (Cage (C,i)))) `)) by XBOOLE_1:24 .= (BDD (L~ (Cage (C,i)))) \/ ((UBD (L~ (Cage (C,i)))) `) by A1, XBOOLE_1:28 .= (UBD (L~ (Cage (C,i)))) ` by A4, XBOOLE_1:7, XBOOLE_1:12 ; then A5: Cl ((UBD (L~ (Cage (C,i)))) `) = (BDD (L~ (Cage (C,i)))) \/ (L~ (Cage (C,i))) by PRE_TOPC:22; A6: ((UBD (L~ (Cage (C,i)))) `) ` = 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)))) = {} by XBOOLE_0:def_7; Fr ((UBD (L~ (Cage (C,i)))) `) = (Cl ((UBD (L~ (Cage (C,i)))) `)) /\ (Cl (((UBD (L~ (Cage (C,i)))) `) `)) 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 Fr ((UBD (L~ (Cage (C,i)))) `) = L~ (Cage (C,i)) ; ::_thesis: verum end; begin 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: :: KURATO_2:def 2 for x being set holds ( x in it iff ex A being subsequence of S st x in Lim_inf A ); existence ex b1 being Subset of T st for x being set holds ( x in b1 iff ex A being subsequence of S st x in Lim_inf A ) proof defpred S1[ set ] means ex A being subsequence of S st \$1 in Lim_inf A; consider X being set such that A1: for x being set holds ( x in X iff ( x in the carrier of T & S1[x] ) ) from XBOOLE_0:sch_1(); X c= the carrier of T proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in X or x in the carrier of T ) assume x in X ; ::_thesis: x in the carrier of T hence x in the carrier of T by A1; ::_thesis: verum end; then reconsider X = X as Subset of T ; take X ; ::_thesis: for x being set holds ( x in X iff ex A being subsequence of S st x in Lim_inf A ) thus for x being set holds ( x in X iff ex A being subsequence of S st x in Lim_inf A ) by A1; ::_thesis: verum end; uniqueness for b1, b2 being Subset of T st ( for x being set holds ( x in b1 iff ex A being subsequence of S st x in Lim_inf A ) ) & ( for x being set holds ( x in b2 iff ex A being subsequence of S st x in Lim_inf A ) ) holds b1 = b2 proof defpred S1[ set ] means ex A being subsequence of S st \$1 in Lim_inf A; let A1, A2 be Subset of T; ::_thesis: ( ( for x being set holds ( x in A1 iff ex A being subsequence of S st x in Lim_inf A ) ) & ( for x being set holds ( x in A2 iff ex A being subsequence of S st x in Lim_inf A ) ) implies A1 = A2 ) assume that A2: for x being set holds ( x in A1 iff S1[x] ) and A3: for x being set holds ( x in A2 iff S1[x] ) ; ::_thesis: A1 = A2 A1 = A2 from XBOOLE_0:sch_2(A2, A3); hence A1 = A2 ; ::_thesis: verum end; end; :: deftheorem Def2 defines Lim_sup KURATO_2:def_2_:_ for T being non empty TopSpace for S being SetSequence of the carrier of T for b3 being Subset of T holds ( b3 = Lim_sup S iff for x being set holds ( x in b3 iff ex A being subsequence of S st x in Lim_inf A ) ); theorem :: KURATO_2:30 for N being Element of NAT for F being sequence of (TOP-REAL N) for x being Point of (TOP-REAL N) for x9 being Point of (Euclid N) st x = x9 holds ( x is_a_cluster_point_of F iff for r being real number for n being Element of NAT st r > 0 holds ex m being Element of NAT st ( n <= m & F . m in Ball (x9,r) ) ) proof let N be Element of NAT ; ::_thesis: for F being sequence of (TOP-REAL N) for x being Point of (TOP-REAL N) for x9 being Point of (Euclid N) st x = x9 holds ( x is_a_cluster_point_of F iff for r being real number for n being Element of NAT st r > 0 holds ex m being Element of NAT st ( n <= m & F . m in Ball (x9,r) ) ) let F be sequence of (TOP-REAL N); ::_thesis: for x being Point of (TOP-REAL N) for x9 being Point of (Euclid N) st x = x9 holds ( x is_a_cluster_point_of F iff for r being real number for n being Element of NAT st r > 0 holds ex m being Element of NAT st ( n <= m & F . m in Ball (x9,r) ) ) let x be Point of (TOP-REAL N); ::_thesis: for x9 being Point of (Euclid N) st x = x9 holds ( x is_a_cluster_point_of F iff for r being real number for n being Element of NAT st r > 0 holds ex m being Element of NAT st ( n <= m & F . m in Ball (x9,r) ) ) let x9 be Point of (Euclid N); ::_thesis: ( x = x9 implies ( x is_a_cluster_point_of F iff for r being real number for n being Element of NAT st r > 0 holds ex m being Element of NAT st ( n <= m & F . m in Ball (x9,r) ) ) ) assume A1: x = x9 ; ::_thesis: ( x is_a_cluster_point_of F iff for r being real number for n being Element of NAT st r > 0 holds ex m being Element of NAT st ( n <= m & F . m in Ball (x9,r) ) ) hereby ::_thesis: ( ( for r being real number for n being Element of NAT st r > 0 holds ex m being Element of NAT st ( n <= m & F . m in Ball (x9,r) ) ) implies x is_a_cluster_point_of F ) assume A2: x is_a_cluster_point_of F ; ::_thesis: for r being real number for n being Element of NAT st r > 0 holds ex m being Element of NAT st ( n <= m & F . m in Ball (x9,r) ) let r be real number ; ::_thesis: for n being Element of NAT st r > 0 holds ex m being Element of NAT st ( n <= m & F . m in Ball (x9,r) ) let n be Element of NAT ; ::_thesis: ( r > 0 implies ex m being Element of NAT st ( n <= m & F . m in Ball (x9,r) ) ) reconsider O = Ball (x9,r) as open Subset of (TOP-REAL N) by Th1; assume r > 0 ; ::_thesis: ex m being Element of NAT st ( n <= m & F . m in Ball (x9,r) ) 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 = m as Element of NAT ; take m = m; ::_thesis: ( n <= m & F . m in Ball (x9,r) ) thus ( n <= m & F . m in Ball (x9,r) ) by A3; ::_thesis: verum end; assume A4: for r being real number for n being Element of NAT st r > 0 holds ex m being Element of NAT st ( n <= m & F . m in Ball (x9,r) ) ; ::_thesis: x is_a_cluster_point_of F for O being Subset of (TOP-REAL N) for n being Element of NAT st O is open & x in O holds ex m being Element of NAT st ( n <= m & F . m in O ) proof let O be Subset of (TOP-REAL N); ::_thesis: for n being Element of NAT st O is open & x in O holds ex m being Element of NAT st ( n <= m & F . m in O ) let n be Element of NAT ; ::_thesis: ( O is open & x in O implies ex m being Element of NAT st ( n <= m & F . m in O ) ) assume that A5: O is open and A6: x in O ; ::_thesis: ex m being Element of NAT st ( n <= m & F . m in O ) reconsider n9 = n as Element of NAT ; A7: TopStruct(# the carrier of (TOP-REAL N), the topology 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 number such that A8: r > 0 and A9: Ball (x9,r) c= G9 by A1, A6, TOPMETR:15; consider m being Element of NAT such that A10: ( n9 <= m & F . m in Ball (x9,r) ) by A4, A8; take m ; ::_thesis: ( n <= m & F . m in O ) thus ( n <= m & F . m in O ) by A9, A10; ::_thesis: verum end; hence x is_a_cluster_point_of F by FRECHET2:def_3; ::_thesis: verum end; theorem Th31: :: KURATO_2:31 for T being non empty TopSpace for A being SetSequence of the carrier of T holds Lim_inf A c= Lim_sup A proof let T be non empty TopSpace; ::_thesis: for A being SetSequence of the carrier of T holds Lim_inf A c= Lim_sup A let A be SetSequence of the carrier of T; ::_thesis: Lim_inf A c= Lim_sup A let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Lim_inf A or x in Lim_sup A ) assume A1: x in Lim_inf A ; ::_thesis: x in Lim_sup 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 ; ::_thesis: x in Lim_inf B thus x in Lim_inf B by A1; ::_thesis: verum end; hence x in Lim_sup A by Def2; ::_thesis: verum end; theorem Th32: :: KURATO_2:32 for A, B, C being SetSequence of the carrier of (TOP-REAL 2) st ( for i being Element of NAT holds A . i c= B . i ) & C is subsequence of A holds ex D being subsequence of B st for i being Element of NAT holds C . i c= D . i proof let A, B, C be SetSequence of the carrier of (TOP-REAL 2); ::_thesis: ( ( for i being Element of NAT holds A . i c= B . i ) & C is subsequence of A implies ex D being subsequence of B st for i being Element of NAT holds C . i c= D . i ) assume that A1: for i being Element of NAT holds A . i c= B . i and A2: C is subsequence of A ; ::_thesis: ex D being subsequence of B st for i being Element of NAT holds C . i c= D . i 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 = B * NS as SetSequence of (TOP-REAL 2) ; reconsider D = D as subsequence of B ; take D ; ::_thesis: for i being Element of NAT holds C . i c= D . i for i being Element of NAT holds C . i c= D . i proof let i be Element of NAT ; ::_thesis: C . i c= D . i A4: dom NS = NAT by FUNCT_2:def_1; C . i c= D . i proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in C . i or x in D . i ) assume x in C . i ; ::_thesis: x in D . i then A5: x in A . (NS . i) by A3, A4, FUNCT_1:13; A . (NS . i) c= B . (NS . i) by A1; then x in B . (NS . i) by A5; hence x in D . i by A4, FUNCT_1:13; ::_thesis: verum end; hence C . i c= D . i ; ::_thesis: verum end; hence for i being Element of NAT holds C . i c= D . i ; ::_thesis: verum end; theorem :: KURATO_2:33 for A, B, C being SetSequence of the carrier of (TOP-REAL 2) st ( for i being Element of NAT holds A . i c= B . i ) & C is subsequence of B holds ex D being subsequence of A st for i being Element of NAT holds D . i c= C . i proof let A, B, C be SetSequence of the carrier of (TOP-REAL 2); ::_thesis: ( ( for i being Element of NAT holds A . i c= B . i ) & C is subsequence of B implies ex D being subsequence of A st for i being Element of NAT holds D . i c= C . i ) assume that A1: for i being Element of NAT holds A . i c= B . i and A2: C is subsequence of B ; ::_thesis: ex D being subsequence of A st for i being Element of NAT holds D . i c= C . i 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 = A * NS as SetSequence of (TOP-REAL 2) ; reconsider D = D as subsequence of A ; take D ; ::_thesis: for i being Element of NAT holds D . i c= C . i for i being Element of NAT holds D . i c= C . i proof let i be Element of NAT ; ::_thesis: D . i c= C . i A4: dom NS = NAT by FUNCT_2:def_1; D . i c= C . i proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in D . i or x in C . i ) assume x in D . i ; ::_thesis: x in C . i then A5: x in A . (NS . i) by A4, FUNCT_1:13; A . (NS . i) c= B . (NS . i) by A1; then x in B . (NS . i) by A5; hence x in C . i by A3, A4, FUNCT_1:13; ::_thesis: verum end; hence D . i c= C . i ; ::_thesis: verum end; hence for i being Element of NAT holds D . i c= C . i ; ::_thesis: verum end; theorem Th34: :: KURATO_2:34 for A, B being SetSequence of the carrier of (TOP-REAL 2) st ( for i being Element of 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); ::_thesis: ( ( for i being Element of NAT holds A . i c= B . i ) implies Lim_sup A c= Lim_sup B ) assume A1: for i being Element of NAT holds A . i c= B . i ; ::_thesis: Lim_sup A c= Lim_sup B Lim_sup A c= Lim_sup B proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Lim_sup A or x in Lim_sup B ) assume x in Lim_sup A ; ::_thesis: x in Lim_sup B 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 Element of NAT holds A1 . i c= D . i by A1, Th32; Lim_inf A1 c= Lim_inf D by A3, Th17; hence x in Lim_sup B by A2, Def2; ::_thesis: verum end; hence Lim_sup A c= Lim_sup B ; ::_thesis: verum end; theorem :: KURATO_2:35 for A, B, C being SetSequence of the carrier of (TOP-REAL 2) st ( for i being Element of 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); ::_thesis: ( ( for i being Element of NAT holds C . i = (A . i) \/ (B . i) ) implies (Lim_sup A) \/ (Lim_sup B) c= Lim_sup C ) assume A1: for i being Element of NAT holds C . i = (A . i) \/ (B . i) ; ::_thesis: (Lim_sup A) \/ (Lim_sup B) c= Lim_sup C A2: for i being Element of NAT holds B . i c= C . i proof let i be Element of NAT ; ::_thesis: B . i c= C . i C . i = (A . i) \/ (B . i) by A1; hence B . i c= C . i by XBOOLE_1:7; ::_thesis: verum end; A3: for i being Element of NAT holds A . i c= C . i proof let i be Element of NAT ; ::_thesis: A . i c= C . i C . i = (A . i) \/ (B . i) by A1; hence A . i c= C . i by XBOOLE_1:7; ::_thesis: verum end; thus (Lim_sup A) \/ (Lim_sup B) c= Lim_sup C ::_thesis: verum proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (Lim_sup A) \/ (Lim_sup B) or x in Lim_sup C ) assume A4: x in (Lim_sup A) \/ (Lim_sup B) ; ::_thesis: x in Lim_sup C percases ( x in Lim_sup A or x in Lim_sup B ) by A4, XBOOLE_0:def_3; suppose x in Lim_sup A ; ::_thesis: x in Lim_sup C 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 Element of NAT holds A1 . i c= C1 . i by A3, Th32; Lim_inf A1 c= Lim_inf C1 by A6, Th17; hence x in Lim_sup C by A5, Def2; ::_thesis: verum end; suppose x in Lim_sup B ; ::_thesis: x in Lim_sup C 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 Element of NAT holds B1 . i c= C1 . i by A2, Th32; Lim_inf B1 c= Lim_inf C1 by A8, Th17; hence x in Lim_sup C by A7, Def2; ::_thesis: verum end; end; end; end; theorem :: KURATO_2:36 for A, B, C being SetSequence of the carrier of (TOP-REAL 2) st ( for i being Element of 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); ::_thesis: ( ( for i being Element of NAT holds C . i = (A . i) /\ (B . i) ) implies Lim_sup C c= (Lim_sup A) /\ (Lim_sup B) ) assume A1: for i being Element of NAT holds C . i = (A . i) /\ (B . i) ; ::_thesis: Lim_sup C c= (Lim_sup A) /\ (Lim_sup B) let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Lim_sup C or x in (Lim_sup A) /\ (Lim_sup B) ) assume x in Lim_sup C ; ::_thesis: x in (Lim_sup A) /\ (Lim_sup B) then consider C1 being subsequence of C such that A2: x in Lim_inf C1 by Def2; for i being Element of NAT holds C . i c= B . i proof let i be Element of NAT ; ::_thesis: C . i c= B . i C . i = (A . i) /\ (B . i) by A1; hence C . i c= B . i by XBOOLE_1:17; ::_thesis: verum end; then consider E1 being subsequence of B such that A3: for i being Element of 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 Element of NAT holds C . i c= A . i proof let i be Element of NAT ; ::_thesis: C . i c= A . i C . i = (A . i) /\ (B . i) by A1; hence C . i c= A . i by XBOOLE_1:17; ::_thesis: verum end; then consider D1 being subsequence of A such that A5: for i being Element of 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 x in (Lim_sup A) /\ (Lim_sup B) by A4, XBOOLE_0:def_4; ::_thesis: verum end; theorem Th37: :: KURATO_2:37 for A, B being SetSequence of the carrier of (TOP-REAL 2) for C, C1 being SetSequence of the carrier of [:(TOP-REAL 2),(TOP-REAL 2):] st ( for i being Element of 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 Element of NAT holds C1 . i = [:(A1 . i),(B1 . i):] ) ) proof let A, B be SetSequence of the carrier of (TOP-REAL 2); ::_thesis: for C, C1 being SetSequence of the carrier of [:(TOP-REAL 2),(TOP-REAL 2):] st ( for i being Element of 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 Element of NAT holds C1 . i = [:(A1 . i),(B1 . i):] ) ) let C, C1 be SetSequence of the carrier of [:(TOP-REAL 2),(TOP-REAL 2):]; ::_thesis: ( ( for i being Element of NAT holds C . i = [:(A . i),(B . i):] ) & C1 is subsequence of C implies 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 Element of NAT holds C1 . i = [:(A1 . i),(B1 . i):] ) ) ) assume that A1: for i being Element of NAT holds C . i = [:(A . i),(B . i):] and A2: C1 is subsequence of C ; ::_thesis: 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 Element of NAT holds C1 . i = [:(A1 . i),(B1 . i):] ) ) 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 = A * NS as SetSequence of (TOP-REAL 2) ; reconsider B1 = B * NS as SetSequence of (TOP-REAL 2) ; take A1 ; ::_thesis: ex B1 being SetSequence of the carrier of (TOP-REAL 2) st ( A1 is subsequence of A & B1 is subsequence of B & ( for i being Element of NAT holds C1 . i = [:(A1 . i),(B1 . i):] ) ) take B1 ; ::_thesis: ( A1 is subsequence of A & B1 is subsequence of B & ( for i being Element of NAT holds C1 . i = [:(A1 . i),(B1 . i):] ) ) for i being Element of NAT holds C1 . i = [:(A1 . i),(B1 . i):] proof let i be Element of NAT ; ::_thesis: C1 . i = [:(A1 . i),(B1 . i):] A4: dom NS = NAT by FUNCT_2:def_1; then A5: ( A1 . i = A . (NS . i) & B1 . i = B . (NS . i) ) by FUNCT_1:13; C1 . i = C . (NS . i) by A3, A4, FUNCT_1:13 .= [:(A1 . i),(B1 . i):] by A1, A5 ; hence C1 . i = [:(A1 . i),(B1 . i):] ; ::_thesis: verum end; hence ( A1 is subsequence of A & B1 is subsequence of B & ( for i being Element of NAT holds C1 . i = [:(A1 . i),(B1 . i):] ) ) ; ::_thesis: verum end; theorem :: KURATO_2:38 for A, B being SetSequence of the carrier of (TOP-REAL 2) for C being SetSequence of the carrier of [:(TOP-REAL 2),(TOP-REAL 2):] st ( for i being Element of 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); ::_thesis: for C being SetSequence of the carrier of [:(TOP-REAL 2),(TOP-REAL 2):] st ( for i being Element of NAT holds C . i = [:(A . i),(B . i):] ) holds Lim_sup C c= [:(Lim_sup A),(Lim_sup B):] let C be SetSequence of the carrier of [:(TOP-REAL 2),(TOP-REAL 2):]; ::_thesis: ( ( for i being Element of NAT holds C . i = [:(A . i),(B . i):] ) implies Lim_sup C c= [:(Lim_sup A),(Lim_sup B):] ) assume A1: for i being Element of NAT holds C . i = [:(A . i),(B . i):] ; ::_thesis: Lim_sup C c= [:(Lim_sup A),(Lim_sup B):] let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Lim_sup C or x in [:(Lim_sup A),(Lim_sup B):] ) assume x in Lim_sup C ; ::_thesis: x in [:(Lim_sup A),(Lim_sup B):] 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 set 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 Element of 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 x in [:(Lim_sup A),(Lim_sup B):] by A3, A8, ZFMISC_1:87; ::_thesis: verum end; theorem Th39: :: KURATO_2:39 for T being non empty TopSpace for F being SetSequence of the carrier of T for 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; ::_thesis: for F being SetSequence of the carrier of T for A being Subset of T st ( for i being Nat holds F . i = A ) holds Lim_inf F = Lim_sup F let F be SetSequence of the carrier of T; ::_thesis: for A being Subset of T st ( for i being Nat holds F . i = A ) holds Lim_inf F = Lim_sup F let A be Subset of T; ::_thesis: ( ( for i being Nat holds F . i = A ) implies Lim_inf F = Lim_sup F ) assume A1: for i being Nat holds F . i = A ; ::_thesis: Lim_inf F = Lim_sup F thus Lim_inf F c= Lim_sup F by Th31; :: according to XBOOLE_0:def_10 ::_thesis: Lim_sup F c= Lim_inf F thus Lim_sup F c= Lim_inf F ::_thesis: verum proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Lim_sup F or x in Lim_inf F ) assume x in Lim_sup F ; ::_thesis: x in Lim_inf F then ex G being subsequence of F st x in Lim_inf G by Def2; hence x in Lim_inf F by A1, Th12; ::_thesis: verum end; end; theorem :: KURATO_2:40 for F being SetSequence of the carrier of (TOP-REAL 2) for 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); ::_thesis: for A being Subset of (TOP-REAL 2) st ( for i being Nat holds F . i = A ) holds Lim_sup F = Cl A let A be Subset of (TOP-REAL 2); ::_thesis: ( ( for i being Nat holds F . i = A ) implies Lim_sup F = Cl A ) assume A1: for i being Nat holds F . i = A ; ::_thesis: Lim_sup F = Cl A then Lim_inf F = Lim_sup F by Th39; hence Lim_sup F = Cl A by A1, Th23; ::_thesis: verum end; theorem :: KURATO_2:41 for F, G being SetSequence of the carrier of (TOP-REAL 2) st ( for i being Element of 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); ::_thesis: ( ( for i being Element of NAT holds G . i = Cl (F . i) ) implies Lim_sup G = Lim_sup F ) assume A1: for i being Element of NAT holds G . i = Cl (F . i) ; ::_thesis: Lim_sup G = Lim_sup F thus Lim_sup G c= Lim_sup F :: according to XBOOLE_0:def_10 ::_thesis: Lim_sup F c= Lim_sup G proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Lim_sup G or x in Lim_sup F ) assume x in Lim_sup G ; ::_thesis: x in Lim_sup F 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 = F * NS as SetSequence of (TOP-REAL 2) ; reconsider P = P as subsequence of F ; for i being Element of NAT holds H . i = Cl (P . i) proof let i be Element of NAT ; ::_thesis: H . i = Cl (P . i) A4: dom NS = NAT by FUNCT_2:def_1; then H . i = G . (NS . i) by A3, FUNCT_1:13 .= Cl (F . (NS . i)) by A1 .= Cl (P . i) by A4, FUNCT_1:13 ; hence H . i = Cl (P . i) ; ::_thesis: verum end; then Lim_inf H = Lim_inf P by Th20; hence x in Lim_sup F by A2, Def2; ::_thesis: verum end; for i being Element of NAT holds F . i c= G . i proof let i be Element of NAT ; ::_thesis: F . i c= G . i G . i = Cl (F . i) by A1; hence F . i c= G . i by PRE_TOPC:18; ::_thesis: verum end; hence Lim_sup F c= Lim_sup G by Th34; ::_thesis: verum end;