:: Double Sequences and Iterated Limits in Regular Space
:: by Roland Coghetto
::
:: Received June 30, 2016
:: Copyright (c) 2016-2018 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies TOPS_1, YELLOW_1, SEQ_2, XCMPLX_0, FINSEQ_2, COMPLEX1, REAL_1,
METRIC_1, EUCLID, YELLOW19, CONNSP_2, PRE_TOPC, FUNCT_1, STRUCT_0,
CARD_3, FACIRC_1, FINSET_1, CARD_1, XBOOLE_0, SUBSET_1, SETFAM_1, TARSKI,
ZFMISC_1, RELAT_1, CARD_FIL, PBOOLE, XXREAL_0, WAYBEL_0, NUMBERS,
FINSEQ_1, NAT_1, YELLOW13, ARYTM_3, CANTOR_1, FILTER_0, DICKSON,
MEMBERED, XXREAL_1, CARDFIL2, MCART_1, ARYTM_1, CARDFIL4, ORDINAL2,
FRECHET, PCOMPS_1, DBLSEQ_1, CARD_5, MESFUNC9, COMPTS_1, WAYBEL_7,
RCOMP_1, LATTICE3, LATTICES, TOPMETR;
notations RCOMP_1, YELLOW19, CONNSP_2, TARSKI, RELAT_1, SETFAM_1, FINSET_1,
NUMBERS, XXREAL_0, FINSEQ_1, DICKSON, WAYBEL_0, MEMBERED, XTUPLE_0,
XBOOLE_0, CARD_FIL, CARDFIL2, XXREAL_2, CARD_3, PRE_TOPC, RELSET_1,
EUCLID, XREAL_0, BINOP_1, FUNCT_1, ZFMISC_1, SUBSET_1, FUNCT_2, ORDINAL1,
XCMPLX_0, NAT_1, STRUCT_0, METRIC_1, PCOMPS_1, FRECHET, CARD_1, FINSEQ_2,
COMPLEX1, DBLSEQ_1, SRINGS_5, MESFUNC9, DOMAIN_1, LATTICE3, YELLOW_0,
YELLOW_1, WAYBEL_7, COMPTS_1, MCART_1, TOPS_1, SEQ_2, ORDERS_2, TOPMETR;
constructors RCOMP_1, YELLOW19, NAT_LAT, DICKSON, XXREAL_2, CARDFIL2, FRECHET,
YELLOW_8, COMPLEX1, DBLSEQ_1, SRINGS_5, TOPMETR, MESFUNC9, WAYBEL_7,
COMPTS_1, SIMPLEX0, TOPS_1, COMSEQ_2, SEQ_2;
registrations NUMBERS, VALUED_0, EUCLID, METRIC_1, YELLOW19, CARD_3, XBOOLE_0,
SUBSET_1, ORDINAL1, RELSET_1, FINSET_1, CARD_1, XREAL_0, NAT_1, MEMBERED,
XTUPLE_0, XXREAL_2, STRUCT_0, PCOMPS_1, FRECHET, BINOP_2, CARDFIL2,
XXREAL_0, TOPMETR, TOPS_1, LATTICE3, WAYBEL_0, YELLOW_1, WAYBEL_7,
WAYBEL_3, DICKSON, HAUSDORF;
requirements NUMERALS, SUBSET, BOOLE, REAL, ARITHM;
begin :: Preliminaries
reserve x for object,
X,Y,Z for set,
i,j,k,l,m,n for Nat,
r,s for Real,
no for Element of OrderedNAT,
A for Subset of [:NAT,NAT:];
theorem :: CARDFIL4:1
for W being finite Subset of X st X \ W c= Z holds
X \ Z is finite;
theorem :: CARDFIL4:2
Z c= X & X \ Z is finite implies
ex W being finite Subset of X st X \ W = Z;
theorem :: CARDFIL4:3 :: SRINGS_2:Lem 3
for X1,X2 being set, S1 be Subset-Family of X1, S2 be Subset-Family of X2
holds {s where s is Subset of [:X1,X2:]: ex s1,s2 be set st s1 in S1 &
s2 in S2 & s = [:s1,s2:]} is Subset-Family of [:X1,X2:];
theorem :: CARDFIL4:4
x in [:X,Y:] implies x is pair;
theorem :: CARDFIL4:5
0 < r implies ex m st m is non zero & 1 / m < r;
theorem :: CARDFIL4:6
for x,y being Point of RealSpace ex xr,yr being Real st x = xr & y = yr &
dist(x,y) = real_dist.(x,y) & dist(x,y) = (Pitag_dist 1).(<*x*>,<*y*>) &
dist(x,y) = |.xr - yr.|;
theorem :: CARDFIL4:7
for x,y being Point of TopSpaceMetr(Euclid 1)
ex x1,y1 being Point of RealSpace, xr,yr being Real st
x1 = xr & y1 = yr & x = <*xr*> & y = <*yr*> &
dist(x1,y1) = real_dist.(xr,yr) &
dist(x1,y1) = (Pitag_dist 1).(<*xr*>,<*yr*>) &
dist(x1,y1) = |.xr - yr.|;
theorem :: CARDFIL4:8
for x,y being Point of Euclid 1, r,s being Real st
x = <*r*> & y = <*s*> holds dist(x,y) = |.r - s.|;
registration
cluster [:NAT,NAT:] -> countable;
end;
registration
cluster [:NAT,NAT:] -> denumerable;
end;
theorem :: CARDFIL4:9
the set of all [0,n] where n is Nat is infinite;
theorem :: CARDFIL4:10
i <= k & j <= l implies [:Segm i,Segm j:] c= [:Segm k,Segm l:];
theorem :: CARDFIL4:11
[: NAT \ Segm m , NAT \ Segm n:] c= [:NAT,NAT:] \ [:Segm m,Segm n:];
theorem :: CARDFIL4:12
n = no & n <= m implies m in uparrow no;
theorem :: CARDFIL4:13
n = no & m in uparrow no implies n <= m;
theorem :: CARDFIL4:14
n = no implies uparrow no = NAT \ Segm n;
theorem :: CARDFIL4:15
proj1 A = {x where x is Element of NAT:
ex y being Element of NAT st [x,y] in A};
theorem :: CARDFIL4:16
proj2 A = {y where y is Element of NAT:
ex x being Element of NAT st [x,y] in A};
theorem :: CARDFIL4:17
for A being finite Subset of [:NAT,NAT:] holds
ex m,n st A c= [:Segm m,Segm n:];
theorem :: CARDFIL4:18
for X being non empty set, cF being Filter of X holds
cF is proper Filter of BoolePoset X;
theorem :: CARDFIL4:19
for X being non empty set, cF being Filter of X holds
ex cB being filter_base of X st cB = cF & <.cB.) = cF;
theorem :: CARDFIL4:20
for T being non empty TopSpace, cF being Filter of the carrier of T st
x in lim_filter cF holds x is_a_cluster_point_of cF,T;
theorem :: CARDFIL4:21
for B being Element of base_of_frechet_filter holds ex n st B = NAT \ Segm n;
theorem :: CARDFIL4:22
for B being Subset of NAT st B = NAT \ Segm n holds
B is Element of base_of_frechet_filter;
begin :: Cartesian Product of Two Filters
reserve X,Y,X1,X2 for non empty set,
cA1,cB1 for filter_base of X1,
cA2,cB2 for filter_base of X2,
cF1 for Filter of X1,
cF2 for Filter of X2,
cBa1 for basis of cF1,
cBa2 for basis of cF2;
definition
let X1,X2 be non empty set,
cB1 be filter_base of X1,
cB2 be filter_base of X2;
func [:cB1,cB2:] -> filter_base of [:X1,X2:] equals
:: CARDFIL4:def 1
the set of all [:B1,B2:] where B1 is Element of cB1,B2 is Element of cB2;
end;
theorem :: CARDFIL4:23
cF1 = <. cB1.) & cF1 = <. cA1.) &
cF2 = <. cB2.) & cF2 = <. cA2.) implies
<. [:cB1,cB2:] .) = <. [:cA1,cA2:] .);
theorem :: CARDFIL4:24
cBa1 = cB1 implies <.cB1.] = cF1;
theorem :: CARDFIL4:25
ex cB1 st <.cB1.) = cF1;
definition
let X1,X2 be non empty set, cF1 be Filter of X1,
cF2 be Filter of X2;
func <. cF1,cF2 .) -> Filter of [:X1,X2:] means
:: CARDFIL4:def 2
ex cB1 being filter_base of X1, cB2 being filter_base of X2 st
<.cB1.) = cF1 & <.cB2.) = cF2 & it = <. [:cB1,cB2:] .);
end;
definition
let X1,X2 be non empty set, cF1 be Filter of X1,
cF2 be Filter of X2, cB1 be basis of cF1, cB2 be basis of cF2;
func [: cB1,cB2 :] -> basis of <. cF1,cF2 .) means
:: CARDFIL4:def 3
ex cB3 being filter_base of X1, cB4 being filter_base of X2 st
cB1 = cB3 & cB2 = cB4 & it = [: cB3, cB4 :];
end;
definition
let n be Nat;
func square-uparrow n -> Subset of [:NAT,NAT:] means
:: CARDFIL4:def 4
for x being Element of [:NAT,NAT:] holds x in it iff
ex n1,n2 being Nat st n1 = x`1 & n2 = x`2 & n <= n1 & n <= n2;
end;
theorem :: CARDFIL4:26
[n,n] in square-uparrow n;
registration let n;
cluster square-uparrow n -> non empty;
end;
theorem :: CARDFIL4:27
[i,j] in square-uparrow n implies [i + k,j] in square-uparrow n &
[i,j + l] in square-uparrow n;
theorem :: CARDFIL4:28
square-uparrow n is infinite Subset of [:NAT,NAT:];
theorem :: CARDFIL4:29
no = n implies square-uparrow n = [:uparrow no,uparrow no:];
theorem :: CARDFIL4:30
m = n - 1 implies square-uparrow n c= [:NAT,NAT:] \ [:Seg m,Seg m:];
theorem :: CARDFIL4:31
square-uparrow n c= [:NAT,NAT:] \ [:Segm n,Segm n:];
theorem :: CARDFIL4:32
square-uparrow n = [:NAT \ Segm n, NAT \ Segm n:];
theorem :: CARDFIL4:33
ex n st square-uparrow n c= [:(NAT \ Segm i),(NAT \ Segm j):];
theorem :: CARDFIL4:34
n = max(i,j) implies
square-uparrow n c= square-uparrow i /\ square-uparrow j;
definition
let n be Nat;
func square-downarrow n -> Subset of [:NAT,NAT:] means
:: CARDFIL4:def 5
for x being Element of [:NAT,NAT:] holds x in it iff
ex n1,n2 being Nat st n1 = x`1 & n2 = x`2 & n1 < n & n2 < n;
end;
theorem :: CARDFIL4:35
square-downarrow n = [:Segm n,Segm n:];
theorem :: CARDFIL4:36
for A being finite Subset of [:NAT,NAT:] holds ex n st
A c= square-downarrow n;
theorem :: CARDFIL4:37
square-downarrow n is finite Subset of [:NAT,NAT:];
begin :: Comparaison between cartesian product of Frechet Filter on $\mathbb{N}$ and the Frechet Filter of $\mathbb{N}\times\mathbb{N}$
theorem :: CARDFIL4:38
for x being Element of [: base_of_frechet_filter,base_of_frechet_filter :]
holds ex i,j st x = [:NAT \ Segm i,NAT \ Segm j:];
theorem :: CARDFIL4:39
for x being Element of [: base_of_frechet_filter,base_of_frechet_filter :]
holds ex n st square-uparrow n c= x;
theorem :: CARDFIL4:40
[: base_of_frechet_filter,base_of_frechet_filter :] is
filter_base of [:NAT,NAT:];
theorem :: CARDFIL4:41
ex cB being basis of Frechet_Filter(NAT) st
cB = base_of_frechet_filter & [: cB, cB :] is
basis of <. Frechet_Filter(NAT),Frechet_Filter(NAT) .);
definition
func all-square-uparrow -> filter_base of [:NAT,NAT:] equals
:: CARDFIL4:def 6
the set of all square-uparrow n where n is Nat;
end;
theorem :: CARDFIL4:42
all-square-uparrow, [: base_of_frechet_filter,base_of_frechet_filter :]
are_equivalent_generators;
theorem :: CARDFIL4:43
<. [: base_of_frechet_filter,base_of_frechet_filter :] .)
= <. Frechet_Filter(NAT),Frechet_Filter(NAT).);
theorem :: CARDFIL4:44
<. all-square-uparrow .)
= <. Frechet_Filter(NAT),Frechet_Filter(NAT).);
theorem :: CARDFIL4:45
<. Frechet_Filter(NAT),Frechet_Filter(NAT).)
is_filter-finer_than Frechet_Filter([:NAT,NAT:]);
theorem :: CARDFIL4:46
([:NAT,NAT:] \ the set of all [0,n] where n is Nat)
in <. Frechet_Filter(NAT),Frechet_Filter(NAT).) &
not ([:NAT,NAT:] \ the set of all [0,n] where n is Nat)
in Frechet_Filter([:NAT,NAT:]);
theorem :: CARDFIL4:47
Frechet_Filter([:NAT,NAT:]) <> <. Frechet_Filter(NAT),Frechet_Filter(NAT).);
begin :: Topological space and double sequence
reserve T for non empty TopSpace,
s for Function of [:NAT,NAT:], the carrier of T,
M for Subset of the carrier of T;
reserve cF3,cF4 for Filter of the carrier of T;
theorem :: CARDFIL4:48
cF4 is_filter-finer_than cF3 implies lim_filter cF3 c= lim_filter cF4;
theorem :: CARDFIL4:49
for f being Function of X,Y, cFXa,cFXb being Filter of X st
cFXb is_filter-finer_than cFXa holds
filter_image(f,cFXb) is_filter-finer_than filter_image(f,cFXa);
theorem :: CARDFIL4:50
s"(M) in Frechet_Filter([:NAT,NAT:]) iff
ex A being finite Subset of [:NAT,NAT:] st s"(M) = [:NAT,NAT:] \ A;
theorem :: CARDFIL4:51
s"(M) in <. Frechet_Filter(NAT),Frechet_Filter(NAT).) iff
ex n st square-uparrow n c= s"(M);
theorem :: CARDFIL4:52
filter_image(s,Frechet_Filter([:NAT,NAT:])) = {M where M is Subset of
the carrier of T: ex A being finite Subset of [:NAT,NAT:] st
s"(M) = [:NAT,NAT:] \ A};
theorem :: CARDFIL4:53
filter_image(s,<. Frechet_Filter(NAT),Frechet_Filter(NAT).)) =
{M where M is Subset of the carrier of T: ex n being Nat st
square-uparrow n c= s"(M)};
theorem :: CARDFIL4:54
for x being Point of T holds
x in lim_filter(s,Frechet_Filter([:NAT,NAT:])) iff
for A being a_neighborhood of x holds
ex B being finite Subset of [:NAT,NAT:] st s"(A) = [:NAT,NAT:] \ B;
theorem :: CARDFIL4:55
for x being Point of T holds
x in lim_filter(s,Frechet_Filter([:NAT,NAT:])) iff
for A being a_neighborhood of x holds [:NAT,NAT:] \ s"(A) is finite;
theorem :: CARDFIL4:56
for x being Point of T holds
x in lim_filter(s,<. Frechet_Filter(NAT),Frechet_Filter(NAT).)) iff
for A being a_neighborhood of x holds ex n being Nat st
square-uparrow n c= s"(A);
theorem :: CARDFIL4:57
for x being Point of T, cB being basis of BOOL2F NeighborhoodSystem x holds
x in lim_filter(s,<. Frechet_Filter(NAT),Frechet_Filter(NAT).)) iff
for B being Element of cB holds ex n being Nat st square-uparrow n c= s"(B);
theorem :: CARDFIL4:58
for x being Point of T, cB being basis of BOOL2F NeighborhoodSystem x holds
x in lim_filter(s,Frechet_Filter([:NAT,NAT:])) iff
for B being Element of cB holds ex A being finite Subset of [:NAT,NAT:] st
s"(B) = [:NAT,NAT:] \ A;
theorem :: CARDFIL4:59
for x being Point of T, cB being basis of BOOL2F NeighborhoodSystem x holds
x in lim_filter(s,<. Frechet_Filter(NAT),Frechet_Filter(NAT).)) iff
for B being Element of cB holds ex n being Nat st s.:(square-uparrow n) c= B;
theorem :: CARDFIL4:60
for x being Point of T, cB being basis of BOOL2F NeighborhoodSystem x holds
x in lim_filter(s,Frechet_Filter([:NAT,NAT:])) iff
for B being Element of cB holds ex A being finite Subset of [:NAT,NAT:] st
s.:([:NAT,NAT:] \ A) c= B;
theorem :: CARDFIL4:61
for x being Point of T, cB being basis of BOOL2F NeighborhoodSystem x holds
x in lim_filter(s,Frechet_Filter([:NAT,NAT:])) iff for B being Element of cB
holds ex n,m st s.:([:NAT,NAT:] \ [:Segm n,Segm m:]) c= B;
theorem :: CARDFIL4:62
x in s.:(square-uparrow n) iff ex i,j st n <= i & n <= j & x = s.(i,j);
theorem :: CARDFIL4:63
x in s.:([:NAT,NAT:] \ [:Segm i,Segm j:]) iff ex n,m being Nat st
(i <= n or j <= m) & x = s.(n,m);
theorem :: CARDFIL4:64
for x being Point of T, cB being basis of BOOL2F NeighborhoodSystem x holds
x in lim_filter(s,<. Frechet_Filter(NAT),Frechet_Filter(NAT).)) iff
for B being Element of cB holds ex n being Nat st for n1,n2 being Nat st
n <= n1 & n <= n2 holds s.(n1,n2) in B;
theorem :: CARDFIL4:65
for x being Point of T, cB being basis of BOOL2F NeighborhoodSystem x holds
x in lim_filter(s,Frechet_Filter([:NAT,NAT:])) iff
for B being Element of cB holds ex i,j st for m,n st i <= m or j <= n holds
s.(m,n) in B;
theorem :: CARDFIL4:66
lim_filter(s,Frechet_Filter([:NAT,NAT:])) c=
lim_filter(s,<. all-square-uparrow.));
begin :: Metric space and double sequence
theorem :: CARDFIL4:67
for M being non empty MetrSpace, p being Point of M,
x being Point of TopSpaceMetr(M),
s being Function of [:NAT,NAT:], TopSpaceMetr(M) st x = p holds
x in lim_filter(s,<. Frechet_Filter(NAT),Frechet_Filter(NAT).)) iff
for m being non zero Nat ex n being Nat st for n1,n2 being Nat st
n <= n1 & n <= n2 holds
s.(n1,n2) in {q where q is Point of M: dist(p,q) < 1/m};
theorem :: CARDFIL4:68
for M being non empty MetrSpace, p being Point of M,
x being Point of TopSpaceMetr(M),
s being Function of [:NAT,NAT:], TopSpaceMetr(M),
s2 being Function of [:NAT,NAT:], M st
x = p & s = s2 holds
x in lim_filter(s,<. Frechet_Filter(NAT),Frechet_Filter(NAT).)) iff
for m being non zero Nat ex n being Nat st for n1,n2 being Nat st
n <= n1 & n <= n2 holds s2.(n1,n2) in
{q where q is Point of M: dist(p,q) < 1/m};
begin :: One-dimensional Euclidean metric space and double sequence
reserve Rseq for Function of [:NAT,NAT:],REAL;
theorem :: CARDFIL4:69
for x being Point of TopSpaceMetr(Euclid 1),
y being Point of Euclid 1,
cB being basis of BOOL2F NeighborhoodSystem x,
b being Element of cB st x = y & cB = Balls(x) holds
ex n being Nat
st b = {q where q is Element of Euclid 1: dist(y,q) < 1/n};
definition
let s be Function of [:NAT,NAT:],REAL;
func #s -> Function of [:NAT,NAT:],R^1 equals
:: CARDFIL4:def 7
s;
end;
theorem :: CARDFIL4:70
for s being Function of [:NAT,NAT:],TopSpaceMetr(Euclid 1),
y being Point of Euclid 1 holds (s.:(square-uparrow n)
c= {q where q is Element of Euclid 1: dist(y,q) < 1/m}) iff
(for x being object st x in s.:(square-uparrow n) holds
ex rx,ry being Real st x = <*rx*> & y = <*ry*> & |.ry - rx.| < 1/m);
theorem :: CARDFIL4:71
r in lim_filter( #Rseq , <. Frechet_Filter(NAT),Frechet_Filter(NAT).))
iff (for m being non zero Nat ex n being Nat st for n1,n2 being Nat st
n <= n1 & n <= n2 holds |. Rseq.(n1,n2) - r .| < 1/m);
begin :: Basic relations convergence in Pringsheim's sense and filter convergence
theorem :: CARDFIL4:72
lim_filter( #Rseq,<. Frechet_Filter(NAT),Frechet_Filter(NAT).)) <> {}
implies ex x being Real st
lim_filter( #Rseq,<. Frechet_Filter(NAT),Frechet_Filter(NAT).)) = {x};
theorem :: CARDFIL4:73
Rseq is P-convergent implies P-lim Rseq in
lim_filter( #Rseq,<. Frechet_Filter(NAT),Frechet_Filter(NAT).));
theorem :: CARDFIL4:74
Rseq is P-convergent iff
lim_filter( #Rseq,<. Frechet_Filter(NAT),Frechet_Filter(NAT).)) <> {};
theorem :: CARDFIL4:75
Rseq is P-convergent implies {P-lim Rseq} =
lim_filter( #Rseq,<. Frechet_Filter(NAT),Frechet_Filter(NAT).));
theorem :: CARDFIL4:76
lim_filter( #Rseq,<. Frechet_Filter(NAT),Frechet_Filter(NAT).)) is
non empty implies Rseq is P-convergent & {P-lim Rseq} =
lim_filter( #Rseq,<. Frechet_Filter(NAT),Frechet_Filter(NAT).));
begin :: Example: double sequence converges in Pringsheim's sense but not in Frechet Filter of $\mathbb{N}\times\mathbb{N}$'s sense
definition
func dblseq_ex_1 -> Function of [:NAT,NAT:],REAL means
:: CARDFIL4:def 8
for m,n being Nat holds it.(m,n) = 1 / (m + 1);
end;
theorem :: CARDFIL4:77
for m being non zero Nat ex n being Nat st for n1,n2 being Nat st
n <= n1 & n <= n2 holds |. dblseq_ex_1.(n1,n2) - 0 .| < 1/m;
theorem :: CARDFIL4:78
0 in lim_filter( # dblseq_ex_1,<. Frechet_Filter(NAT),Frechet_Filter(NAT).));
theorem :: CARDFIL4:79
lim_filter( #dblseq_ex_1,Frechet_Filter([:NAT,NAT:])) = {};
theorem :: CARDFIL4:80
lim_filter( #dblseq_ex_1,<. Frechet_Filter(NAT),Frechet_Filter(NAT).))
<> lim_filter( #dblseq_ex_1,Frechet_Filter([:NAT,NAT:]));
begin :: Correspondence with some definitions of the article DBLSEQ_1
definition
let X1,X2 be non empty set,
cF1 be Filter of X1,
Y be Hausdorff non empty TopSpace,
f be Function of [:X1,X2:], Y;
assume
for x being Element of X2 holds lim_filter(ProjMap2(f,x),cF1) <> {};
func lim_in_cod1(f,cF1) -> Function of X2,Y means
:: CARDFIL4:def 9
(for x being Element of X2 holds {it.x} = lim_filter(ProjMap2(f,x),cF1));
end;
definition
let X1,X2 be non empty set,
cF2 be Filter of X2,
Y be Hausdorff non empty TopSpace,
f be Function of [:X1,X2:],Y;
assume
for x being Element of X1 holds lim_filter(ProjMap1(f,x),cF2) <> {};
func lim_in_cod2(f,cF2) -> Function of X1,Y means
:: CARDFIL4:def 10
(for x being Element of X1 holds {it.x} = lim_filter(ProjMap1(f,x),cF2));
end;
theorem :: CARDFIL4:81
for f being Function of X,REAL holds f is Function of X, R^1;
theorem :: CARDFIL4:82
for s being sequence of REAL holds s is Function of NAT, R^1;
reserve f for Function of [#]OrderedNAT,R^1,
seq for Function of NAT,REAL;
theorem :: CARDFIL4:83
f = seq & lim_f f <> {} implies seq is convergent & ex z being Real
st z in lim_f f & for p being Real st 0 < p holds ex n being Nat st
for m being Nat st n <= m holds |.seq.m - z.| < p;
theorem :: CARDFIL4:84
f = seq & lim_f f <> {} implies lim_f f = {lim seq};
theorem :: CARDFIL4:85
for f being Function of [#]OrderedNAT,T for s being sequence of T st
f = s holds lim_f f = lim_f s;
theorem :: CARDFIL4:86
for f being Function of [#]OrderedNAT,T for g being Function of NAT,T st
f = g holds lim_f f = lim_f g;
theorem :: CARDFIL4:87
for f being Function of NAT,R^1 st f = seq & lim_f f <> {} holds
lim_f f = {lim seq};
theorem :: CARDFIL4:88
(for x being Element of NAT holds
lim_filter(ProjMap2( #Rseq ,x),Frechet_Filter(NAT)) <> {})
iff
Rseq is convergent_in_cod1;
theorem :: CARDFIL4:89
(for x being Element of NAT holds
lim_filter(ProjMap1( #Rseq ,x),Frechet_Filter(NAT)) <> {})
iff
Rseq is convergent_in_cod2;
theorem :: CARDFIL4:90
for t being Element of NAT, f being Function of [:NAT,NAT:],R^1
for seq being Function of [:NAT,NAT:],REAL st f = seq &
(for x being Element of NAT holds
lim_filter(ProjMap1(f,x),Frechet_Filter(NAT)) <> {}) holds
lim_filter(ProjMap1(f,t),Frechet_Filter(NAT)) = {lim ProjMap1(seq,t)};
theorem :: CARDFIL4:91
for t being Element of NAT, f being Function of [:NAT,NAT:],R^1
for seq being Function of [:NAT,NAT:],REAL st f = seq &
(for x being Element of NAT holds
lim_filter(ProjMap2(f,x),Frechet_Filter(NAT)) <> {}) holds
lim_filter(ProjMap2(f,t),Frechet_Filter(NAT)) = {lim ProjMap2(seq,t)};
theorem :: CARDFIL4:92
for Y being Hausdorff non empty TopSpace,
f being Function of [:NAT,NAT:],Y st (for x being Element of NAT holds
lim_filter(ProjMap2(f,x),Frechet_Filter(NAT)) <> {}) & f = Rseq &
Y = R^1 holds
lim_in_cod1(f,Frechet_Filter(NAT)) = lim_in_cod1 Rseq;
theorem :: CARDFIL4:93
for Y being non empty Hausdorff TopSpace,
f being Function of [:NAT,NAT:],Y st
(for x being Element of NAT holds
lim_filter(ProjMap1(f,x),Frechet_Filter(NAT)) <> {}) & f = Rseq & Y = R^1
holds
lim_in_cod2(f,Frechet_Filter(NAT)) = lim_in_cod2 Rseq;
begin :: Regular space, double limit and iterated limit
reserve Y for non empty TopSpace,
x for Point of Y,
f for Function of [:X1,X2:],Y;
theorem :: CARDFIL4:94
x in lim_filter(f,<.cF1,cF2.)) & <.cB1.) = cF1 & <.cB2.) = cF2
implies for V being Subset of Y st V is open & x in V holds
ex B1 being Element of cB1, B2 being Element of cB2 st f.:([:B1,B2:]) c= V;
theorem :: CARDFIL4:95
x in lim_filter(f,<.cF1,cF2.)) & <.cB1.) = cF1 & <.cB2.) = cF2
implies for U being a_neighborhood of x st U is closed holds
ex B1 being Element of cB1, B2 being Element of cB2 st
f.:([:B1,B2:]) c= Int(U);
theorem :: CARDFIL4:96
x in lim_filter(f,<.cF1,cF2.)) & <.cB1.) = cF1 & <.cB2.) = cF2 implies
for U being a_neighborhood of x st U is closed holds
ex B1 being Element of cB1, B2 being Element of cB2 st
for y being Element of B1 holds f.:([:{y},B2:]) c= Int(U);
theorem :: CARDFIL4:97
x in lim_filter(f,<.cF1,cF2.)) & <.cB1.) = cF1 & <.cB2.) = cF2 implies
for U being a_neighborhood of x st U is closed holds
ex B1 being Element of cB1, B2 being Element of cB2 st
for z being Element of X1, y being Element of Y st
z in B1 & y in lim_filter(ProjMap1(f,z),cF2) holds
y in Cl Int U;
theorem :: CARDFIL4:98
x in lim_filter(f,<.cF1,cF2.)) & <.cB1.) = cF1 & <.cB2.) = cF2
implies for U being a_neighborhood of x st U is closed holds
ex B1 being Element of cB1, B2 being Element of cB2 st
for z being Element of X2, y being Element of Y st z in B2 &
y in lim_filter(ProjMap2(f,z),cF1) holds y in Cl Int U;
theorem :: CARDFIL4:99
for Y being Hausdorff regular non empty TopSpace,
f being Function of [:X1,X2:],Y st (for x being Element of X2 holds
lim_filter(ProjMap2(f,x),cF1) <> {}) holds
lim_filter(f,<.cF1,cF2.)) c= lim_filter(lim_in_cod1(f,cF1),cF2);
theorem :: CARDFIL4:100
for Y being Hausdorff regular non empty TopSpace,
f being Function of [:X1,X2:],Y st (for x being Element of X1 holds
lim_filter(ProjMap1(f,x),cF2) <> {}) holds
lim_filter(f,<.cF1,cF2.)) c= lim_filter(lim_in_cod2(f,cF2),cF1);
theorem :: CARDFIL4:101
for X1,X2 being non empty set,
cF1 being Filter of X1,
cF2 being Filter of X2,
Y being Hausdorff regular non empty TopSpace,
f being Function of [:X1,X2:],Y st
lim_filter(f,<.cF1,cF2.)) <> {} &
(for x being Element of X1 holds lim_filter(ProjMap1(f,x),cF2) <> {})
holds lim_filter(f,<.cF1,cF2.)) = lim_filter(lim_in_cod2(f,cF2),cF1);
theorem :: CARDFIL4:102
for X1,X2 being non empty set,
cF1 being Filter of X1,
cF2 being Filter of X2,
Y being Hausdorff regular non empty TopSpace,
f being Function of [:X1,X2:],Y st
lim_filter(f,<.cF1,cF2.)) <> {} &
(for x being Element of X2 holds lim_filter(ProjMap2(f,x),cF1) <> {})
holds lim_filter(f,<.cF1,cF2.)) = lim_filter(lim_in_cod1(f,cF1),cF2);
theorem :: CARDFIL4:103
for X1,X2 being non empty set,
cF1 being Filter of X1,
cF2 being Filter of X2,
Y being Hausdorff regular non empty TopSpace,
f being Function of [:X1,X2:],Y
st lim_filter(f,<.cF1,cF2.)) <> {} &
(for x being Element of X1 holds lim_filter(ProjMap1(f,x),cF2) <> {}) &
(for x being Element of X2 holds lim_filter(ProjMap2(f,x),cF1) <> {})
holds
lim_filter(lim_in_cod2(f,cF2),cF1)
= lim_filter(lim_in_cod1(f,cF1),cF2);