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