:: Double Sequences and Iterated Limits in Regular Space
:: by Roland Coghetto
::
:: Received June 30, 2016
:: Copyright (c) 2016-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 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;
definitions CARDFIL2, TARSKI, XBOOLE_0;
equalities DICKSON, CARDFIL2, METRIC_1, PCOMPS_1, TOPMETR, EUCLID;
expansions XTUPLE_0, CARDFIL2, TARSKI, XBOOLE_0, DBLSEQ_1;
theorems TARSKI, XREAL_0, BINOP_1, FINSEQ_2, PCOMPS_1, SRINGS_5, COMPLEX1,
FRECHET, RELAT_1, FUNCT_2, CARDFIL3, YELLOW19, COMBGRAS, CARD_1, FUNCT_1,
XBOOLE_1, CARD_4, STIRL2_1, ORDINAL1, CARDFIL2, ZFMISC_1, SRINGS_2,
XBOOLE_0, SETFAM_1, XTUPLE_0, FINSEQ_1, XXREAL_0, XREAL_1, NAT_1,
XXREAL_2, METRIC_1, SEQ_4, XCMPLX_1, DBLSEQ_1, ABSVALUE, XXREAL_1,
MESFUNC9, WAYBEL_7, FCONT_3, CONNSP_2, CARD_FIL, TOPS_1, LATTICE3,
YELLOW_1, STRUCT_0, YELLOW_8, PRE_TOPC, SEQ_2, WAYBEL_0;
schemes FUNCT_1, FUNCT_2, SUBSET_1;
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 Th1:
for W being finite Subset of X st X \ W c= Z holds
X \ Z is finite
proof
let W be finite Subset of X;
assume X \ W c= Z;
then X \ Z c= (X \ (X \ W)) by XBOOLE_1:34;
then X \ Z c= X /\ W by XBOOLE_1:48;
hence thesis;
end;
theorem Th2:
Z c= X & X \ Z is finite implies
ex W being finite Subset of X st X \ W = Z
proof
assume that
A1: Z c= X and
A2: X \ Z is finite;
X \ (X \ Z) = X /\ Z by XBOOLE_1:48
.= Z by A1,XBOOLE_1:17,XBOOLE_1:19;
hence thesis by A2;
end;
theorem Th3: :: 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:]
proof
let X1,X2 be set, S1 be Subset-Family of X1, S2 be Subset-Family of X2;
set S = {s where s is Subset of [:X1,X2:]:
ex s1,s2 be set st s1 in S1 & s2 in S2 & s=[:s1,s2:]};
S c= bool [:X1,X2:]
proof
let x be object;
assume x in S;
then consider s0 be Subset of [:X1,X2:] such that
A1: x=s0 & ex s1,s2 be set st s1 in S1 & s2 in S2 & s0=[:s1,s2:];
thus thesis by A1;
end;
hence thesis;
end;
theorem Th4:
x in [:X,Y:] implies x is pair
proof
assume x in [:X,Y:];
then ex a,b be object st a in X & b in Y & x = [a,b] by ZFMISC_1:def 2;
hence thesis;
end;
theorem Th5:
0 < r implies ex m st m is non zero & 1 / m < r
proof
assume
A1: 0 < r;
consider m be Nat such that
A2: 1/r < m by SEQ_4:3;
A3: 0 < m by A1,A2;
take m;
thus m is non zero by A1,A2;
1/r*r < m*r by A2,A1,XREAL_1:68;
then 1 < m*r by A1,XCMPLX_1:106;
then 1/m < m*r/m by A3,XREAL_1:74;
then 1/m < r*(m/m) by XCMPLX_1:74;
hence thesis by A3,XCMPLX_1:88;
end;
theorem Th6:
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.|
proof
let x,y be Point of RealSpace;
reconsider xr = x,yr = y as Real;
A1: real_dist.(x,y) = |.xr - yr.| by METRIC_1:def 12;
reconsider x2 = <*xr*>,y2 = <*yr*> as Element of REAL 1;
x2.1 = xr & y2.1 = yr by FINSEQ_1:def 8;
then (Pitag_dist 1).(<*x*>,<*y*>) = |. xr - yr .| by SRINGS_5:99;
hence thesis by A1;
end;
theorem Th7:
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.|
proof
let x,y be Point of TopSpaceMetr(Euclid 1);
reconsider xr1 = x as Point of Euclid 1;
xr1 in 1-tuples_on REAL;
then xr1 in the set of all <*r*> where r is Element of REAL by FINSEQ_2:96;
then consider r1 be Element of REAL such that
A1: xr1 = <*r1*>;
reconsider yr1 = y as Point of Euclid 1;
yr1 in 1-tuples_on REAL;
then yr1 in the set of all <*r*> where r is Element of REAL by FINSEQ_2:96;
then consider r2 be Element of REAL such that
A2: yr1 = <*r2*>;
reconsider xr2 = r1,yr2 = r2 as Element of RealSpace;
reconsider x2 = <*r1*>,y2 = <*r2*> as Element of REAL 1;
A3: x2.1 = r1 by FINSEQ_1:def 8;
A4: (Pitag_dist 1).(<*r1*>,<*r2*>) = |.x2.1-y2.1.| by SRINGS_5:99
.= |. r1 - r2 .| by A3,FINSEQ_1:def 8;
take xr2,yr2;
take r1,r2;
thus thesis by A4,A1,A2,METRIC_1:def 12;
end;
theorem Th8:
for x,y being Point of Euclid 1, r,s being Real st
x = <*r*> & y = <*s*> holds dist(x,y) = |.r - s.|
proof
let x,y be Point of Euclid 1,r,s be Real;
assume that
A1: x = <*r*> and
A2: y = <*s*>;
consider x1,y1 being Point of RealSpace, xr,yr being Real such that
x1 = xr and
y1 = yr and
A3: x = <*xr*> and
A4: y = <*yr*> and
dist(x1,y1) = real_dist.(xr,yr) and
A5: dist(x1,y1) = (Pitag_dist 1).(<*xr*>,<*yr*>) and
A6: dist(x1,y1) = |.xr - yr.| by Th7;
xr = r & yr = s by A3,A1,A2,A4,FINSEQ_1:76;
hence thesis by A5,A6,A3,A4;
end;
registration
cluster [:NAT,NAT:] -> countable;
coherence by CARD_4:7;
end;
registration
cluster [:NAT,NAT:] -> denumerable;
coherence;
end;
theorem Th9:
the set of all [0,n] where n is Nat is infinite
proof
deffunc F(object) = [0,$1];
consider f be Function such that
A1: dom f = NAT and
A2: for x be object st x in NAT holds f.x = F(x) from FUNCT_1:sch 3;
A3: f is one-to-one
proof
now
let x,y be object; assume that
A4: x in dom f and
A5: y in dom f and
A6: f.x = f.y;
f.y = [0,y] by A5,A1,A2;
then [0,x] = [0,y] by A6,A4,A1,A2;
hence x = y by XTUPLE_0:1;
end;
hence thesis by FUNCT_1:def 4;
end;
rng f = the set of all [0,n] where n is Nat
proof
A7: rng f c= the set of all [0,n] where n is Nat
proof
let x be object;
assume x in rng f;
then consider y be object such that
A8: y in dom f and
A9: x = f.y by FUNCT_1:def 3;
reconsider z = y as Nat by A8,A1;
x = [0,z] by A9,A2,A1,A8;
hence thesis;
end;
the set of all [0,n] where n is Nat c= rng f
proof
let x be object;
assume x in the set of all [0,n] where n is Nat;
then consider n such that
A10: x = [0,n];
n in dom f & f.n = [0,n] by A1,A2,ORDINAL1:def 12;
hence thesis by A10,FUNCT_1:3;
end;
hence thesis by A7;
end;
hence thesis by A1,A3,CARD_1:59;
end;
theorem
i <= k & j <= l implies [:Segm i,Segm j:] c= [:Segm k,Segm l:]
proof
assume that
A1: i <= k and
A2: j <= l;
now
let x be object;
assume x in [:Segm i,Segm j:];
then consider xi,xj be object such that
A3: xi in Segm i and
A4: xj in Segm j and
A5: x = [xi,xj] by ZFMISC_1:def 2;
reconsider xi,xj as Nat by A3,A4;
xi < k & xj < l by A1,A2,A3,A4,NAT_1:44,XXREAL_0:2;
then xi in Segm k & xj in Segm l by NAT_1:44;
hence x in [:Segm k,Segm l:] by A5,ZFMISC_1:def 2;
end;
hence thesis;
end;
theorem Th10:
[: NAT \ Segm m , NAT \ Segm n:] c= [:NAT,NAT:] \ [:Segm m,Segm n:]
proof
A1: [:NAT,NAT:] \ [:Segm m,Segm n:] =
[:NAT \ Segm m,NAT:] \/ [:NAT,NAT \ Segm n:] by ZFMISC_1:103;
[: NAT \ Segm m , NAT \ Segm n:] =
[:NAT \ Segm m,NAT:] \ [:NAT \ Segm m,Segm n:] by ZFMISC_1:102;
hence thesis by A1,XBOOLE_1:10;
end;
theorem Th11:
n = no & n <= m implies m in uparrow no
proof
assume that
A1: no = n and
A2: n <= m;
reconsider m as Element of NAT by ORDINAL1:def 12;
reconsider p0 = no as Element of NAT;
m in {x where x is Element of NAT:ex p0 be Element of NAT st
no = p0 & p0 <= x} by A1,A2;
hence thesis by CARDFIL2:50;
end;
theorem Th12:
n = no & m in uparrow no implies n <= m
proof
assume that
A1: n = no and
A2: m in uparrow no;
m in {x where x is Element of NAT:ex p0 be Element of NAT st no = p0 &
p0 <= x} by A2,CARDFIL2:50;
then ex x be Element of NAT st m = x & ex p0 be Element of NAT st
no = p0 & p0 <= x;
hence thesis by A1;
end;
theorem Th13:
n = no implies uparrow no = NAT \ Segm n
proof
assume
A1: n = no;
A2: uparrow no c= NAT \ Segm n
proof
let x be object;
assume
A3: x in uparrow no;
then x in {x where x is Element of NAT:ex p0 be Element of NAT st
no = p0 & p0 <= x} by CARDFIL2:50;
then ex y be Element of NAT st y = x & ex p0 be Element of NAT st
no = p0 & p0 <= y;
then reconsider y = x as Element of NAT;
not y in Segm n by A1,A3,Th12,NAT_1:44;
hence thesis by XBOOLE_0:def 5;
end;
NAT \ Segm n c= uparrow no
proof
let x be object;
assume
A4: x in NAT \ Segm n; then
A5: x in NAT & not x in Segm n by XBOOLE_0:def 5;
reconsider y = x as Element of NAT by A4;
reconsider n1 = n as Element of NAT by ORDINAL1:def 12;
n1 <= y & n1 = no by A1,A5,NAT_1:44;
then y in {x where x is Element of NAT:ex p0 be Element of NAT st
no = p0 & p0 <= x};
hence thesis by CARDFIL2:50;
end;
hence thesis by A2;
end;
theorem Th14:
proj1 A = {x where x is Element of NAT:
ex y being Element of NAT st [x,y] in A}
proof
set A1 = {x where x is Element of NAT:
ex y being Element of NAT st [x,y] in A};
A1: proj1 A c= A1
proof
let x be object;
assume x in proj1 A;
then consider y be object such that
A2: [x,y] in A by XTUPLE_0:def 12;
ex x1,y1 be object st x1 in NAT & y1 in NAT & [x,y] = [x1,y1]
by A2,ZFMISC_1:def 2;
then reconsider x,y as Element of NAT by XTUPLE_0:1;
[x,y] in A & y is Element of NAT by A2;
hence thesis;
end;
A1 c= proj1 A
proof
let x be object;
assume x in A1;
then ex x1 be Element of NAT st x = x1 & ex y be Element of NAT st
[x1,y] in A;
hence thesis by XTUPLE_0:def 12;
end;
hence thesis by A1;
end;
theorem Th15:
proj2 A = {y where y is Element of NAT:
ex x being Element of NAT st [x,y] in A}
proof
set A2 = {y where y is Element of NAT: ex x being Element of NAT st
[x,y] in A};
A1: proj2 A c= A2
proof
let y be object;
assume y in proj2 A;
then consider x be object such that
A2: [x,y] in A by XTUPLE_0:def 13;
ex x1,y1 be object st x1 in NAT & y1 in NAT & [x,y] = [x1,y1]
by A2,ZFMISC_1:def 2;
then reconsider x,y as Element of NAT by XTUPLE_0:1;
[x,y] in A & y is Element of NAT by A2;
hence thesis;
end;
A2 c= proj2 A
proof
let y be object;
assume y in A2;
then ex y1 be Element of NAT st y = y1 & ex x be Element of NAT st
[x,y1] in A;
hence thesis by XTUPLE_0:def 13;
end;
hence thesis by A1;
end;
theorem Th16:
for A being finite Subset of [:NAT,NAT:] holds
ex m,n st A c= [:Segm m,Segm n:]
proof
let A be finite Subset of [:NAT,NAT:];
per cases;
suppose A is empty;
then A c= [:Segm 0,Segm 0:];
hence thesis;
end;
suppose
A1: A is non empty;
set A1 = {x where x is Element of NAT: ex y be Element of NAT st
[x,y] in A};
A2: A1 is non empty
proof
set n = the Element of A;
n in A by A1; then
consider x,y be object such that
A3: x in NAT and
A4: y in NAT and
A5: n = [x,y] by ZFMISC_1:def 2;
reconsider x,y as Element of NAT by A3,A4;
x in A1 by A4,A5,A1;
hence thesis;
end;
A1 c= NAT
proof
let t be object;
assume t in A1;
then ex x be Element of NAT st t = x & ex y be Element of NAT st
[x,y] in A;
hence thesis;
end;
then reconsider B1 = A1 as non empty ext-real-membered set by A2;
reconsider A as Relation;
proj1 A is finite;
then B1 is finite by Th14;
then sup B1 in A1 by XXREAL_2:def 6;
then consider x1 be Element of NAT such that
A6: sup B1 = x1 and
ex y be Element of NAT st [x1,y] in A;
set A2 = {y where y is Element of NAT: ex x be Element of NAT st
[x,y] in A};
A7: A2 is non empty
proof
set n = the Element of A;
n in A by A1; then
consider x,y be object such that
A8: x in NAT and
A9: y in NAT and
A10: n = [x,y] by ZFMISC_1:def 2;
reconsider x,y as Element of NAT by A8,A9;
y in A2 by A8,A10,A1;
hence thesis;
end;
A2 c= NAT
proof
let t be object;
assume t in A2;
then ex y be Element of NAT st t = y & ex x be Element of NAT st
[x,y] in A;
hence thesis;
end;
then reconsider B2 = A2 as non empty ext-real-membered set by A7;
reconsider A as Relation;
proj2 A is finite;
then B2 is finite by Th15;
then sup B2 in A2 by XXREAL_2:def 6;
then consider y1 be Element of NAT such that
A11: sup B2 = y1 and
ex x be Element of NAT st [x,y1] in A;
A c= [:Segm (x1+1),Segm (y1+1):]
proof
let t be object;
assume
A12: t in A;
then reconsider u = t as Element of [:NAT,NAT:];
consider x,y be object such that
A13: x in NAT and
A14: y in NAT and
A15: u = [x,y] by ZFMISC_1:def 2;
reconsider x2 = x, y2 = y as Element of NAT by A13,A14;
x2 in A1 by A12,A14,A15;
then x2 <= sup B1 by XXREAL_2:4;
then x2 < x1 + 1 by A6,NAT_1:13; then
A16: x2 in Segm (x1+1) by NAT_1:44;
y2 in A2 by A12,A13,A15;
then y2 <= sup B2 by XXREAL_2:4;
then y2 < y1 + 1 by A11,NAT_1:13;
then y2 in Segm (y1+1) by NAT_1:44;
hence thesis by A16,A15,ZFMISC_1:def 2;
end;
hence thesis;
end;
end;
theorem Th17:
for X being non empty set, cF being Filter of X holds
cF is proper Filter of BoolePoset X
proof
let X be non empty set,cF be Filter of X;
reconsider cF as non empty Subset of BooleLatt X by LATTICE3:def 1;
reconsider cF as Filter of BoolePoset X by CARDFIL2:73,CARDFIL2:75;
not {} in cF by CARD_FIL:def 1;
then not Bottom BoolePoset X in cF by YELLOW_1:18;
hence thesis by WAYBEL_7:4;
end;
theorem Th18:
for X being non empty set, cF being Filter of X holds
ex cB being filter_base of X st cB = cF & <.cB.) = cF
proof
let X be non empty set, cF be Filter of X;
cF is basis of cF by CARDFIL2:13;
then reconsider cB = cF as filter_base of X by CARDFIL2:29;
take cB;
now
hereby
let x be object;
assume
A1: x in <.cB.);
then reconsider y = x as Subset of X;
ex b be Element of cB st b c= y by A1,CARDFIL2:def 8;
hence x in cF by CARD_FIL:def 1;
end;
let x be object;
assume x in cF;
hence x in <.cB.) by CARDFIL2:def 8;
end;
then <.cB.) c= cF & cF c= <.cB.);
hence thesis;
end;
theorem Th19:
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
proof
let T be non empty TopSpace, cF be Filter of the carrier of T;
assume
A1: x in lim_filter cF;
now
let A be Subset of T;
assume that
A2: A is open and
A3: x in A;
A4: A in cF by A1,A3,A2,CARDFIL2:80,WAYBEL_7:def 5;
not {} in cF by CARD_FIL:def 1;
hence for B be set st B in cF holds A meets B by A4,CARD_FIL:def 1;
end;
hence thesis by WAYBEL_7:def 4;
end;
theorem Th20:
for B being Element of base_of_frechet_filter holds ex n st B = NAT \ Segm n
proof
let B be Element of base_of_frechet_filter;
B in #(Tails OrderedNAT);
then consider no such that
A1: B = uparrow no;
reconsider n = no as Nat;
take n;
thus thesis by A1,Th13;
end;
theorem Th21:
for B being Subset of NAT st B = NAT \ Segm n holds
B is Element of base_of_frechet_filter
proof
let B be Subset of NAT;
assume
A1: B = NAT \ Segm n;
reconsider no = n as Element of OrderedNAT by ORDINAL1:def 12;
B = uparrow no by A1,Th13;
then B in #(Tails OrderedNAT);
hence thesis;
end;
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
the set of all [:B1,B2:] where B1 is Element of cB1,B2 is Element of cB2;
coherence
proof
set cB12 = the set of all [:B1,B2:] where B1 is Element of cB1,
B2 is Element of cB2;
reconsider cB1a = cB1 as non empty Subset-Family of X1;
reconsider cB2a = cB2 as non empty Subset-Family of X2;
set cB12a = the set of all [:B1,B2:] where B1 is Element of cB1a,
B2 is Element of cB2a;
the set of all [:B1,B2:] where B1 is Element of cB1a,
B2 is Element of cB2a ={s where s is Subset of [:X1,X2:]:
ex x1,x2 be set st x1 in cB1a & x2 in cB2a & s = [:x1,x2:]}
by SRINGS_2:2;
then reconsider cB12 as Subset-Family of [:X1,X2:] by Th3;
now
thus
A1: cB12 is non empty
proof
set B1 = the Element of cB1a, B2 = the Element of cB2a;
[:B1,B2:] in cB12;
hence thesis;
end;
thus cB12 is with_non-empty_elements
proof
assume not cB12 is with_non-empty_elements;
then {} in cB12 by SETFAM_1:def 8;
then ex B1 be Element of cB1a, B2 be Element of cB2a st {} = [:B1,B2:];
hence contradiction;
end;
thus cB12 is quasi_basis
proof
hereby
let b1,b2 be Element of cB12;
b1 in cB12 by A1;
then consider b11 be Element of cB1, b12 be Element of cB2 such that
A2: b1 = [:b11,b12:];
b2 in cB12 by A1;
then consider b21 be Element of cB1, b22 be Element of cB2 such that
A3: b2 = [:b21,b22:];
cB1 is quasi_basis;
then consider a1 be Element of cB1 such that
A4: a1 c= b11 /\ b21;
cB2 is quasi_basis;
then consider a2 be Element of cB2 such that
A5: a2 c= b12 /\ b22;
[:a1,a2:] in cB12;
then reconsider b = [:a1,a2:] as Element of cB12;
[:a1,a2:] c= [:b11 /\ b21, a2:] &
[:b11 /\ b21, a2:] c= [:b11 /\ b21, b12 /\ b22:]
by A4,A5,ZFMISC_1:95;
then [:a1,a2:] c= [:b11 /\ b21,b12 /\ b22:];
then b c= b1 /\ b2 by A2,A3,ZFMISC_1:100;
hence ex b be Element of cB12 st b c= b1 /\ b2;
end;
end;
end;
hence thesis;
end;
end;
theorem Th22:
cF1 = <. cB1.) & cF1 = <. cA1.) &
cF2 = <. cB2.) & cF2 = <. cA2.) implies
<. [:cB1,cB2:] .) = <. [:cA1,cA2:] .)
proof
assume that
A1: cF1 = <. cB1.) and
A2: cF1 = <. cA1.) and
A3: cF2 = <. cB2.) and
A4: cF2 = <. cA2.);
A5: cB1,cA1 are_equivalent_generators by A1,A2,CARDFIL2:26;
A6: cB2,cA2 are_equivalent_generators by A3,A4,CARDFIL2:26;
now
hereby
let B be Element of [:cB1,cB2:];
B in [:cB1,cB2:];
then consider B1 be Element of cB1, B2 be Element of cB2 such that
A7: B = [:B1,B2:];
consider B1A1 be Element of cA1 such that
A8: B1A1 c= B1 by A5;
consider B2A2 be Element of cA2 such that
A9: B2A2 c= B2 by A6;
[:B1A1,B2A2:] in [:cA1,cA2:];
then reconsider A = [:B1A1,B2A2:] as Element of [:cA1,cA2:];
[:B1A1,B2A2:] c= [:B1,B2A2:] & [:B1,B2A2:] c= [:B1,B2:]
by A8,A9,ZFMISC_1:95;
then A c= B by A7;
hence ex A be Element of [:cA1,cA2:] st A c= B;
end;
hereby
let A be Element of [:cA1,cA2:];
A in [:cA1,cA2:];
then consider A1 be Element of cA1, A2 be Element of cA2 such that
A10: A = [:A1,A2:];
consider A1B1 be Element of cB1 such that
A11: A1B1 c= A1 by A5;
consider A2B2 be Element of cB2 such that
A12: A2B2 c= A2 by A6;
[:A1B1,A2B2:] in [:cB1,cB2:];
then reconsider B = [:A1B1,A2B2:] as Element of [:cB1,cB2:];
[:A1B1,A2B2:] c= [:A1,A2B2:] & [:A1,A2B2:] c= [:A1,A2:]
by A11,A12,ZFMISC_1:95;
then B c= A by A10;
hence ex B be Element of [:cB1,cB2:] st B c= A;
end;
end;
then [:cB1,cB2:], [:cA1,cA2:] are_equivalent_generators;
hence thesis by CARDFIL2:20;
end;
theorem Th23:
cBa1 = cB1 implies <.cB1.] = cF1
proof
assume
A1: cBa1 = cB1;
cF1 = <.#cBa1.] by CARDFIL2:21;
hence thesis by A1;
end;
theorem Th24:
ex cB1 st <.cB1.) = cF1
proof
A1: cF1 is basis of cF1 by CARDFIL2:13;
then reconsider cB1 = cF1 as filter_base of X1 by CARDFIL2:29;
<.cB1.) = <.cB1.];
hence thesis by A1,Th23;
end;
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
:Def1:
ex cB1 being filter_base of X1, cB2 being filter_base of X2 st
<.cB1.) = cF1 & <.cB2.) = cF2 & it = <. [:cB1,cB2:] .);
existence
proof
consider cB1 be filter_base of X1 such that
A1: <.cB1.) = cF1 by Th24;
consider cB2 be filter_base of X2 such that
A2: <.cB2.) = cF2 by Th24;
<. [:cB1,cB2:] .) is Filter of [:X1,X2:];
hence thesis by A1,A2;
end;
uniqueness by Th22;
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
:Def2:
ex cB3 being filter_base of X1, cB4 being filter_base of X2 st
cB1 = cB3 & cB2 = cB4 & it = [: cB3, cB4 :];
existence
proof
reconsider cB3 = cB1 as filter_base of X1 by CARDFIL2:29;
reconsider cB4 = cB2 as filter_base of X2 by CARDFIL2:29;
reconsider cF1F2 = <. cF1 ,cF2 .) as Filter of [:X1,X2:];
consider cB5 being filter_base of X1, cB6 being filter_base of X2 such that
A1: <.cB5.) = cF1 and
A2: <.cB6.) = cF2 and
A3: cF1F2 = <. [:cB5,cB6:] .) by Def1;
A4: <.cB3.) = cF1 & <.cB4.) = cF2 by Th23;
[:cB3,cB4:] c= <. [:cB3,cB4:] .) by CARDFIL2:18;
then reconsider cB3B4 = [: cB3,cB4 :] as non empty Subset of cF1F2
by A4,A1,A2,A3,Th22;
cB3B4 is filter_basis
proof
let f be Element of cF1F2;
f is Element of <. [:cB3,cB4:] .) by A4,A1,A2,A3,Th22;
hence thesis by CARDFIL2:def 8;
end;
hence thesis;
end;
uniqueness;
end;
definition
let n be Nat;
func square-uparrow n -> Subset of [:NAT,NAT:] means
:Def3:
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;
existence
proof
defpred P[Element of [:NAT,NAT:]] means
ex n1,n2 being Nat st n1 = $1`1 & n2 = $1`2 & n <= n1 & n <= n2;
ex B be Subset of [:NAT,NAT:] st for x be Element of [:NAT,NAT:] holds
x in B iff P[x] from SUBSET_1:sch 3;
hence thesis;
end;
uniqueness
proof
let x1, x2 be Subset of [:NAT,NAT:] such that
A1: for x being Element of [:NAT,NAT:] holds x in x1 iff
ex n1,n2 being Nat st n1 = x`1 & n2 = x`2 & n <= n1 & n <= n2 and
A2: for x being Element of [:NAT,NAT:] holds x in x2 iff
ex n1,n2 being Nat st n1 = x`1 & n2 = x`2 & n <= n1 & n <= n2;
x1 = x2
proof
thus x1 c= x2
proof
let t be object;
assume
A3: t in x1;
then reconsider u = t as Element of [:NAT,NAT:];
ex n1,n2 being Nat st n1 = u`1 & n2 = u`2 & n <= n1 & n <= n2
by A3,A1;
hence t in x2 by A2;
end;
let t be object;
assume
A4: t in x2;
then reconsider u = t as Element of [:NAT,NAT:];
ex n1,n2 being Nat st n1 = u`1 & n2 = u`2 & n <= n1 & n <= n2
by A4,A2;
hence t in x1 by A1;
end;
hence thesis;
end;
end;
theorem Th25:
[n,n] in square-uparrow n
proof
n in NAT by ORDINAL1:def 12;
then reconsider x = [n,n] as Element of [:NAT,NAT:] by ZFMISC_1:def 2;
x`1 = n & x`2 = n;
hence thesis by Def3;
end;
registration let n;
cluster square-uparrow n -> non empty;
coherence by Th25;
end;
theorem
[i,j] in square-uparrow n implies [i + k,j] in square-uparrow n &
[i,j + l] in square-uparrow n
proof
assume [i,j] in square-uparrow n;
then consider i1,j1 be Nat such that
A1: i1 = [i,j]`1 and
A2: j1 = [i,j]`2 and
A3: n <= i1 and
A4: n <= j1 by Def3;
i <= i + k & j <= j + l by NAT_1:11; then
A5: n <= i + k & n <= j + l by A1,A2,A3,A4,XXREAL_0:2;
i in NAT & i + k in NAT & j in NAT & j + l in NAT by ORDINAL1:def 12;
then reconsider x = [i + k,j], y = [i,j + l] as Element of [:NAT,NAT:]
by ZFMISC_1:def 2;
now
ex i2,j1 be Nat st i2 = x`1 & j1 = x`2 & n <= i + k & n <= j by A2,A4,A5;
hence x in square-uparrow n by Def3;
ex i1,j2 be Nat st i1 = y`1 & j2 = y`2 & n <= i & n <= j + l by A1,A3,A5;
hence y in square-uparrow n by Def3;
end;
hence thesis;
end;
theorem
square-uparrow n is infinite Subset of [:NAT,NAT:]
proof
assume not square-uparrow n is infinite Subset of [:NAT,NAT:];
then reconsider A = square-uparrow n as finite Subset of [:NAT,NAT:];
consider i,j be Nat such that
A1: A c= [:Segm i,Segm j:] by Th16;
consider k,l be Nat such that
k = [n,n]`1 and l = [n,n]`2 and
A2: n <= k and
A3: n <= l;
k <= k + i & l <= l + j by NAT_1:11; then
A4: n <= k + i & n <= l + j by XXREAL_0:2,A2,A3;
k + i in NAT & l + j in NAT by ORDINAL1:def 12;
then reconsider y = [k + i,l + j] as Element of [:NAT,NAT:]
by ZFMISC_1:def 2;
y`1 = k + i & y`2 = l + j;
then y in square-uparrow n by Def3,A4;
then ex a,b be object st a in Segm i & b in Segm j & y = [a,b]
by A1,ZFMISC_1:def 2;
then k + i in Segm i & l + j in Segm j by XTUPLE_0:1;
then k + i - i < i - i & l + j - j < j - j by NAT_1:44,XREAL_1:14;
then k < 0 & l < 0;
hence thesis;
end;
theorem Th26:
no = n implies square-uparrow n = [:uparrow no,uparrow no:]
proof
assume
A1: no = n;
thus square-uparrow n c= [:uparrow no,uparrow no:]
proof
let x be object;
assume
A3: x in square-uparrow n;
then reconsider y = x as Element of [:NAT,NAT:];
consider n1,n2 be Nat such that
A4: n1 = y`1 and
A5: n2 = y`2 and
A6: n <= n1 and
A7: n <= n2 by A3,Def3;
A8: n1 in uparrow no & n2 in uparrow no by A1,A6,A7,Th11;
ex x1,x2 be object st x1 in NAT & x2 in NAT & x = [x1,x2]
by A3,ZFMISC_1:def 2;
then reconsider z = x as pair object;
z = [n1,n2] by A4,A5;
hence thesis by A8,ZFMISC_1:def 2;
end;
let x be object;
assume x in [:uparrow no, uparrow no:];
then consider y1,y2 be object such that
A9: y1 in uparrow no and
A10: y2 in uparrow no and
A11: x = [y1,y2] by ZFMISC_1:def 2;
reconsider x as Element of [:NAT,NAT:] by A9,A10,A11,ZFMISC_1:def 2;
reconsider y1, y2 as Nat by A9,A10;
A12: n <= y1 & n <= y2 by A1,A9,A10,Th12;
x`1 = y1 & x`2 = y2 by A11;
hence thesis by A12,Def3;
end;
theorem
m = n - 1 implies square-uparrow n c= [:NAT,NAT:] \ [:Seg m,Seg m:]
proof
assume
A1: m = n - 1;
let x be object;
assume
A2: x in square-uparrow n;
then reconsider y = x as Element of [:NAT,NAT:];
consider n1,n2 be Nat such that
A3: n1 = y`1 and
A4: n2 = y`2 and
A5: n <= n1 and
n <= n2 by A2,Def3;
not x in [:Seg m,Seg m:]
proof
assume x in [:Seg m,Seg m:];
then ex x1,x2 be object st x1 in Seg m & x2 in Seg m &
x = [x1,x2] by ZFMISC_1:def 2;
then n1 <= m & n2 <= m by A3,A4,FINSEQ_1:1;
then n <= m by A5,XXREAL_0:2;
then n - n <= n - 1 - n by A1,XREAL_1:9;
then 0 <= -1;
hence thesis;
end;
hence thesis by A2,XBOOLE_0:def 5;
end;
theorem
square-uparrow n c= [:NAT,NAT:] \ [:Segm n,Segm n:]
proof
let x be object;
assume
A1: x in square-uparrow n;
then reconsider y = x as Element of [:NAT,NAT:];
consider n1,n2 be Nat such that
A2: n1 = y`1 and
A3: n2 = y`2 and
A4: n <= n1 and
n <= n2 by A1,Def3;
not x in [:Segm n,Segm n:]
proof
assume x in [:Segm n,Segm n:];
then ex x1,x2 be object st x1 in Segm n & x2 in Segm n & x = [x1,x2]
by ZFMISC_1:def 2;
then n1 <= n - 1 & n2 <= n - 1 by A2,A3,STIRL2_1:10;
then n <= n - 1 by A4,XXREAL_0:2;
then n - n <= n - 1 - n by XREAL_1:9;
then 0 <= -1;
hence thesis;
end;
hence thesis by A1,XBOOLE_0:def 5;
end;
theorem Th27:
square-uparrow n = [:NAT \ Segm n, NAT \ Segm n:]
proof
reconsider no = n as Element of OrderedNAT by ORDINAL1:def 12;
uparrow no = NAT \Segm n by Th13;
hence thesis by Th26;
end;
theorem Th28:
ex n st square-uparrow n c= [:(NAT \ Segm i),(NAT \ Segm j):]
proof
reconsider n = max(i,j) as Element of NAT by ORDINAL1:def 12;
take n;
let x be object;
assume
A1: x in square-uparrow n;
then reconsider y = x as Element of [:NAT,NAT:];
consider n1,n2 be Nat such that
A2: y`1 = n1 and
A3: y`2 = n2 and
A4: n <= n1 and
A5: n <= n2 by A1,Def3;
A6: y is pair by Th4;
i <= n by XXREAL_0:25; then
A7: not n1 in Segm i by A4,XXREAL_0:2,NAT_1:44;
n1 in NAT by ORDINAL1:def 12; then
A8: n1 in NAT \ Segm i by A7,XBOOLE_0:def 5;
j <= n by XXREAL_0:25; then
A9: not n2 in Segm j by A5,XXREAL_0:2,NAT_1:44;
n2 in NAT by ORDINAL1:def 12;
then n2 in NAT \ Segm j by A9,XBOOLE_0:def 5;
hence thesis by A2,A3,A6,A8,ZFMISC_1:def 2;
end;
theorem Th29:
n = max(i,j) implies
square-uparrow n c= square-uparrow i /\ square-uparrow j
proof
assume
A1: n = max(i,j);
let x be object;
assume
A2: x in square-uparrow n;
then reconsider y = x as Element of [:NAT,NAT:];
consider n1,n2 be Nat such that
A3: n1 = y`1 and
A4: n2 = y`2 and
A5: n <= n1 and
A6: n <= n2 by A2,Def3;
i <= n & j <= n by A1,XXREAL_0:25;
then i <= n1 & j <= n1 & i <= n2 & j <= n2 by A5,A6,XXREAL_0:2;
then y in square-uparrow i & y in square-uparrow j by A3,A4,Def3;
hence thesis by XBOOLE_0:def 4;
end;
definition
let n be Nat;
func square-downarrow n -> Subset of [:NAT,NAT:] means
:Def4:
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;
existence
proof
defpred P[Element of [:NAT,NAT:]] means
ex n1,n2 being Nat st n1 = $1`1 & n2 = $1`2 & n1 < n & n2 < n;
ex B be Subset of [:NAT,NAT:] st for x be Element of [:NAT,NAT:] holds
x in B iff P[x] from SUBSET_1:sch 3;
hence thesis;
end;
uniqueness
proof
let x1, x2 be Subset of [:NAT,NAT:] such that
A1: for x being Element of [:NAT,NAT:] holds x in x1 iff
ex n1,n2 being Nat st n1 = x`1 & n2 = x`2 & n1 < n & n2 < n and
A2: for x being Element of [:NAT,NAT:] holds x in x2 iff
ex n1,n2 being Nat st n1 = x`1 & n2 = x`2 & n1 < n & n2 < n;
thus x1 c= x2
proof
let t be object;
assume
A3: t in x1;
then reconsider u = t as Element of [:NAT,NAT:];
ex n1,n2 being Nat st n1 = u`1 & n2 = u`2 & n1 < n & n2 < n by A3,A1;
hence t in x2 by A2;
end;
let t be object;
assume
A4: t in x2;
then reconsider u = t as Element of [:NAT,NAT:];
ex n1,n2 being Nat st n1 = u`1 & n2 = u`2 & n1 < n & n2 < n by A4,A2;
hence t in x1 by A1;
end;
end;
theorem Th30:
square-downarrow n = [:Segm n,Segm n:]
proof
thus square-downarrow n c= [:Segm n,Segm n:]
proof
let x be object;
assume
A2: x in square-downarrow n;
then consider n1,n2 be Nat such that
A3: n1 = x`1 and
A4: n2 = x`2 and
A5: n1 < n and
A6: n2 < n by Def4;
A7: n1 in Segm n by A5,NAT_1:44;
A8: n2 in Segm n by A6,NAT_1:44;
ex x1,x2 be object st x1 in NAT & x2 in NAT & x = [x1,x2]
by A2,ZFMISC_1:def 2;
then reconsider x as pair object;
x = [n1,n2] by A3,A4;
hence thesis by A7,A8,ZFMISC_1:def 2;
end;
let x be object;
assume x in [:Segm n, Segm n:];
then consider y1, y2 be object such that
A9: y1 in Segm n and
A10: y2 in Segm n and
A11: x = [y1,y2] by ZFMISC_1:def 2;
reconsider y1,y2 as Nat by A9,A10;
A12: y1 = x`1 & y2 = x`2 & y1 < n & y2 < n by A11,A9,A10,NAT_1:44;
x is Element of [:NAT,NAT:] by A9,A10,A11,ZFMISC_1:def 2;
hence thesis by A12,Def4;
end;
theorem
for A being finite Subset of [:NAT,NAT:] holds ex n st
A c= square-downarrow n
proof
let A be finite Subset of [:NAT,NAT:];
consider m,n such that
A1: A c= [:Segm m,Segm n:] by Th16;
reconsider m,n as Element of NAT by ORDINAL1:def 12;
reconsider mn = max(m,n) as Nat;
A c= square-downarrow mn
proof
Segm m c= Segm mn & Segm n c= Segm mn by XXREAL_0:25,NAT_1:39;
then [:Segm m,Segm n:] c= [:Segm mn,Segm mn:] by ZFMISC_1:96;
then [:Segm m,Segm n:] c= square-downarrow mn by Th30;
hence thesis by A1;
end;
hence thesis;
end;
theorem
square-downarrow n is finite Subset of [:NAT,NAT:]
proof
[:Segm n,Segm n:] is finite;
hence thesis by Th30;
end;
begin :: Comparaison between cartesian product of Frechet Filter on $\mathbb{N}$ and the Frechet Filter of $\mathbb{N}\times\mathbb{N}$
theorem Th31:
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:]
proof
let x be Element of [: base_of_frechet_filter,base_of_frechet_filter :];
x in the set of all [:B1,B2:] where B1 is Element of
base_of_frechet_filter, B2 is Element of base_of_frechet_filter;
then consider B1 be Element of base_of_frechet_filter,
B2 be Element of base_of_frechet_filter such that
A1: x = [:B1,B2:];
consider i such that
A2: B1 = NAT \ Segm i by Th20;
consider j such that
A3: B2 = NAT \ Segm j by Th20;
take i,j;
thus thesis by A1,A2,A3;
end;
theorem Th32:
for x being Element of [: base_of_frechet_filter,base_of_frechet_filter :]
holds ex n st square-uparrow n c= x
proof
let x be Element of [: base_of_frechet_filter,base_of_frechet_filter :];
ex i,j st x = [:NAT \ Segm i,NAT \ Segm j:] by Th31;
hence thesis by Th28;
end;
theorem
[: base_of_frechet_filter,base_of_frechet_filter :] is
filter_base of [:NAT,NAT:];
theorem Th33:
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) .)
proof
reconsider bff = base_of_frechet_filter as basis of Frechet_Filter(NAT)
by CARDFIL2:56;
[: bff,bff :] is basis of <. Frechet_Filter(NAT),Frechet_Filter(NAT).);
hence thesis;
end;
definition
func all-square-uparrow -> filter_base of [:NAT,NAT:] equals
the set of all square-uparrow n where n is Nat;
coherence
proof
set S = the set of all square-uparrow n where n is Nat;
S c= bool [:NAT,NAT:]
proof
let x be object;
assume x in S;
then ex n be Nat st x = square-uparrow n;
hence thesis;
end;
then reconsider S as Subset-Family of [:NAT,NAT:];
now
thus S is with_non-empty_elements
proof
assume not S is with_non-empty_elements;
then {} in S by SETFAM_1:def 8;
then ex n be Nat st {} = square-uparrow n;
hence thesis;
end;
A1: square-uparrow 1 in S;
hence S is non empty;
thus S is quasi_basis
proof
let b1,b2 be Element of S;
b1 in S by A1;
then consider i such that
A2: b1 = square-uparrow i;
b2 in S by A1;
then consider j such that
A3: b2 = square-uparrow j;
reconsider i,j as Element of NAT by ORDINAL1:def 12;
reconsider n = max(i,j) as Element of NAT;
square-uparrow n in S;
hence thesis by A2,A3,Th29;
end;
end;
hence thesis;
end;
end;
theorem Th34:
all-square-uparrow, [: base_of_frechet_filter,base_of_frechet_filter :]
are_equivalent_generators
proof
set cB1 = all-square-uparrow,
cB2 = [: base_of_frechet_filter,base_of_frechet_filter :];
A1: now
let b1 be Element of cB1;
b1 in cB1;
then consider n such that
A2: b1 = square-uparrow n;
NAT \ Segm n is Element of base_of_frechet_filter by Th21;
then [:NAT \ Segm n,NAT \ Segm n :] in [: base_of_frechet_filter,
base_of_frechet_filter :];
then reconsider b2 = [:NAT \ Segm n, NAT \ Segm n:] as Element of cB2;
b2 c= b1 by A2,Th27;
hence ex b2 be Element of cB2 st b2 c= b1;
end;
now
let b2 be Element of cB2;
consider n such that
A1: square-uparrow n c= b2 by Th32;
square-uparrow n in all-square-uparrow;
hence ex b1 be Element of cB1 st b1 c= b2 by A1;
end;
hence thesis by A1;
end;
theorem Th35:
<. [: base_of_frechet_filter,base_of_frechet_filter :] .)
= <. Frechet_Filter(NAT),Frechet_Filter(NAT).)
proof
consider cB being basis of Frechet_Filter(NAT) such that
A1: cB = base_of_frechet_filter and
[: cB, cB :] is basis of <. Frechet_Filter(NAT),Frechet_Filter(NAT) .)
by Th33;
<. #([: cB,cB :]) .] = <. [: base_of_frechet_filter,
base_of_frechet_filter :] .)
proof
set cF1 = <. #([: cB,cB :]) .],
cF2 = <. [: base_of_frechet_filter,base_of_frechet_filter :] .);
now
let x be object;
assume
A2: x in cF1;
then reconsider y = x as Subset of [:NAT,NAT:];
consider b be Element of #([: cB,cB:]) such that
A3: b c= y by A2,CARDFIL2:def 8;
consider cB3 being filter_base of NAT,
cB4 being filter_base of NAT such that
A4: cB = cB3 and
A5: cB = cB4 and
A6: [: cB,cB :] = [:cB3,cB4:] by Def2;
b in the set of all [:B1,B2:] where B1 is Element of cB3,
B2 is Element of cB4 by A6;
then consider B1 be Element of cB3, B2 be Element of cB4 such that
A7: b = [:B1,B2:];
b in [: base_of_frechet_filter,base_of_frechet_filter :]
by A1,A4,A5,A7;
hence x in cF2 by A3,CARDFIL2:def 8;
end;
then
A8: cF1 c= cF2;
now
let x be object;
assume
A9: x in cF2;
then reconsider y = x as Subset of [:NAT,NAT:];
consider b be Element of [: base_of_frechet_filter,
base_of_frechet_filter :] such that
A10: b c= y by A9,CARDFIL2:def 8;
ex cB3 being filter_base of NAT, cB4 being filter_base of NAT st
cB = cB3 & cB = cB4 & [:cB,cB:] = [:cB3,cB4:] by Def2;
hence x in cF1 by A1,A10,CARDFIL2:def 8;
end;
then cF2 c= cF1;
hence thesis by A8;
end;
hence thesis by CARDFIL2:21;
end;
theorem Th36:
<. all-square-uparrow .)
= <. Frechet_Filter(NAT),Frechet_Filter(NAT).) by Th34,CARDFIL2:19,Th35;
theorem Th37:
<. Frechet_Filter(NAT),Frechet_Filter(NAT).)
is_filter-finer_than Frechet_Filter([:NAT,NAT:])
proof
now
let x be object;
assume
A1: x in Frechet_Filter([:NAT,NAT:]);
x in the set of all [:NAT,NAT:] \ A where
A is finite Subset of [:NAT,NAT:] by A1,CARDFIL2:51;
then consider A be finite Subset of [:NAT,NAT:] such that
A2: x = [:NAT,NAT:] \ A;
reconsider y = x as Subset of [:NAT,NAT:] by A2;
consider m,n such that
A3: A c= [:Segm m,Segm n:] by Th16;
A4: [:NAT,NAT:] \ [:Segm m,Segm n:] c= y by A2,A3,XBOOLE_1:34;
[: NAT \ Segm m , NAT \ Segm n:] c= [:NAT,NAT:] \ [:Segm m,Segm n:]
by Th10; then
A5: [: NAT \ Segm m , NAT \ Segm n:] c= y by A4;
NAT \ Segm m is Element of base_of_frechet_filter &
NAT \ Segm n is Element of base_of_frechet_filter by Th21;
then [:NAT \ Segm m ,NAT \ Segm n :] in
[: base_of_frechet_filter,base_of_frechet_filter :];
hence x in <.Frechet_Filter(NAT),Frechet_Filter(NAT).)
by Th35,A5,CARDFIL2:def 8;
end;
then Frechet_Filter([:NAT,NAT:]) c=
<. Frechet_Filter(NAT),Frechet_Filter(NAT).);
hence thesis;
end;
theorem Th38:
([: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:])
proof
set X = [:NAT,NAT:] \ the set of all [0,n] where n is Nat;
A1: square-uparrow 1 c= X
proof
let x be object;
assume x in square-uparrow 1;
then x in [:NAT \ Segm 1,NAT \ Segm 1:] by Th27;
then consider n,m be object such that
A2: n in NAT \ Segm 1 and
A3: m in NAT \ Segm 1 and
A4: x = [n,m] by ZFMISC_1:def 2;
reconsider n,m as Nat by A2,A3;
A5: x in [:NAT,NAT:] by A4,A2,A3,ZFMISC_1:def 2;
not n in Segm 1 by A2,XBOOLE_0:def 5;
then
A6: not n = 0 by NAT_1:44;
not x in (the set of all [0,n] where n is Nat)
proof
assume not thesis;
then ex k be Nat st x = [0,k];
hence thesis by A6,A4,XTUPLE_0:1;
end;
hence thesis by A5,XBOOLE_0:def 5;
end;
square-uparrow 1 in the set of all square-uparrow n where n is Nat;
hence X in <. Frechet_Filter(NAT),Frechet_Filter(NAT).)
by A1,CARDFIL2:def 8,Th36;
thus not X in Frechet_Filter([:NAT,NAT:])
proof
assume not thesis;
then X in the set of all [:NAT,NAT:] \ A where
A is finite Subset of [:NAT,NAT:] by CARDFIL2:51;
then consider A be finite Subset of [:NAT,NAT:] such that
A7: X = [:NAT,NAT:] \ A;
the set of all [0,n] where n is Nat c= [:NAT,NAT:]
proof
let x be object;
assume x in the set of all [0,n] where n is Nat;
then consider n be Nat such that
A8: x = [0,n];
n in NAT & 0 in NAT by ORDINAL1:def 12;
hence thesis by A8,ZFMISC_1:def 2;
end;
hence contradiction by A7,COMBGRAS:5,Th9;
end;
end;
theorem
Frechet_Filter([:NAT,NAT:]) <> <. Frechet_Filter(NAT),Frechet_Filter(NAT).)
by Th38;
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 Th39:
cF4 is_filter-finer_than cF3 implies lim_filter cF3 c= lim_filter cF4
proof
assume
A1: cF4 is_filter-finer_than cF3;
let x be object;
assume x in lim_filter cF3;
then consider y be Point of T such that
A2: x = y and
A3: cF3 is_filter-finer_than NeighborhoodSystem y;
NeighborhoodSystem y c= cF3 & cF3 c= cF4 by A1,A3;
then NeighborhoodSystem y c= cF4;
then cF4 is_filter-finer_than NeighborhoodSystem y;
hence thesis by A2;
end;
theorem Th40:
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)
proof
let f be Function of X,Y, cFXa,cFXb be Filter of X;
assume
A1: cFXb is_filter-finer_than cFXa;
filter_image(f,cFXa) c= filter_image(f,cFXb)
proof
let x be object;
assume x in filter_image(f,cFXa);
then ex M be Subset of Y st x = M & f"(M) in cFXa;
hence thesis by A1;
end;
hence thesis;
end;
theorem Th41:
s"(M) in Frechet_Filter([:NAT,NAT:]) iff
ex A being finite Subset of [:NAT,NAT:] st s"(M) = [:NAT,NAT:] \ A
proof
hereby
assume s"(M) in Frechet_Filter([:NAT,NAT:]);
then s"(M) in the set of all [:NAT,NAT:] \ A where
A is finite Subset of [:NAT,NAT:] by CARDFIL2:51;
hence ex A be finite Subset of [:NAT,NAT:] st s"(M) = [:NAT,NAT:] \ A;
end;
assume ex A be finite Subset of [:NAT,NAT:] st s"(M) = [:NAT,NAT:] \ A;
then s"(M) in the set of all [:NAT,NAT:] \ A
where A is finite Subset of [:NAT,NAT:];
hence s"(M) in Frechet_Filter([:NAT,NAT:]) by CARDFIL2:51;
end;
theorem Th42:
s"(M) in <. Frechet_Filter(NAT),Frechet_Filter(NAT).) iff
ex n st square-uparrow n c= s"(M)
proof
hereby
assume s"(M) in <. Frechet_Filter(NAT),Frechet_Filter(NAT).);
then consider b be Element of
[: base_of_frechet_filter,base_of_frechet_filter:] such that
A1: b c= s"(M) by Th35,CARDFIL2:def 8;
ex n st square-uparrow n c= b by Th32;
hence ex n st square-uparrow n c= s"(M) by A1,XBOOLE_1:1;
end;
given n such that
A2: square-uparrow n c= s"(M);
square-uparrow n in the set of all square-uparrow n where n is Nat;
then ex b2 be Element of
[: base_of_frechet_filter,base_of_frechet_filter:] st
b2 c= square-uparrow n by Th34;
then
A3: ex b2 be Element of [: base_of_frechet_filter,base_of_frechet_filter:] st
b2 c= s"(M) by A2,XBOOLE_1:1;
dom s = [:NAT,NAT:] by FUNCT_2:def 1;
then s"(M) is Subset of [:NAT,NAT:] by RELAT_1:132;
hence s"(M) in <. Frechet_Filter(NAT),Frechet_Filter(NAT).)
by A3,Th35,CARDFIL2:def 8;
end;
theorem Th43:
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}
proof
set X = {M where M is Subset of the carrier of T: s"(M) in
Frechet_Filter([:NAT,NAT:])},
Y = {M where M is Subset of the carrier of T:
ex A be finite Subset of [:NAT,NAT:] st s"(M) = [:NAT,NAT:] \ A};
X = Y
proof
now
let x be object;
assume x in X;
then consider M be Subset of the carrier of T such that
A1: x = M and
A2: s"(M) in Frechet_Filter([:NAT,NAT:]);
ex A be finite Subset of [:NAT,NAT:] st s"(M) = [:NAT,NAT:] \ A
by Th41,A2;
hence x in Y by A1;
end;
then
A3: X c= Y;
now
let x be object;
assume x in Y;
then consider M be Subset of the carrier of T such that
A4: x = M and
A5: ex A be finite Subset of [:NAT,NAT:] st s"(M) = [:NAT,NAT:] \ A;
s"(M) in Frechet_Filter([:NAT,NAT:]) by A5,Th41;
hence x in X by A4;
end;
then Y c= X;
hence thesis by A3;
end;
hence thesis;
end;
theorem Th44:
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)}
proof
set X = {M where M is Subset of the carrier of T:
s"(M) in <. Frechet_Filter(NAT),Frechet_Filter(NAT).)},
Y = {M where M is Subset of the carrier of T:
ex n being Nat st square-uparrow n c= s"(M)};
X = Y
proof
now
let x be object;
assume x in X;
then consider M be Subset of the carrier of T such that
A1: x = M and
A2: s"(M) in <. Frechet_Filter(NAT),Frechet_Filter(NAT).);
ex n st square-uparrow n c= s"(M) by Th42,A2;
hence x in Y by A1;
end; then
A3: X c= Y;
now
let x be object;
assume x in Y;
then consider M be Subset of the carrier of T such that
A4: x = M and
A5: ex n st square-uparrow n c= s"(M);
s"(M) in <. Frechet_Filter(NAT),Frechet_Filter(NAT).) by A5,Th42;
hence x in X by A4;
end;
then Y c= X;
hence thesis by A3;
end;
hence thesis;
end;
theorem Th45:
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
proof
let x be Point of T;
set F = filter_image(s,Frechet_Filter([:NAT,NAT:]));
A1: F is_filter-finer_than NeighborhoodSystem x iff
for A be a_neighborhood of x holds
ex B be finite Subset of [:NAT,NAT:] st s"(A) = [:NAT,NAT:] \ B
proof
hereby
assume F is_filter-finer_than NeighborhoodSystem x;
then NeighborhoodSystem x c= {M where
M is Subset of the carrier of T: ex A being finite Subset of
[:NAT,NAT:] st s"(M) = [:NAT,NAT:] \ A} by Th43; then
A2: the set of all A where A is a_neighborhood of x c=
{M where M is Subset of the carrier of T:
ex A being finite Subset of [:NAT,NAT:] st
s"(M) = [:NAT,NAT:] \ A} by YELLOW19:def 1;
thus for A be a_neighborhood of x holds
ex B be finite Subset of [:NAT,NAT:] st s"(A) = [:NAT,NAT:] \ B
proof
let A be a_neighborhood of x;
A in the set of all A where A is a_neighborhood of x;
then A in {M where M is Subset of the carrier of T:
ex A being finite Subset of [:NAT,NAT:] st
s"(M) = [:NAT,NAT:] \ A} by A2;
then ex M be Subset of the carrier of T st A = M &
ex B being finite Subset of [:NAT,NAT:] st
s"(M) = [:NAT,NAT:] \ B;
hence thesis;
end;
end;
assume
A3: for A be a_neighborhood of x holds ex B be finite Subset of
[:NAT,NAT:] st s"(A) = [:NAT,NAT:] \ B;
NeighborhoodSystem x c= F
proof
let y be object;
assume y in NeighborhoodSystem x;
then y in the set of all A where A is a_neighborhood of x
by YELLOW19:def 1;
then consider A be a_neighborhood of x such that
A4: y = A;
ex B be finite Subset of [:NAT,NAT:] st s"(A) = [:NAT,NAT:] \ B by A3;
then A in {M where M is Subset of the carrier of T:
ex A being finite Subset of [:NAT,NAT:] st
s"(M) = [:NAT,NAT:] \ A};
hence thesis by A4,Th43;
end;
hence F is_filter-finer_than NeighborhoodSystem x;
end;
F is_filter-finer_than NeighborhoodSystem x iff x in lim_filter F
proof
thus F is_filter-finer_than NeighborhoodSystem x implies
x in lim_filter F;
assume x in lim_filter F;
then ex y be Point of T st x = y &
F is_filter-finer_than NeighborhoodSystem y;
hence F is_filter-finer_than NeighborhoodSystem x;
end;
hence thesis by A1;
end;
theorem Th46:
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
proof
let x be Point of T;
hereby
assume
A1: x in lim_filter(s,Frechet_Filter([:NAT,NAT:]));
now
let A be a_neighborhood of x;
ex B being finite Subset of [:NAT,NAT:] st
s"(A) = [:NAT,NAT:] \ B by A1,Th45;
hence [:NAT,NAT:] \ s"(A) is finite by Th1;
end;
hence for A be a_neighborhood of x holds [:NAT,NAT:] \ s"(A) is finite;
end;
assume
A2: for A be a_neighborhood of x holds [:NAT,NAT:] \ s"(A) is finite;
now
let A be a_neighborhood of x;
A3: dom s = [:NAT,NAT:] by FUNCT_2:def 1;
[:NAT,NAT:] \ s"(A) is finite by A2;
hence ex B being finite Subset of [:NAT,NAT:] st
s"(A) = [:NAT,NAT:] \ B by A3,RELAT_1:132,Th2;
end;
hence x in lim_filter(s,Frechet_Filter([:NAT,NAT:])) by Th45;
end;
theorem Th47:
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)
proof
let x be Point of T;
set F = filter_image(s,<. Frechet_Filter(NAT),Frechet_Filter(NAT).));
A1: F is_filter-finer_than NeighborhoodSystem x iff
for A be a_neighborhood of x holds ex n be Nat st square-uparrow n c= s"(A)
proof
hereby
assume F is_filter-finer_than NeighborhoodSystem x;
then NeighborhoodSystem x c= {M where
M is Subset of the carrier of T:
ex n being Nat st square-uparrow n c= s"(M)} by Th44; then
A2: the set of all A where A is a_neighborhood of x c=
{M where M is Subset of the carrier of T:
ex n being Nat st square-uparrow n c= s"(M)} by YELLOW19:def 1;
thus for A be a_neighborhood of x holds ex n be Nat st
square-uparrow n c= s"(A)
proof
let A be a_neighborhood of x;
A in the set of all A where A is a_neighborhood of x;
then A in {M where M is Subset of the carrier of T:
ex n being Nat st square-uparrow n c= s"(M)} by A2;
then ex M be Subset of the carrier of T st A = M & ex n be Nat st
square-uparrow n c= s"(M);
hence thesis;
end;
end;
assume
A3: for A be a_neighborhood of x holds ex n be Nat st
square-uparrow n c= s"(A);
NeighborhoodSystem x c= F
proof
let y be object;
assume y in NeighborhoodSystem x;
then y in the set of all A where A is a_neighborhood of x
by YELLOW19:def 1;
then consider A be a_neighborhood of x such that
A4: y = A;
ex n be Nat st square-uparrow n c= s"(A) by A3;
then A in {M where M is Subset of the carrier of T: ex n be Nat st
square-uparrow n c= s"(M)};
hence thesis by A4,Th44;
end;
hence F is_filter-finer_than NeighborhoodSystem x;
end;
F is_filter-finer_than NeighborhoodSystem x iff x in lim_filter F
proof
thus F is_filter-finer_than NeighborhoodSystem x implies
x in lim_filter F;
assume x in lim_filter F;
then ex y be Point of T st x = y &
F is_filter-finer_than NeighborhoodSystem y;
hence F is_filter-finer_than NeighborhoodSystem x;
end;
hence thesis by A1;
end;
theorem Th48:
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)
proof
let x be Point of T,cB be basis of BOOL2F NeighborhoodSystem x;
hereby
assume
A1: x in lim_filter(s,<. Frechet_Filter(NAT),Frechet_Filter(NAT).) );
hereby
let B be Element of cB;
B is a_neighborhood of x by YELLOW19:2;
hence ex n being Nat st square-uparrow n c= s"(B) by A1,Th47;
end;
end;
assume
A2: for B being Element of cB holds ex n being Nat st
square-uparrow n c= s"(B);
now
let A be a_neighborhood of x;
A3: A is Element of BOOL2F NeighborhoodSystem x by YELLOW19:2;
cB is filter_basis;
then consider B be Element of cB such that
A4: B c= A by A3;
A5: ex n being Nat st square-uparrow n c= s"(B) by A2;
s"(B) c= s"(A) by A4,RELAT_1:145;
hence ex n being Nat st square-uparrow n c= s"(A) by A5,XBOOLE_1:1;
end;
hence x in lim_filter(s,<. Frechet_Filter(NAT),Frechet_Filter(NAT).) )
by Th47;
end;
theorem Th49:
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
proof
let x be Point of T,cB be basis of BOOL2F NeighborhoodSystem x;
hereby
assume
A1: x in lim_filter(s,Frechet_Filter[:NAT,NAT:]);
hereby
let B be Element of cB;
B is a_neighborhood of x by YELLOW19:2;
hence ex A being finite Subset of [:NAT,NAT:] st
s"(B) = [:NAT,NAT:] \ A by A1,Th45;
end;
end;
assume
A2: for B being Element of cB holds ex A being finite Subset of [:NAT,NAT:]
st s"(B) = [:NAT,NAT:] \ A;
now
let A be a_neighborhood of x;
A3: A is Element of BOOL2F NeighborhoodSystem x by YELLOW19:2;
cB is filter_basis;
then consider B be Element of cB such that
A4: B c= A by A3;
ex C be finite Subset of [:NAT,NAT:] st s"(B) = [:NAT,NAT:] \ C by A2;
hence [:NAT,NAT:] \ s"(A) is finite by A4,RELAT_1:145,Th1;
end;
hence x in lim_filter(s,Frechet_Filter([:NAT,NAT:])) by Th46;
end;
theorem Th50:
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
proof
let x be Point of T,cB be basis of BOOL2F NeighborhoodSystem x;
hereby
assume
A1: x in lim_filter(s,<. Frechet_Filter(NAT),Frechet_Filter(NAT).));
hereby
let B be Element of cB;
consider n be Nat such that
A2: square-uparrow n c= s"(B) by A1,Th48;
take n;
A3: s.:(square-uparrow n) c= s.:(s"B) by A2,RELAT_1:123;
s.:(s"B) c= B by FUNCT_1:75;
hence s.:(square-uparrow n) c= B by A3;
end;
end;
assume
A4: for B being Element of cB holds ex n being Nat st
s.:(square-uparrow n) c= B;
now
let B be Element of cB;
consider n be Nat such that
A5: s.:(square-uparrow n) c= B by A4;
A6: s"(s.:(square-uparrow n)) c= s"B by A5,RELAT_1:143;
dom s = [:NAT,NAT:] by FUNCT_2:def 1;
then square-uparrow n c= s"(s.:(square-uparrow n)) by FUNCT_1:76;
then square-uparrow n c= s"B by A6;
hence ex n be Nat st square-uparrow n c= s"(B);
end;
hence x in lim_filter(s,<. Frechet_Filter(NAT),Frechet_Filter(NAT).))
by Th48;
end;
theorem Th51:
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
proof
let x be Point of T,cB be basis of BOOL2F NeighborhoodSystem x;
hereby
assume
A1: x in lim_filter(s,Frechet_Filter([:NAT,NAT:]));
hereby
let B be Element of cB;
consider A be finite Subset of [:NAT,NAT:] such that
A2: s"(B) = [:NAT,NAT:] \ A by A1,Th49;
take A;
thus s.:([:NAT,NAT:] \ A) c= B by A2,FUNCT_1:75;
end;
end;
assume
A3: for B being Element of cB holds ex A be finite Subset of [:NAT,NAT:] st
s.:([:NAT,NAT:]\A) c= B;
for A being a_neighborhood of x holds [:NAT,NAT:] \ s"(A) is finite
proof
let A be a_neighborhood of x;
A4: A is Element of BOOL2F NeighborhoodSystem x by YELLOW19:2;
cB is filter_basis;
then consider B be Element of cB such that
A5: B c= A by A4;
consider C be finite Subset of [:NAT,NAT:] such that
A6: s.:([:NAT,NAT:] \ C) c= B by A3;
s.:([:NAT,NAT:]\ C ) c= A by A6,A5; then
A7: s"(s.:([:NAT,NAT:] \ C)) c= s"A by RELAT_1:143;
dom s = [:NAT,NAT:] by FUNCT_2:def 1;
then [:NAT,NAT:] \ C c= s"(s.:([:NAT,NAT:] \ C)) by FUNCT_1:76;
then [:NAT,NAT:] \ C c= s"A by A7; then
[:NAT,NAT:] \ s"A c= ([:NAT,NAT:] \ ([:NAT,NAT:] \C)) by XBOOLE_1:34;
then [:NAT,NAT:] \ s"A c= [:NAT,NAT:] /\ C by XBOOLE_1:48;
hence thesis;
end;
hence x in lim_filter(s,Frechet_Filter([:NAT,NAT:])) by Th46;
end;
theorem Th52:
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
proof
let x be Point of T,cB be basis of BOOL2F NeighborhoodSystem x;
hereby
assume
A1: x in lim_filter(s,Frechet_Filter([:NAT,NAT:]));
now
let B be Element of cB;
consider A be finite Subset of [:NAT,NAT:] such that
A2: s.:([:NAT,NAT:] \ A) c= B by A1,Th51;
consider n,m such that
A3: A c= [:Segm n,Segm m:] by Th16;
[:NAT,NAT:] \ [:Segm n,Segm m:] c= [:NAT,NAT:] \ A by A3,XBOOLE_1:34;
then s.:([:NAT,NAT:] \ [:Segm n,Segm m:]) c= s.:([:NAT,NAT:] \ A)
by RELAT_1:123;
then s.:([:NAT,NAT:] \ [:Segm n,Segm m:]) c= B by A2;
hence ex n,m st s.:([:NAT,NAT:] \ [:Segm n,Segm m:]) c= B;
end;
hence for B being Element of cB holds ex n,m st
s.:([:NAT,NAT:] \ [:Segm n,Segm m:]) c= B;
end;
assume
A4: for B being Element of cB holds ex n,m st
s.:([:NAT,NAT:] \ [:Segm n,Segm m:]) c= B;
now
let B be Element of cB;
consider n,m such that
A5: s.:([:NAT,NAT:] \ [:Segm n,Segm m:]) c= B by A4;
reconsider A = [:Segm n,Segm m:] as finite Subset of [:NAT,NAT:];
thus ex A be finite Subset of [:NAT,NAT:] st s.:([:NAT,NAT:] \ A) c= B
by A5;
end;
hence x in lim_filter(s,Frechet_Filter([:NAT,NAT:])) by Th51;
end;
theorem Th53:
x in s.:(square-uparrow n) iff ex i,j st n <= i & n <= j & x = s.(i,j)
proof
hereby
assume x in s.:(square-uparrow n);
then consider y be object such that
A1: y in dom s and
A2: y in square-uparrow n and
A3: x = s.y by FUNCT_1:def 6;
reconsider z = y as Element of [:NAT,NAT:] by A1;
consider i,j such that
A4: z`1 = i and
A5: z`2 = j and
A6: n <= i and
A7: n <= j by A2,Def3;
consider m1,m2 be object such that
m1 in NAT and
m2 in NAT and
A8: z = [m1,m2] by ZFMISC_1:def 2;
x = s.(i,j) by A4,A5,A8,A3,BINOP_1:def 1;
hence ex i,j st n <= i & n <= j & x = s.(i,j) by A6,A7;
end;
assume ex i,j st n <= i & n <= j & x = s.(i,j);
then consider i,j such that
A9: n <= i and
A10: n <= j and
A11: x = s.(i,j);
A12: dom s = [:NAT,NAT:] by FUNCT_2:def 1;
A13: i in NAT & j in NAT by ORDINAL1:def 12;
A14: x = s.([i,j]) by A11,BINOP_1:def 1;
[i,j]`1 = i & [i,j]`2 = j & [i,j] in [:NAT,NAT:]
by A13,ZFMISC_1:def 2;
then [i,j] in square-uparrow n by A9,A10,Def3;
hence x in s.:(square-uparrow n) by A12,A14,FUNCT_1:def 6;
end;
theorem
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)
proof
hereby
assume x in s.:([:NAT,NAT:] \ [:Segm i,Segm j:]);
then consider y be object such that
A1: y in dom s and
A2: y in [:NAT,NAT:] \ [:Segm i,Segm j:] and
A3: x = s.y by FUNCT_1:def 6;
reconsider z = y as Element of [:NAT,NAT:] by A1;
A4: not z`1 in Segm i or not z`2 in Segm j
proof
assume not (not z`1 in Segm i or not z`2 in Segm j);
then
A5: [z`1,z`2] in [:Segm i,Segm j:] by ZFMISC_1:def 2;
z is pair by Th4;
hence thesis by A2,A5,XBOOLE_0:def 5;
end;
reconsider n = z`1,m = z`2 as Nat;
take n,m;
thus i <= n or j <= m by A4,NAT_1:44;
z is pair by Th4;
hence x = s.(n,m) by A3,BINOP_1:def 1;
end;
assume ex n,m be Nat st (i <= n or j <= m) & x = s.(n,m);
then consider n,m be Nat such that
A6: (i <= n or j <= m) and
A7: x = s.(n,m);
n in NAT & m in NAT by ORDINAL1:def 12; then
A8: [n,m] in [:NAT,NAT:] by ZFMISC_1:def 2;
not [n,m] in [:Segm i,Segm j:]
proof
assume [n,m] in [:Segm i,Segm j:];
then ex a,b be object st a in Segm i & b in Segm j & [n,m] = [a,b]
by ZFMISC_1:def 2;
then n in Segm i & m in Segm j by XTUPLE_0:1;
hence thesis by A6,NAT_1:44;
end;
then
A9: [n,m] in [:NAT,NAT:] \ [:Segm i,Segm j:] by A8,XBOOLE_0:def 5;
A10: x = s.([n,m]) by BINOP_1:def 1,A7;
[n,m] in dom s by A8,FUNCT_2:def 1;
hence x in s.:([:NAT,NAT:] \ [:Segm i,Segm j:]) by A9,A10,FUNCT_1:def 6;
end;
theorem Th54:
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
proof
let x be Point of T, cB be basis of BOOL2F NeighborhoodSystem x;
(for B being Element of cB holds ex n being Nat st
s.:(square-uparrow n) c= B) 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)
proof
hereby
assume
A1: for B being Element of cB holds ex n being Nat st
s.:(square-uparrow n) c= B;
hereby
let B be Element of cB;
consider n0 being Nat such that
A2: s.:(square-uparrow n0) c= B by A1;
take n0;
thus for n1,n2 be Nat st n0 <= n1 & n0 <= n2 holds s.(n1,n2) in B
by A2,Th53;
end;
end;
assume
A3: 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;
hereby
let B be Element of cB;
consider n0 be Nat such that
A4: for n1,n2 being Nat st n0 <= n1 & n0 <= n2 holds s.(n1,n2) in B by A3;
thus ex n being Nat st s.:(square-uparrow n) c= B
proof
take n0;
let x be object;
assume x in s.:(square-uparrow n0);
then ex n1,n2 be Nat st n0 <= n1 & n0 <= n2 & x = s.(n1,n2) by Th53;
hence thesis by A4;
end;
end;
end;
hence thesis by Th50;
end;
theorem Th55:
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
proof
let x be Point of T,cB be basis of BOOL2F NeighborhoodSystem x;
hereby
assume
A1: x in lim_filter(s,Frechet_Filter([:NAT,NAT:]));
hereby
let B be Element of cB;
consider i,j be Nat such that
A2: s.:([:NAT,NAT:] \ [:Segm i,Segm j:]) c= B by A1,Th52;
take i,j;
thus for m,n st i <= m or j <= n holds s.(m,n) in B
proof
let m,n;
assume
A3: i <= m or j <= n;
m in NAT & n in NAT by ORDINAL1:def 12; then
A4: [m,n] in [:NAT,NAT:] by ZFMISC_1:def 2;
A5: not (m in Segm i & n in Segm j) by A3,NAT_1:44;
not [m,n] in [:Segm i,Segm j:]
proof
assume [m,n] in [:Segm i,Segm j:];
then ex a,b be object st a in Segm i & b in Segm j & [m,n] = [a,b]
by ZFMISC_1:def 2;
hence thesis by A5,XTUPLE_0:1;
end;
then
A6: [m,n] in [:NAT,NAT:] \ [:Segm i,Segm j:] by A4,XBOOLE_0:def 5;
[m,n] in dom s by A4,FUNCT_2:def 1;
then s.([m,n]) in s.:([:NAT,NAT:] \ [:Segm i,Segm j:])
by A6,FUNCT_1:def 6;
then s.([m,n]) in B by A2;
hence s.(m,n) in B by BINOP_1:def 1;
end;
end;
end;
assume
A7: 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;
now
let B be Element of cB;
consider i,j such that
A8: for m,n st i <= m or j <= n holds s.(m,n) in B by A7;
s.:([:NAT,NAT:] \ [:Segm i,Segm j:]) c= B
proof
let t be object;
assume t in s.:([:NAT,NAT:] \ [:Segm i,Segm j:]);
then consider a be object such that
A9: a in dom s and
A10: a in [:NAT,NAT:] \ [:Segm i,Segm j:] and
A11: t = s.a by FUNCT_1:def 6;
reconsider a as Element of [:NAT,NAT:] by A9;
consider a1,a2 be object such that
A12: a1 in NAT and
A13: a2 in NAT and
A14: a = [a1,a2] by ZFMISC_1:def 2;
reconsider a1,a2 as Nat by A12,A13;
not a1 in Segm i or not a2 in Segm j
proof
assume not (not a1 in Segm i or not a2 in Segm j);
then [a1,a2] in [:Segm i,Segm j:] by ZFMISC_1:def 2;
hence thesis by A14,A10,XBOOLE_0:def 5;
end;
then
A15: i <= a1 or j <= a2 by NAT_1:44;
t = s.(a1,a2) by A11,A14,BINOP_1:def 1;
hence t in B by A8,A15;
end;
hence ex n1,n2 be Nat st s.:([:NAT,NAT:] \ [:Segm n1,Segm n2:]) c= B;
end;
hence x in lim_filter(s,Frechet_Filter([:NAT,NAT:]))
by Th52;
end;
theorem Th56:
lim_filter(s,Frechet_Filter([:NAT,NAT:])) c=
lim_filter(s,<. all-square-uparrow.))
proof
<. all-square-uparrow .) = <. Frechet_Filter(NAT),Frechet_Filter(NAT).)
by Th34,CARDFIL2:19,Th35;
hence thesis by Th37,Th39,Th40;
end;
begin :: Metric space and double sequence
theorem Th57:
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}
proof
let M be non empty MetrSpace, p be Point of M,
x be Point of TopSpaceMetr(M),
s be Function of [:NAT,NAT:], TopSpaceMetr(M);
assume
A1: x = p;
x in lim_filter(s,<. Frechet_Filter(NAT),Frechet_Filter(NAT).)) iff
for m be non zero Nat ex n be Nat st for n1,n2 be Nat st n <= n1 &
n <= n2 holds
s.(n1,n2) in {q where q is Point of M: dist(p,q) < 1/m}
proof
hereby
assume
A2: x in lim_filter(s,<. Frechet_Filter(NAT),Frechet_Filter(NAT).));
hereby
let m be non zero Nat;
set B = {q where q is Point of M: dist(p,q) < 1/m};
A3: B = Ball(p,1/m) by METRIC_1:def 14;
ex y be Point of M st y = x &
Balls(x) = {Ball(y,1/m) where m is Nat: m <> 0 }
by FRECHET:def 1; then
A4: B in Balls(x) by A3,A1;
Balls(x) is basis of BOOL2F NeighborhoodSystem x by CARDFIL3:6;
hence ex n be Nat st for n1,n2 be Nat st n <= n1 & n <= n2 holds
s.(n1,n2) in {q where q is Point of M: dist(p,q) < 1/m}
by A2,A4,Th54;
end;
end;
assume
A5: for m be non zero Nat ex n be Nat st for n1,n2 be Nat st
n <= n1 & n <= n2 holds
s.(n1,n2) in {q where q is Point of M: dist(p,q) < 1/m};
A6: Balls(x) is basis of BOOL2F NeighborhoodSystem x by CARDFIL3:6;
for B being Element of Balls(x) holds ex n being Nat st
for n1,n2 being Nat st n <= n1 & n <= n2 holds s.(n1,n2) in B
proof
let B be Element of Balls(x);
consider y be Point of M such that
A7: y = x and
A8: Balls(x) = {Ball(y,1/m) where m is Nat: m <> 0 } by FRECHET:def 1;
B in Balls(x);
then consider m0 be Nat such that
A9: B = Ball(y,1/m0) and
A10: m0 <> 0 by A8;
consider n0 be Nat such that
A11: for n1,n2 be Nat st n0 <= n1 & n0 <= n2 holds s.(n1,n2) in
{q where q is Point of M: dist(p,q) < 1/m0} by A5,A10;
for n1,n2 be Nat st n0 <= n1 & n0 <= n2 holds s.(n1,n2) in B
proof
let n1,n2 be Nat;
assume n0 <= n1 & n0 <= n2;
then s.(n1,n2) in {q where q is Point of M: dist(p,q) < 1/m0} by A11;
hence thesis by A9,A1,A7,METRIC_1:def 14;
end;
hence thesis;
end;
hence x in lim_filter(s,<. Frechet_Filter(NAT),Frechet_Filter(NAT).))
by A6,Th54;
end;
hence thesis;
end;
theorem
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} by Th57;
begin :: One-dimensional Euclidean metric space and double sequence
reserve Rseq for Function of [:NAT,NAT:],REAL;
theorem
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}
proof
let x be Point of TopSpaceMetr(Euclid 1),
y be Point of Euclid 1,
cB be basis of BOOL2F NeighborhoodSystem x,
b be Element of cB;
assume that
A1: x = y and
A2: cB = Balls(x);
consider z be Point of Euclid 1 such that
A3: x = z and
A4: Balls(x) = {Ball(z,1/n) where n is Nat : n <> 0 } by FRECHET:def 1;
b in {Ball(z,1/n) where n is Nat : n <> 0 } by A2,A4;
then consider n be Nat such that
A5: b = Ball(z,1/n) and n <> 0;
Ball(y,1/n) = {q where q is Element of Euclid 1: dist(y,q) < 1/n}
by METRIC_1:def 14;
hence thesis by A5,A1,A3;
end;
definition
let s be Function of [:NAT,NAT:],REAL;
func #s -> Function of [:NAT,NAT:],R^1 equals s;
coherence;
end;
theorem
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)
proof
let s be Function of [:NAT,NAT:],TopSpaceMetr(Euclid 1),
y be Point of Euclid 1;
hereby
assume
A1: (s.:(square-uparrow n) c=
{q where q is Element of Euclid 1: dist(y,q) < 1/m});
now
let x be object;
assume
A2: x in s.:(square-uparrow n);
then consider yo be object such that
A3: yo in dom s and
yo in square-uparrow n and
A4: x = s.yo by FUNCT_1:def 6;
reconsider z = x as Element of Euclid 1 by A3,A4,FUNCT_2:5;
z in {q where q is Element of Euclid 1: dist(y,q) < 1/m} by A2,A1;
then consider q be Element of Euclid 1 such that
A5: z = q and
A6: dist(y,q) < 1/m;
reconsider yr1 = y as Point of Euclid 1;
yr1 in 1-tuples_on REAL;
then yr1 in the set of all <*r*> where r is Element of REAL
by FINSEQ_2:96;
then consider ry be Element of REAL such that
A8: yr1 = <*ry*>;
reconsider zr1 = z as Point of Euclid 1;
zr1 in 1-tuples_on REAL;
then zr1 in the set of all <*r*> where r is Element of REAL
by FINSEQ_2:96;
then consider rx be Element of REAL such that
A9: zr1 = <*rx*>;
|.ry - rx.| < 1/m by A5,A6,A8,A9,Th8;
hence ex rx,ry be Real st x = <*rx*> & y = <*ry*> & |.ry-rx.| < 1/m
by A8,A9;
end;
hence for x be object st x in s.:(square-uparrow n) holds
ex rx,ry be Real st x = <*rx*> & y = <*ry*> & |.ry - rx.| < 1/m;
end;
assume
A10: for x be object st x in s.:(square-uparrow n) holds
ex rx,ry be Real st x = <*rx*> & y = <*ry*> & |.ry - rx.| < 1/m;
now
let t be object;
assume
A11: t in s.:(square-uparrow n);
then consider rx,ry be Real such that
A12: t = <*rx*> and
A13: y = <*ry*> and
A14: |.ry - rx.| < 1/m by A10;
consider yo be object such that
A15: yo in dom s and
yo in square-uparrow n and
A16: t = s.yo by A11,FUNCT_1:def 6;
reconsider q = t as Element of Euclid 1 by A15,A16,FUNCT_2:5;
dist(y,q) < 1/m by A12,A13,A14,Th8;
hence t in {q where q is Element of Euclid 1: dist(y,q) < 1/m};
end;
hence (s.:(square-uparrow n) c=
{q where q is Element of Euclid 1: dist(y,q) < 1/m});
end;
theorem Th58:
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)
proof
reconsider p = r as Point of RealSpace by XREAL_0:def 1;
(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) in {q where q is Point of RealSpace: dist(p,q) < 1/m}))
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)
proof
hereby
assume
A1: 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) in
{q where q is Point of RealSpace: dist(p,q) < 1/m});
now
let m be non zero Nat;
consider n0 be Nat such that
A2: for n1,n2 be Nat st n0 <= n1 & n0 <= n2 holds Rseq.(n1,n2) in
{q where q is Point of RealSpace: dist(p,q) < 1/m} by A1;
take n0;
for n1,n2 being Nat st n0 <= n1 & n0<= n2 holds
|. Rseq.(n1,n2) - r .| < 1/m
proof
let n1,n2 be Nat;
assume n0 <= n1 & n0 <= n2;
then Rseq.(n1,n2) in
{q where q is Point of RealSpace: dist(p,q) < 1/m} by A2;
then consider q be Point of RealSpace such that
A3: Rseq.(n1,n2) = q and
A4: dist(p,q) < 1/m;
reconsider qr = q as Real;
ex xr,yr being Real st p = xr & q = yr &
dist(p,q) = real_dist.(p,q) &
dist(p,q) = (Pitag_dist 1).(<*p*>,<*q*>) &
dist(p,q) = |.xr - yr.| by Th6;
hence |. Rseq.(n1,n2) - r .| < 1/m by A3,A4,COMPLEX1:60;
end;
hence for n1,n2 being Nat st n0 <= n1 & n0<= n2 holds
|. Rseq.(n1,n2) - r .| < 1/m;
end;
hence 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;
end;
assume
A5: 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;
now
let m be non zero Nat;
consider n0 being Nat such that
A6: for n1,n2 being Nat st n0 <= n1 & n0 <= n2 holds
|. Rseq.(n1,n2) - r .| < 1/m by A5;
now
take n0;
hereby
let n1,n2 be Nat;
assume n0 <= n1 & n0 <= n2; then
A7: |. Rseq.(n1,n2) - r .| < 1/m by A6;
reconsider m1 = n1, m2 = n2 as Element of NAT by ORDINAL1:def 12;
Rseq.(m1,m2) in the carrier of RealSpace;
then reconsider q = Rseq.(n1,n2) as Point of RealSpace;
consider xr,yr being Real such that
A8: p = xr and
A9: q = yr and
dist(p,q) = real_dist.(p,q) and
dist(p,q) = (Pitag_dist 1).(<*p*>,<*q*>) and
A10: dist(p,q) = |.xr - yr.| by Th6;
|.xr - yr.| < 1/m by A8,A9,A7,COMPLEX1:60;
hence Rseq.(n1,n2) in
{q where q is Point of RealSpace: dist(p,q) < 1/m} by A10;
end;
end;
hence ex n be Nat st for n1,n2 being Nat st n <= n1 & n <= n2 holds
Rseq.(n1,n2) in
{q where q is Point of RealSpace: dist(p,q) < 1/m};
end;
hence(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) in
{q where q is Point of RealSpace: dist(p,q) < 1/m}));
end;
hence thesis by Th57;
end;
begin :: Basic relations convergence in Pringsheim's sense and filter convergence
theorem Th59:
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}
proof
assume
A1: lim_filter( #Rseq,<. Frechet_Filter(NAT),Frechet_Filter(NAT).)) <> {};
reconsider s1 = Rseq as Function of [:NAT,NAT:],the carrier of R^1;
consider x be object such that
A2: lim_filter( #Rseq,<. Frechet_Filter(NAT),Frechet_Filter(NAT).)) = {x}
by A1,ZFMISC_1:131;
x in lim_filter( #Rseq,<. Frechet_Filter(NAT),Frechet_Filter(NAT).))
by A2,TARSKI:def 1;
hence thesis by A2;
end;
theorem Th60:
Rseq is P-convergent implies P-lim Rseq in
lim_filter( #Rseq,<. Frechet_Filter(NAT),Frechet_Filter(NAT).))
proof
assume
A1: Rseq is P-convergent;
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) - P-lim Rseq .| < 1/m
proof
let m be non zero Nat;
0/m < 1/m by XREAL_1:74;
hence thesis by A1,DBLSEQ_1:def 2;
end;
hence P-lim Rseq in
lim_filter( #Rseq,<. Frechet_Filter(NAT),Frechet_Filter(NAT).)) by Th58;
end;
theorem Th61:
Rseq is P-convergent iff
lim_filter( #Rseq,<. Frechet_Filter(NAT),Frechet_Filter(NAT).)) <> {}
proof
hereby
assume Rseq is P-convergent;
then consider x be Real such that
A1: for e be Real st 0 < e ex N be Nat st
for n,m be Nat st n >= N & m >= N holds |.Rseq.(n,m) - x.| < e;
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) - x .| < 1/m
proof
let m be non zero Nat;
0/m < 1/m by XREAL_1:74;
hence thesis by A1;
end;
hence lim_filter( #Rseq,<. Frechet_Filter(NAT),Frechet_Filter(NAT).))
<> {} by Th58;
end;
assume lim_filter( #Rseq,<. Frechet_Filter(NAT),Frechet_Filter(NAT).))
<> {};
then consider p be object such that
A2: p in lim_filter( #Rseq,<. Frechet_Filter(NAT),Frechet_Filter(NAT).))
by XBOOLE_0:def 1;
reconsider p as Real by A2;
ex p0 be Real st for e be Real st 0 < e ex N be Nat st for n,m be Nat st
n >= N & m >= N holds |.Rseq.(n,m) - p0.| < e
proof
take p;
hereby
let e be Real;
assume 0 < e;
then ex m st m is non zero & 1 / m < e by Th5;
then consider m0 be non zero Nat such that
m0 is non zero and
A3: 1 / m0 < e;
consider n0 being Nat such that
A4: for n1,n2 being Nat st n0 <= n1 & n0 <= n2 holds
|. Rseq.(n1,n2) - p .| < 1 / m0 by Th58,A2;
now
take N = n0;
hereby
let n,m be Nat;
assume n >= N & m >= N;
then |.Rseq.(n,m) - p.| < 1/m0 by A4;
hence |.Rseq.(n,m) - p.| < e by A3,XXREAL_0:2;
end;
end;
hence ex N be Nat st for n,m be Nat st n>=N & m>=N holds
|.Rseq.(n,m) - p.| < e;
end;
end;
hence Rseq is P-convergent;
end;
theorem Th62:
Rseq is P-convergent implies {P-lim Rseq} =
lim_filter( #Rseq,<. Frechet_Filter(NAT),Frechet_Filter(NAT).))
proof
assume Rseq is P-convergent; then
A1: P-lim Rseq in
lim_filter( #Rseq,<. Frechet_Filter(NAT),Frechet_Filter(NAT).)) by Th60;
then ex x be Real st
lim_filter( #Rseq,<. Frechet_Filter(NAT),Frechet_Filter(NAT).)) = {x}
by Th59;
hence {P-lim Rseq} =
lim_filter( #Rseq,<. Frechet_Filter(NAT),Frechet_Filter(NAT).))
by A1,TARSKI:def 1;
end;
theorem
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).))
by Th61,Th62;
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
:Def5: for m,n being Nat holds it.(m,n) = 1 / (m + 1);
existence
proof
defpred P[object,object] means ex r be Real,n1,n2 be Nat st
$1 = [n1,n2] & $2 = r & r = 1 / (n1 + 1);
A1: for x being object st x in [:NAT,NAT:] ex y be object st
y in REAL & P[x,y]
proof
let x be object;
assume x in [:NAT,NAT:];
then consider n1,n2 be object such that
A2: n1 in NAT and
A3: n2 in NAT and
A4: x = [n1,n2] by ZFMISC_1:def 2;
reconsider n1,n2 as Nat by A2,A3;
reconsider y = 1/(n1 + 1) as Real;
take y;
thus y in REAL by XREAL_0:def 1;
thus P[x,y] by A3,A4;
end;
consider f being Function of [:NAT,NAT:],REAL such that
A5: for x be object st x in [:NAT,NAT:] holds P[x,f.x]
from FUNCT_2:sch 1(A1);
now
let m,n be Nat;
m in NAT & n in NAT by ORDINAL1:def 12;
then [m,n] in [:NAT,NAT:] by ZFMISC_1:def 2;
then consider r be Real,n1,n2 be Nat such that
A6: [m,n] = [n1,n2] and
A7: f.([m,n]) = r and
A8: r = 1/(n1+1) by A5;
f.(m,n) = r by A7,BINOP_1:def 1
.= 1/(m+1) by A8,A6,XTUPLE_0:1;
hence f.(m,n) = 1/(m+1);
end;
hence thesis;
end;
uniqueness
proof
let F1,F2 be Function of [:NAT,NAT:],REAL such that
A1: for m,n be Nat holds F1.(m,n) = 1/(m+1) and
A2: for m,n be Nat holds F2.(m,n) = 1/(m+1);
now
dom F1 = [:NAT,NAT:] & dom F2 = [:NAT,NAT:] by FUNCT_2:def 1;
hence dom F1 = dom F2;
hereby
let x be object;
assume x in dom F1;
then consider n1,n2 be object such that
A4: n1 in NAT and
A5: n2 in NAT and
A6: x = [n1,n2] by ZFMISC_1:def 2;
reconsider n1,n2 as Nat by A4,A5;
thus F1.x = F1.(n1,n2) by A6,BINOP_1:def 1
.= 1/(n1+1) by A1
.= F2.(n1,n2) by A2
.= F2.x by A6,BINOP_1:def 1;
end;
end;
hence thesis by FUNCT_1:def 11;
end;
end;
theorem Th63:
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
proof
let m be non zero Nat;
now
let n1,n2 be Nat;
assume that
A1: m <= n1 and
m <= n2;
m + 0 < n1 + 1 by A1,XREAL_1:8;
then 1/(n1 + 1) < 1/m by XREAL_1:76;
then |.1/(n1 + 1) - 0.| < 1/m by ABSVALUE:def 1;
hence |.dblseq_ex_1.(n1,n2) - 0.| < 1/m by Def5;
end;
hence ex n being Nat st for n1,n2 being Nat st
n <= n1 & n <= n2 holds |. dblseq_ex_1.(n1,n2) - 0 .| < 1/m;
end;
theorem Th64:
0 in lim_filter( # dblseq_ex_1,<. Frechet_Filter(NAT),Frechet_Filter(NAT).))
by Th63,Th58;
theorem Th65:
lim_filter( #dblseq_ex_1,Frechet_Filter([:NAT,NAT:])) = {}
proof
assume lim_filter( #dblseq_ex_1,Frechet_Filter([:NAT,NAT:])) <> {}; then
lim_filter( #dblseq_ex_1,Frechet_Filter([:NAT,NAT:])) is non empty; then
consider x be object such that
A1: x in lim_filter( #dblseq_ex_1,Frechet_Filter([:NAT,NAT:]));
A2: lim_filter( #dblseq_ex_1,Frechet_Filter([:NAT,NAT:])) c=
lim_filter( #dblseq_ex_1,<. all-square-uparrow.)) by Th56;
A3: <. all-square-uparrow .) = <. Frechet_Filter(NAT),Frechet_Filter(NAT).)
by Th34,CARDFIL2:19,Th35;
then consider y being Real such that
A4: lim_filter( #dblseq_ex_1,<. Frechet_Filter(NAT),Frechet_Filter(NAT).))
= {y} by A1,A2,Th59;
y = 0 by A4,Th64; then
A5: x = 0 by A1,A2,A3,A4,TARSKI:def 1;
reconsider xp = 0 as Point of TopSpaceMetr(RealSpace) by Th64;
A6: Balls(xp) is basis of BOOL2F NeighborhoodSystem xp by CARDFIL3:6;
consider yr be Point of RealSpace such that
A7: yr = xp and
A8: Balls(xp) = {Ball(yr,1/n) where n is Nat: n <> 0} by FRECHET:def 1;
Ball(yr,1/2) in Balls(xp) by A8;
then consider i,j such that
A9: for m,n st i <= m or j <= n holds dblseq_ex_1.(m,n) in Ball(yr,1/2)
by A6,A5,A1,Th55;
dblseq_ex_1.(0,j) in Ball(yr,1/2) by A9;
then dblseq_ex_1.(0,j) in ].yr - 1/2,yr + 1/2.[ by FRECHET:7;
then 1/(0+1) in ].yr - 1/2,yr + 1/2.[ by Def5;
hence thesis by A7,XXREAL_1:4;
end;
theorem
lim_filter( #dblseq_ex_1,<. Frechet_Filter(NAT),Frechet_Filter(NAT).))
<> lim_filter( #dblseq_ex_1,Frechet_Filter([:NAT,NAT:]))
by Th63,Th58,Th65;
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
A1: for x being Element of X2 holds lim_filter(ProjMap2(f,x),cF1) <> {};
func lim_in_cod1(f,cF1) -> Function of X2,Y means :Def6:
(for x being Element of X2 holds {it.x} = lim_filter(ProjMap2(f,x),cF1));
existence
proof
defpred P[object,object] means ex x be Element of X2,
y be Element of Y st x = $1 & y = $2 &
$2 in lim_filter(ProjMap2(f,x),cF1);
A2: for x being object st x in X2 ex y being object st
y in the carrier of Y & P[x,y]
proof
let x be object;
assume x in X2;
then reconsider x2 = x as Element of X2;
lim_filter(ProjMap2(f,x2),cF1) is non empty by A1;
then consider y be object such that
A3: y in lim_filter(ProjMap2(f,x2),cF1);
take y;
thus y in the carrier of Y by A3;
thus P[x,y] by A3;
end;
consider g1 being Function of X2,the carrier of Y such that
A4: for x being object st x in X2 holds P[x,g1.x] from FUNCT_2:sch 1(A2);
reconsider g2 = g1 as Function of X2,Y;
take g2;
hereby
let x be Element of X2;
P[x,g2.x] by A4;
then consider x2 be Element of X2, y1 be Element of Y such that
A5: x = x2 and
A6: g2.x = y1 and
A7: y1 in lim_filter(ProjMap2(f,x2),cF1);
lim_filter(ProjMap2(f,x),cF1) is non empty trivial by A1;
then ex z be object st lim_filter(ProjMap2(f,x),cF1) = {z}
by ZFMISC_1:131;
hence {g2.x} = lim_filter(ProjMap2(f,x),cF1) by A5,A6,A7,TARSKI:def 1;
end;
end;
uniqueness
proof
let g1,g2 be Function of X2,Y such that
A1: for x be Element of X2 holds {g1.x} = lim_filter(ProjMap2(f,x),cF1) and
A2: for x be Element of X2 holds {g2.x} = lim_filter(ProjMap2(f,x),cF1);
now
let x be Element of X2;
{g1.x} = lim_filter(ProjMap2(f,x),cF1) by A1;
then {g1.x} = {g2.x} by A2;
hence g1.x = g2.x by ZFMISC_1:3;
end;
hence g1 = g2 by FUNCT_2:def 8;
end;
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
A1: for x being Element of X1 holds lim_filter(ProjMap1(f,x),cF2) <> {};
func lim_in_cod2(f,cF2) -> Function of X1,Y means
:Def7:
(for x being Element of X1 holds {it.x} = lim_filter(ProjMap1(f,x),cF2));
existence
proof
defpred P[object,object] means ex x be Element of X1,
y be Element of Y st x = $1 & y = $2 &
$2 in lim_filter(ProjMap1(f,x),cF2);
A2: for x being object st x in X1 ex y being object st
y in the carrier of Y & P[x,y]
proof
let x be object;
assume x in X1;
then reconsider x1 = x as Element of X1;
lim_filter(ProjMap1(f,x1),cF2) is non empty by A1;
then consider y be object such that
A3: y in lim_filter(ProjMap1(f,x1),cF2);
take y;
thus y in the carrier of Y by A3;
thus P[x,y] by A3;
end;
consider g1 being Function of X1,the carrier of Y such that
A4: for x being object st x in X1 holds P[x,g1.x] from FUNCT_2:sch 1(A2);
reconsider g2 = g1 as Function of X1,Y;
take g2;
hereby
let x be Element of X1;
P[x,g2.x] by A4;
then consider x1 be Element of X1, y1 be Element of Y such that
A5: x = x1 and
A6: g2.x = y1 and
A7: y1 in lim_filter(ProjMap1(f,x1),cF2);
lim_filter(ProjMap1(f,x),cF2) is non empty trivial by A1;
then ex z be object st lim_filter(ProjMap1(f,x),cF2) = {z}
by ZFMISC_1:131;
hence {g2.x} = lim_filter(ProjMap1(f,x),cF2) by A5,A6,A7,TARSKI:def 1;
end;
end;
uniqueness
proof
let g1,g2 be Function of X1,Y such that
A1: for x be Element of X1 holds {g1.x} = lim_filter(ProjMap1(f,x),cF2) and
A2: for x be Element of X1 holds {g2.x} = lim_filter(ProjMap1(f,x),cF2);
now
let x be Element of X1;
{g1.x} = lim_filter(ProjMap1(f,x),cF2) by A1;
then {g1.x} = {g2.x} by A2;
hence g1.x = g2.x by ZFMISC_1:3;
end;
hence g1 = g2 by FUNCT_2:def 8;
end;
end;
theorem
for f being Function of X,REAL holds f is Function of X, R^1;
theorem
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 Th70:
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
proof
assume that
A1: f = seq and
A2: lim_f f <> {};
consider x be object such that
A3: x in lim_f f by A2, XBOOLE_0:def 1;
reconsider y = x as Point of TopSpaceMetr(RealSpace) by A3;
reconsider z = y as Real;
A4: Balls(y) is basis of BOOL2F NeighborhoodSystem y by CARDFIL3:6;
consider yr be Point of RealSpace such that
A5: yr = y and
A6: Balls(y) = {Ball(yr,1/n) where n is Nat: n <> 0} by FRECHET:def 1;
A7: for p be Real st 0 < p holds ex n be Nat st for m be Nat st n <= m holds
|.seq.m - z.| < p
proof
now
let p be Real;
assume 0 < p;
then consider M be Nat such that
A8: M is non zero and
A9: 1 / M < p by Th5;
now
Ball(yr,1/M) in Balls(y) by A8,A6;
then consider i be Element of OrderedNAT such that
A10: for j be Element of OrderedNAT st i <= j holds f.j in Ball(yr,1/M)
by A4,A3,CARDFIL2:84;
reconsider i0 = i as Nat;
take i0;
let m be Nat;
assume
A11: i0 <= m;
reconsider m0 = m as Element of OrderedNAT by ORDINAL1:def 12;
m0 in {x where x is Element of NAT:ex p0 be Element of NAT st
i0 = p0 & p0 <= x} by A11;
then m0 in uparrow i by CARDFIL2:50;
then f.m0 in Ball(yr,1/M) by A10,WAYBEL_0:18;
then f.m0 in ].yr - 1/M, yr + 1/M.[ by FRECHET:7; then
A12: yr - 1/M < seq.m0 < yr + 1/M by A1,XXREAL_1:4;
yr - p < yr - 1/M & yr + 1/M < yr + p by A9,XREAL_1:8,XREAL_1:15;
then yr - p < seq.m0 < yr + p by A12,XXREAL_0:2;
then seq.m0 in ].yr - p,yr + p.[ by XXREAL_1:4;
then f.m0 in Ball(yr,p) by A1,FRECHET:7;
then f.m0 in {q where q is Element of RealSpace:dist(yr,q) < p}
by METRIC_1:def 14;
then consider q0 be Element of RealSpace such that
A13: f.m0 = q0 and
A14: dist(yr,q0) < p;
reconsider g2 = yr as Point of RealSpace;
ex x1r,y1r being Real st
q0 = x1r &
g2 = y1r &
dist(q0,g2) = real_dist.(q0,g2) &
dist(q0,g2) = (Pitag_dist 1).(<*q0*>,<*g2*>) &
dist(q0,g2) = |.x1r - y1r.| by Th6;
hence |.seq.m - z.| < p by A14,A1,A5,A13;
end;
hence ex n be Nat st for m be Nat st n <= m holds |.seq.m - z.| < p;
end;
hence thesis;
end;
hence seq is convergent by SEQ_2:def 6;
thus ex z be Real st z in lim_f f & for p be Real st 0 < p holds
ex n be Nat st for m be Nat st n <= m holds |.seq.m - z.| < p
by A3,A7;
end;
theorem Th71:
f = seq & lim_f f <> {} implies lim_f f = {lim seq}
proof
assume that
A1: f = seq and
A2: lim_f f <> {};
consider x be object such that
A3: x in lim_f f by A2, XBOOLE_0:def 1;
reconsider y = x as Point of R^1 by A3;
consider u be object such that
A4: lim_f f = {u} by A3,ZFMISC_1:131;
lim_f f = {lim seq}
proof
lim_f f c= {lim seq}
proof
let t be object;
assume
A5: t in lim_f f;
then reconsider t1 = t as Real;
A6: seq is convergent &
ex z being Real st z in lim_f f & for p being Real st 0 < p holds
ex n be Nat st for m be Nat st n <= m holds |.seq.m - z.| < p
by A1,A2,Th70;
consider z being Real such that
A7: z in lim_f f and
A8: for p being Real st 0 < p holds ex n be Nat st for m be Nat st
n <= m holds |.seq.m - z.| < p by A1,A2,Th70;
t = u & z = u by A5,A7,A4,TARSKI:def 1;
then t1 = lim seq by A8,A6,SEQ_2:def 7;
hence thesis by TARSKI:def 1;
end;
hence thesis by A4,ZFMISC_1:3;
end;
hence thesis;
end;
theorem
for f being Function of [#]OrderedNAT,T for s being sequence of T st
f = s holds lim_f f = lim_f s by CARDFIL2:54;
theorem
for f being Function of [#]OrderedNAT,T for g being Function of NAT,T st
f = g holds lim_f f = lim_f g by CARDFIL2:54;
theorem Th72:
for f being Function of NAT,R^1 st f = seq & lim_f f <> {} holds
lim_f f = {lim seq}
proof
let f be Function of NAT,R^1;
assume that
A1: f = seq and
A2: lim_f f <> {};
[#]OrderedNAT = NAT & the carrier of R^1 = REAL by STRUCT_0:def 3;
then reconsider f1 = f as Function of [#]OrderedNAT,R^1;
lim_f f = lim_f f1 by CARDFIL2:54;
hence thesis by A1,A2,Th71;
end;
theorem
(for x being Element of NAT holds
lim_filter(ProjMap2( #Rseq ,x),Frechet_Filter(NAT)) <> {})
iff
Rseq is convergent_in_cod1
proof
hereby
assume
A1: for x being Element of NAT holds
lim_filter(ProjMap2( #Rseq ,x),Frechet_Filter(NAT)) <> {};
now
let m be Element of NAT;
lim_filter(ProjMap2( #Rseq ,m),Frechet_Filter(NAT)) is non empty
by A1;
then consider r be Element of TopSpaceMetr(RealSpace) such that
A2: r in lim_filter(ProjMap2( #Rseq ,m),Frechet_Filter(NAT));
A3: r in lim_f ProjMap2( #Rseq ,m) by A2;
A4: Balls(r) is basis of BOOL2F NeighborhoodSystem r by CARDFIL3:6;
reconsider r1 = r as Real;
now
let e be Real;
assume 0 < e;
then consider m1 be Nat such that
A5: m1 is non zero and
A6: 1 / m1 < e by Th5;
consider y be Point of RealSpace such that
A7: y = r and
A8: Balls(r) = { Ball(y,1/n) where n is Nat: n <> 0 } by FRECHET:def 1;
A9: Ball(y,1/m1) c= Ball(y,e) by A6,PCOMPS_1:1;
Ball(y,1/m1) in Balls(r) by A8,A5;
then consider i be Nat such that
A10: for j be Nat st i <=j holds (ProjMap2( #Rseq,m)).j in Ball(y,1/m1)
by A4,A3,CARDFIL2:97;
thus ex N be Nat st for n be Nat st N <= n holds
|.ProjMap2(Rseq,m).n - r1.| < e
proof
take i;
let j be Nat;
assume i <= j;
then (ProjMap2( #Rseq,m)).j in Ball(y,e) by A9,A10;
then (ProjMap2( #Rseq,m)).j in ]. y - e,y + e .[ by FRECHET:7;
hence thesis by A7,FCONT_3:1;
end;
end;
hence ProjMap2(Rseq,m) is convergent by SEQ_2:def 6;
end;
hence Rseq is convergent_in_cod1;
end;
assume
A13: Rseq is convergent_in_cod1;
now
let x be Element of NAT;
consider r be Real such that
A14: for p be Real st 0 < p ex n st for m be Nat st n <= m holds
|.ProjMap2(Rseq,x).m - r.| < p by A13,SEQ_2:def 6;
reconsider r1 = r as Point of TopSpaceMetr(RealSpace) by XREAL_0:def 1;
A15: Balls(r1) is basis of BOOL2F NeighborhoodSystem r1 by CARDFIL3:6;
for b be Element of Balls(r1) holds ex i be Nat st for j be Nat st
i <= j holds ProjMap2( #Rseq,x).j in b
proof
let b be Element of Balls(r1);
consider y be Point of RealSpace such that
A16: y = r1 and
A17: Balls(r1) = { Ball(y,1/n) where n is Nat: n <> 0 } by FRECHET:def 1;
b in { Ball(y,1/n) where n is Nat: n <> 0 } by A17;
then consider n0 be Nat such that
A18: b = Ball(y,1/n0) and
A19: n0 <> 0;
0 < n0 & 0 * n0 < 1 by A19;
then consider n1 be Nat such that
A20: for m be Nat st n1 <= m holds |.ProjMap2(Rseq,x).m - r.| < 1/n0
by A14,XREAL_1:81;
now
take n1;
hereby
let j be Nat;
assume n1 <= j; then
A21: |.ProjMap2(Rseq,x).j - r.| < 1/n0 by A20;
ProjMap2(Rseq,x).j = r + (ProjMap2(Rseq,x).j - r);
then ProjMap2(Rseq,x).j in ]. r - 1/n0, r + 1/n0.[
by A21,FCONT_3:3;
hence ProjMap2( #Rseq,x).j in b by A16,A18,FRECHET:7;
end;
end;
hence ex i be Nat st for j be Nat st i <= j holds
ProjMap2( #Rseq,x).j in b;
end;
then lim_f ProjMap2( #Rseq ,x) <> {} by A15,CARDFIL2:97;
hence lim_filter(ProjMap2( #Rseq ,x),Frechet_Filter(NAT)) <> {};
end;
hence thesis;
end;
theorem
(for x being Element of NAT holds
lim_filter(ProjMap1( #Rseq ,x),Frechet_Filter(NAT)) <> {})
iff
Rseq is convergent_in_cod2
proof
hereby
assume
A1: for x being Element of NAT holds
lim_filter(ProjMap1( #Rseq ,x),Frechet_Filter(NAT)) <> {};
now
let m be Element of NAT;
lim_filter(ProjMap1( #Rseq ,m),Frechet_Filter(NAT)) is non empty by A1;
then consider r be Element of TopSpaceMetr(RealSpace) such that
A2: r in lim_filter(ProjMap1( #Rseq ,m),Frechet_Filter(NAT));
A3: r in lim_f ProjMap1( #Rseq ,m) by A2;
A4: Balls(r) is basis of BOOL2F NeighborhoodSystem r by CARDFIL3:6;
reconsider r1 = r as Real;
now
let e be Real;
assume 0 < e;
then consider m1 be Nat such that
A5: m1 is non zero and
A6: 1 / m1 < e by Th5;
consider y be Point of RealSpace such that
A7: y = r and
A8: Balls(r) = { Ball(y,1/n) where n is Nat: n <> 0 } by FRECHET:def 1;
A9: Ball(y,1/m1) c= Ball(y,e) by A6,PCOMPS_1:1;
Ball(y,1/m1) in Balls(r) by A8,A5;
then consider i be Nat such that
A10: for j be Nat st i <=j holds (ProjMap1( #Rseq,m)).j in Ball(y,1/m1)
by A4,A3,CARDFIL2:97;
thus ex N be Nat st for n be Nat st N <= n holds
|.ProjMap1(Rseq,m).n - r1.| < e
proof
take i;
let j be Nat;
assume i <= j;
then (ProjMap1( #Rseq,m)).j in Ball(y,e) by A9,A10;
then (ProjMap1( #Rseq,m)).j in ]. y - e,y + e .[ by FRECHET:7;
hence thesis by A7,FCONT_3:1;
end;
end;
hence ProjMap1(Rseq,m) is convergent by SEQ_2:def 6;
end;
hence Rseq is convergent_in_cod2;
end;
assume
A11: Rseq is convergent_in_cod2;
now
let x be Element of NAT;
consider r be Real such that
A12: for p be Real st 0 < p ex n st for m be Nat st n <= m holds
|.ProjMap1(Rseq,x).m - r.| < p by A11,SEQ_2:def 6;
reconsider r1 = r as Point of TopSpaceMetr(RealSpace) by XREAL_0:def 1;
A13: Balls(r1) is basis of BOOL2F NeighborhoodSystem r1 by CARDFIL3:6;
for b be Element of Balls(r1) holds ex i be Nat st for j be Nat st
i <= j holds ProjMap1( #Rseq,x).j in b
proof
let b be Element of Balls(r1);
consider y be Point of RealSpace such that
A14: y = r1 and
A15: Balls(r1) = { Ball(y,1/n) where n is Nat: n <> 0 } by FRECHET:def 1;
b in { Ball(y,1/n) where n is Nat: n <> 0 } by A15;
then consider n0 be Nat such that
A16: b = Ball(y,1/n0) and
A17: n0 <> 0;
0 < n0 & 0 * n0 < 1 by A17;
then consider n1 be Nat such that
A18: for m be Nat st n1 <= m holds |.ProjMap1(Rseq,x).m - r.| < 1/n0
by A12,XREAL_1:81;
now
take n1;
hereby
let j be Nat;
assume n1 <= j; then
A19: |.ProjMap1(Rseq,x).j - r.| < 1/n0 by A18;
ProjMap1(Rseq,x).j = r + (ProjMap1(Rseq,x).j - r);
then ProjMap1(Rseq,x).j in ]. r - 1/n0, r + 1/n0.[
by A19,FCONT_3:3;
hence ProjMap1( #Rseq,x).j in b by A14,A16,FRECHET:7;
end;
end;
hence ex i be Nat st for j be Nat st i <= j holds
ProjMap1( #Rseq,x).j in b;
end;
then lim_f ProjMap1( #Rseq ,x) is non empty by A13,CARDFIL2:97;
hence lim_filter(ProjMap1( #Rseq ,x),Frechet_Filter(NAT)) is non empty;
end;
hence thesis;
end;
theorem Th73:
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)}
proof
let t be Element of NAT,
f be Function of [:NAT,NAT:],R^1;
let seq be Function of [:NAT,NAT:],REAL;
assume that
A1: f = seq and
A2: for x being Element of NAT holds
lim_filter(ProjMap1(f,x),Frechet_Filter(NAT)) <> {};
lim_filter(ProjMap1(f,t),Frechet_Filter(NAT)) is non empty trivial by A2;
then consider x be object such that
A3: lim_filter(ProjMap1(f,t),Frechet_Filter(NAT)) = {x} by ZFMISC_1:131;
reconsider f1 = ProjMap1(f,t) as Function of NAT,R^1;
reconsider seq1 = ProjMap1(seq,t) as Function of NAT,REAL;
lim_f f1 = {lim seq1} by A1,A3,Th72;
hence thesis;
end;
theorem Th74:
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)}
proof
let t be Element of NAT,
f be Function of [:NAT,NAT:],R^1;
let seq be Function of [:NAT,NAT:],REAL;
assume that
A1: f = seq and
A2: for x being Element of NAT holds
lim_filter(ProjMap2(f,x),Frechet_Filter(NAT)) <> {};
lim_filter(ProjMap2(f,t),Frechet_Filter(NAT)) is non empty trivial by A2;
then consider x be object such that
A3: lim_filter(ProjMap2(f,t),Frechet_Filter(NAT)) = {x} by ZFMISC_1:131;
reconsider f1 = ProjMap2(f,t) as Function of NAT,R^1;
reconsider seq1 = ProjMap2(seq,t) as Function of NAT,REAL;
lim_f f1 = {lim seq1} by A1,A3,Th72;
hence thesis;
end;
theorem
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
proof
let Y be Hausdorff non empty TopSpace,
f be Function of [:NAT,NAT:],Y;
assume that
A1: for x being Element of NAT holds
lim_filter(ProjMap2(f,x),Frechet_Filter(NAT)) <> {} and
A2: f = Rseq and
A3: Y = R^1;
now
dom lim_in_cod1(f,Frechet_Filter(NAT)) = NAT by FUNCT_2:def 1;
hence dom lim_in_cod1(f,Frechet_Filter(NAT))
= dom lim_in_cod1 Rseq by FUNCT_2:def 1;
thus for t be object st
t in dom lim_in_cod1(f,Frechet_Filter(NAT))
holds (lim_in_cod1(f,Frechet_Filter(NAT))).t
= (lim_in_cod1 Rseq).t
proof
let t be object;
assume t in dom lim_in_cod1(f,Frechet_Filter(NAT));
then reconsider t1 = t as Element of NAT;
A4: {(lim_in_cod1(f,Frechet_Filter(NAT))).t1}
= lim_filter(ProjMap2(f,t1),Frechet_Filter(NAT)) by A1,Def6;
lim_filter(ProjMap2(f,t1),Frechet_Filter(NAT))
= {lim ProjMap2(Rseq,t1)} by A1,A3,A2,Th74
.= {(lim_in_cod1 Rseq).t1} by DBLSEQ_1:def 5;
hence thesis by A4,ZFMISC_1:3;
end;
end;
hence thesis by FUNCT_1:def 11;
end;
theorem
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
proof
let Y be non empty Hausdorff TopSpace, f be Function of [:NAT,NAT:],Y;
assume that
A1: for x being Element of NAT holds
lim_filter(ProjMap1(f,x),Frechet_Filter(NAT)) <> {} and
A2: f = Rseq and
A3: Y = R^1;
now
dom lim_in_cod2(f,Frechet_Filter(NAT)) = NAT by FUNCT_2:def 1;
hence dom lim_in_cod2(f,Frechet_Filter(NAT))
= dom lim_in_cod2 Rseq by FUNCT_2:def 1;
thus for t be object st
t in dom lim_in_cod2(f,Frechet_Filter(NAT))
holds (lim_in_cod2(f,Frechet_Filter(NAT))).t
= (lim_in_cod2 Rseq).t
proof
let t be object;
assume t in dom lim_in_cod2(f,Frechet_Filter(NAT));
then reconsider t1 = t as Element of NAT;
A4: {(lim_in_cod2(f,Frechet_Filter(NAT))).t1}
= lim_filter(ProjMap1(f,t1),Frechet_Filter(NAT)) by A1,Def7;
lim_filter(ProjMap1(f,t1),Frechet_Filter(NAT))
= {lim ProjMap1(Rseq,t1)} by A1,A3,A2,Th73
.= {(lim_in_cod2 Rseq).t1} by DBLSEQ_1:def 6;
hence thesis by A4,ZFMISC_1:3;
end;
end;
hence lim_in_cod2(f,Frechet_Filter(NAT)) = lim_in_cod2 Rseq
by FUNCT_1:def 11;
end;
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
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
proof
assume that
A1: x in lim_filter(f,<.cF1,cF2.)) and
A2: <.cB1.) = cF1 and
A3: <.cB2.) = cF2;
reconsider FF = filter_image(f,<.cF1,cF2.)) as Filter of the carrier of Y;
let V be Subset of Y;
assume that
A4: V is open and
A5: x in V;
V in {M where M is Subset of Y: f"(M) in <.cF1,cF2.)}
by A1,A4,A5,CARDFIL2:80,WAYBEL_7:def 5;
then consider M be Subset of Y such that
A6: V = M and
A7: f"(M) in <.cF1,cF2.);
<.cF1,cF2.) = <.[:cB1,cB2:].) by A2,A3,Def1;
then consider B be Element of [:cB1,cB2:] such that
A8: B c= f"(M) by A7,CARDFIL2:def 8;
B in [:cB1,cB2:];
then consider B1 be Element of cB1, B2 be Element of cB2 such that
A9: B = [:B1,B2:];
take B1,B2;
A10: f.:([:B1,B2:]) c= f.:(f"(M)) by A8,A9,RELAT_1:123;
f.:(f"(M)) c= M by FUNCT_1:75;
hence thesis by A6,A10;
end;
theorem Th75:
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)
proof
assume that
A1: x in lim_filter(f,<.cF1,cF2.)) and
A2: <.cB1.) = cF1 and
A3: <.cB2.) = cF2;
reconsider FF = filter_image(f,<.cF1,cF2.)) as Filter of the carrier of Y;
let U be a_neighborhood of x;
assume U is closed;
x in Int(U) by CONNSP_2:def 1;
then Int(U) in {M where M is Subset of Y: f"(M) in <.cF1,cF2.)}
by A1,CARDFIL2:80,WAYBEL_7:def 5;
then consider M be Subset of Y such that
A4: Int(U) = M and
A5: f"(M) in <.cF1,cF2.);
<.cF1,cF2.) = <.[:cB1,cB2:].) by A2,A3,Def1;
then consider B be Element of [:cB1,cB2:] such that
A6: B c= f"(M) by A5,CARDFIL2:def 8;
B in [:cB1,cB2:];
then consider B1 be Element of cB1, B2 be Element of cB2 such that
A7: B = [:B1,B2:];
take B1,B2;
A8: f.:([:B1,B2:]) c= f.:(f"(M)) by A6,A7,RELAT_1:123;
f.:(f"(M)) c= M by FUNCT_1:75;
hence thesis by A4,A8;
end;
theorem
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)
proof
assume that
A1: x in lim_filter(f,<.cF1,cF2.)) and
A2: <.cB1.) = cF1 and
A3: <.cB2.) = cF2;
now
let U be a_neighborhood of x;
assume U is closed;
then consider B1 be Element of cB1,B2 be Element of cB2 such that
A4: f.:([:B1,B2:]) c= Int U by A1,A2,A3,Th75;
take B1,B2;
let y be Element of B1;
[:{y},B2:] c= [:B1,B2:] by ZFMISC_1:95;
then f.:([:{y},B2:]) c=f.:([:B1,B2:]) by RELAT_1:125;
hence f.:([:{y},B2:]) c= Int U by A4;
end;
hence thesis;
end;
theorem Th76:
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
proof
assume that
A1: x in lim_filter(f,<.cF1,cF2.)) and
A2: <.cB1.) = cF1 and
A3: <.cB2.) = cF2;
let U be a_neighborhood of x;
assume U is closed;
then consider B1 be Element of cB1,B2 be Element of cB2 such that
A4: f.:([:B1,B2:]) c= Int U by A1,A2,A3,Th75;
take B1,B2;
A5: for y be Element of B1 holds f.:([:{y},B2:]) c= Int U
proof
let y be Element of B1;
[:{y},B2:] c= [:B1,B2:] by ZFMISC_1:95;
then f.:([:{y},B2:]) c=f.:([:B1,B2:]) by RELAT_1:125;
hence thesis by A4;
end;
A6: for z be Element of B1, y be Element of Y st
y in lim_filter(ProjMap1(f,z),cF2)
holds filter_image(ProjMap1(f,z),cF2) is proper Filter of BoolePoset [#]Y
& Int U in filter_image(ProjMap1(f,z),cF2) &
y is_a_cluster_point_of filter_image(ProjMap1(f,z),cF2),Y
proof
let z be Element of B1,y be Element of Y;
assume
A7: y in lim_filter(ProjMap1(f,z),cF2);
filter_image(ProjMap1(f,z),cF2) is Filter of [#]Y by STRUCT_0:def 3;
hence filter_image(ProjMap1(f,z),cF2) is
proper Filter of BoolePoset [#]Y by Th17;
A8: ProjMap1(f,z)"(Int U) is Subset of X2
proof
dom ProjMap1(f,z) = X2 by FUNCT_2:def 1;
hence thesis by RELAT_1:132;
end;
A9: for z be Element of B1 holds ProjMap1(f,z).:B2 c= Int U
proof
let z be Element of B1;
let t be object;
assume t in ProjMap1(f,z).:B2;
then consider u be object such that
u in dom ProjMap1(f,z) and
A10: u in B2 and
A11: t = ProjMap1(f,z).u by FUNCT_1:def 6;
ProjMap1(f,z).u = f.(z,u) by A10,MESFUNC9:def 6; then
A12: t = f.([z,u]) by A11,BINOP_1:def 1;
now
[z,u] in [:X1,X2:] by A10,ZFMISC_1:def 2;
hence [z,u] in dom f by FUNCT_2:def 1;
z in {z} & u in B2 by TARSKI:def 1,A10;
hence [z,u] in [:{z},B2:] by ZFMISC_1:def 2;
end;
then
A13: t in f.:([:{z},B2:]) by A12,FUNCT_1:def 6;
f.:([:{z},B2:]) c= Int U by A5;
hence thesis by A13;
end;
thus Int U in filter_image(ProjMap1(f,z),cF2) &
y is_a_cluster_point_of filter_image(ProjMap1(f,z),cF2),Y
proof
ProjMap1(f,z).:B2 c= Int U by A9;
then B2 c= ProjMap1(f,z)"(Int U) by FUNCT_2:95;
then ProjMap1(f,z)"(Int U) in cF2 by A3,A8,CARDFIL2:def 8;
hence Int U in filter_image(ProjMap1(f,z),cF2);
thus thesis by A7,Th19;
end;
end;
for z be Element of B1, y be Element of Y st
y in lim_filter(ProjMap1(f,z),cF2) holds y in Cl Int U
proof
let z be Element of B1, y be Element of Y;
assume y in lim_filter(ProjMap1(f,z),cF2);
then filter_image(ProjMap1(f,z),cF2) is
proper Filter of BoolePoset [#]Y &
Int U in filter_image(ProjMap1(f,z),cF2) &
y is_a_cluster_point_of filter_image(ProjMap1(f,z),cF2),Y by A6;
hence thesis by YELLOW19:25;
end;
hence thesis;
end;
theorem Th77:
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
proof
assume that
A1: x in lim_filter(f,<.cF1,cF2.)) and
A2: <.cB1.) = cF1 and
A3: <.cB2.) = cF2;
let U be a_neighborhood of x;
assume U is closed;
then consider B1 be Element of cB1,B2 be Element of cB2 such that
A4: f.:([:B1,B2:]) c= Int U by A1,A2,A3,Th75;
take B1,B2;
A5: for y be Element of B2 holds f.:([:B1,{y}:]) c= Int U
proof
let y be Element of B2;
[:B1,{y}:] c= [:B1,B2:] by ZFMISC_1:95;
then f.:([:B1,{y}:]) c=f.:([:B1,B2:]) by RELAT_1:125;
hence thesis by A4;
end;
A6: for z be Element of B2, y be Element of Y st
y in lim_filter(ProjMap2(f,z),cF1)
holds filter_image(ProjMap2(f,z),cF1) is
proper Filter of BoolePoset [#]Y &
Int U in filter_image(ProjMap2(f,z),cF1) &
y is_a_cluster_point_of filter_image(ProjMap2(f,z),cF1),Y
proof
let z be Element of B2,y be Element of Y;
assume
A7: y in lim_filter(ProjMap2(f,z),cF1);
filter_image(ProjMap2(f,z),cF1) is Filter of [#]Y by STRUCT_0:def 3;
hence filter_image(ProjMap2(f,z),cF1) is
proper Filter of BoolePoset [#]Y by Th17;
A8: ProjMap2(f,z)"(Int U) is Subset of X1
proof
dom ProjMap2(f,z) = X1 by FUNCT_2:def 1;
hence thesis by RELAT_1:132;
end;
A9: for z be Element of B2 holds ProjMap2(f,z).:B1 c= Int U
proof
let z be Element of B2;
let t be object;
assume t in ProjMap2(f,z).:B1;
then consider u be object such that
u in dom ProjMap2(f,z) and
A10: u in B1 and
A11: t = ProjMap2(f,z).u by FUNCT_1:def 6;
ProjMap2(f,z).u = f.(u,z) by A10,MESFUNC9:def 7; then
A12: t = f.([u,z]) by A11,BINOP_1:def 1;
now
[u,z] in [:X1,X2:] by A10,ZFMISC_1:def 2;
hence [u,z] in dom f by FUNCT_2:def 1;
z in {z} & u in B1 by TARSKI:def 1,A10;
hence [u,z] in [:B1,{z}:] by ZFMISC_1:def 2;
end;
then VALB:t in f.:([:B1,{z}:]) by A12,FUNCT_1:def 6;
f.:([:B1,{z}:]) c= Int U by A5;
hence thesis by VALB;
end;
thus Int U in filter_image(ProjMap2(f,z),cF1) &
y is_a_cluster_point_of filter_image(ProjMap2(f,z),cF1),Y
proof
ProjMap2(f,z).:B1 c= Int U by A9;
then B1 c= ProjMap2(f,z)"(Int U) by FUNCT_2:95;
then ProjMap2(f,z)"(Int U) in cF1 by A2,A8,CARDFIL2:def 8;
hence Int U in filter_image(ProjMap2(f,z),cF1);
thus thesis by A7,Th19;
end;
end;
for z be Element of B2, y be Element of Y st
y in lim_filter(ProjMap2(f,z),cF1) holds y in Cl Int U
proof
let z be Element of B2, y be Element of Y;
assume y in lim_filter(ProjMap2(f,z),cF1);
then filter_image(ProjMap2(f,z),cF1) is
proper Filter of BoolePoset [#]Y &
Int U in filter_image(ProjMap2(f,z),cF1) &
y is_a_cluster_point_of filter_image(ProjMap2(f,z),cF1),Y by A6;
hence thesis by YELLOW19:25;
end;
hence thesis;
end;
theorem Th78:
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)
proof
let Y be Hausdorff regular non empty TopSpace,
f be Function of [:X1,X2:],Y;
assume
A1: for x1 being Element of X2 holds lim_filter(ProjMap2(f,x1),cF1) <> {};
now
let y0 be object;
assume
A2: y0 in lim_filter(f,<.cF1,cF2.));
then reconsider y = y0 as Element of Y;
consider cB1 be filter_base of X1 such that
cB1 = cF1 and
A3: <.cB1.) = cF1 by Th18;
consider cB2 be filter_base of X2 such that
cB2 = cF2 and
A4: <.cB2.) = cF2 by Th18;
A5: for U being a_neighborhood of y st U is closed holds
ex B1 be Element of cB1, B2 be Element of cB2 st
for z be Element of B2 holds lim_filter(ProjMap2(f,z),cF1) c= Cl Int U
proof
let U be a_neighborhood of y;
assume U is closed;
then consider B1 be Element of cB1, B2 be Element of cB2 such that
A6: for z be Element of X2, t be Element of Y st z in B2 &
t in lim_filter(ProjMap2(f,z),cF1) holds t in Cl Int U
by A3,A4,A2,Th77;
take B1,B2;
thus thesis by A6;
end;
NeighborhoodSystem y c= filter_image(lim_in_cod1(f,cF1),cF2)
proof
let n be object;
assume n in NeighborhoodSystem y;
then n in the set of all A where A is a_neighborhood of y
by YELLOW19:def 1;
then consider A be a_neighborhood of y such that
A7: n = A;
y in Int A by CONNSP_2:def 1;
then consider Q be Subset of Y such that
A8: Q is closed and
A9: Q c= A and
A10: y in Int Q by YELLOW_8:27;
Q is a_neighborhood of y by A10,CONNSP_2:def 1;
then consider B1 be Element of cB1,B2 be Element of cB2 such that
A11: for z be Element of B2 holds
lim_filter(ProjMap2(f,z),cF1) c= Cl Int Q by A8,A5;
A12: Cl Q = Q by PRE_TOPC:18,A8,TOPS_1:5;
A13: Cl Int Q c= Cl Q by TOPS_1:16,PRE_TOPC:19;
reconsider n1 = n as Subset of Y by A7;
now
lim_in_cod1(f,cF1).:B2 c= n1
proof
let t be object;
assume t in lim_in_cod1(f,cF1).:B2;
then consider u be object such that
A14: u in dom lim_in_cod1(f,cF1) and
A15: u in B2 and
A16: t = lim_in_cod1(f,cF1).u by FUNCT_1:def 6;
reconsider u1 = u as Element of X2 by A14;
{t} = lim_filter(ProjMap2(f,u1),cF1) by A16,A1,Def6; then
A17: t in lim_filter(ProjMap2(f,u1),cF1) by TARSKI:def 1;
lim_filter(ProjMap2(f,u1),cF1) c= Cl Int Q by A11,A15;
hence thesis by A7,A17,A13,A12,A9;
end;
hence B2 c= lim_in_cod1(f,cF1)"(n1) by FUNCT_2:95;
dom lim_in_cod1(f,cF1) = X2 by FUNCT_2:def 1;
hence lim_in_cod1(f,cF1)"(n1) is Subset of X2 by RELAT_1:132;
end;
then lim_in_cod1(f,cF1)"(n1) in cF2 by A4,CARDFIL2:def 8;
hence thesis;
end;
then filter_image(lim_in_cod1(f,cF1),cF2)
is_filter-finer_than NeighborhoodSystem y;
hence y0 in lim_filter(lim_in_cod1(f,cF1),cF2);
end;
hence thesis;
end;
theorem Th79:
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)
proof
let Y be Hausdorff regular non empty TopSpace,
f be Function of [:X1,X2:],Y;
assume
A1: for x1 being Element of X1 holds lim_filter(ProjMap1(f,x1),cF2) <> {};
now
let y0 be object;
assume
A2: y0 in lim_filter(f,<.cF1,cF2.));
then reconsider y = y0 as Element of Y;
consider cB1 be filter_base of X1 such that
cB1 = cF1 and
A3: <.cB1.) = cF1 by Th18;
consider cB2 be filter_base of X2 such that
cB2 = cF2 and
A4: <.cB2.) = cF2 by Th18;
A5: for U being a_neighborhood of y st U is closed holds
ex B1 be Element of cB1, B2 be Element of cB2 st
for z be Element of B1 holds lim_filter(ProjMap1(f,z),cF2) c= Cl Int U
proof
let U be a_neighborhood of y;
assume U is closed;
then consider B1 be Element of cB1, B2 be Element of cB2 such that
A6: for z be Element of X1, t be Element of Y st z in B1 &
t in lim_filter(ProjMap1(f,z),cF2) holds t in Cl Int U
by A3,A4,A2,Th76;
take B1,B2;
thus thesis by A6;
end;
NeighborhoodSystem y c= filter_image(lim_in_cod2(f,cF2),cF1)
proof
let n be object;
assume n in NeighborhoodSystem y;
then n in the set of all A where A is a_neighborhood of y
by YELLOW19:def 1;
then consider A be a_neighborhood of y such that
A7: n = A;
y in Int A by CONNSP_2:def 1;
then consider Q be Subset of Y such that
A8: Q is closed and
A9: Q c= A and
A10: y in Int Q by YELLOW_8:27;
Q is a_neighborhood of y by A10,CONNSP_2:def 1;
then consider B1 be Element of cB1,B2 be Element of cB2 such that
A11: for z be Element of B1 holds
lim_filter(ProjMap1(f,z),cF2) c= Cl Int Q by A8,A5;
A12: Cl Q = Q by PRE_TOPC:18,A8,TOPS_1:5;
A13: Cl Int Q c= Cl Q by TOPS_1:16,PRE_TOPC:19;
reconsider n1 = n as Subset of Y by A7;
now
lim_in_cod2(f,cF2).:B1 c= n1
proof
let t be object;
assume t in lim_in_cod2(f,cF2).:B1;
then consider u be object such that
A14: u in dom lim_in_cod2(f,cF2) and
A15: u in B1 and
A16: t = lim_in_cod2(f,cF2).u by FUNCT_1:def 6;
reconsider u1 = u as Element of X1 by A14;
{t} = lim_filter(ProjMap1(f,u1),cF2) by A16,A1,Def7; then
A17: t in lim_filter(ProjMap1(f,u1),cF2) by TARSKI:def 1;
lim_filter(ProjMap1(f,u1),cF2) c= Cl Int Q by A11,A15;
hence thesis by A7,A17,A13,A12,A9;
end;
hence B1 c= lim_in_cod2(f,cF2)"(n1) by FUNCT_2:95;
dom lim_in_cod2(f,cF2) = X1 by FUNCT_2:def 1;
hence lim_in_cod2(f,cF2)"(n1) is Subset of X1 by RELAT_1:132;
end;
then lim_in_cod2(f,cF2)"(n1) in cF1 by A3,CARDFIL2:def 8;
hence thesis;
end;
then filter_image(lim_in_cod2(f,cF2),cF1)
is_filter-finer_than NeighborhoodSystem y;
hence y0 in lim_filter(lim_in_cod2(f,cF2),cF1);
end;
hence thesis;
end;
theorem Th80:
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)
proof
let X1,X2 be non empty set,
cF1 be Filter of X1,
cF2 be Filter of X2,
Y be Hausdorff regular non empty TopSpace,
f be Function of [:X1,X2:],Y;
assume that
A1: lim_filter(f,<.cF1,cF2.)) <> {} and
A2: for x being Element of X1 holds lim_filter(ProjMap1(f,x),cF2) <> {};
consider y be object such that
A3: lim_filter(f,<.cF1,cF2.)) = {y} by A1,ZFMISC_1:131;
A4: y in lim_filter(f,<.cF1,cF2.)) by A3,TARSKI:def 1;
A5: lim_filter(f,<.cF1,cF2.)) c= lim_filter(lim_in_cod2(f,cF2),cF1)
by A2,Th79;
lim_filter(lim_in_cod2(f,cF2),cF1) is non empty trivial by A3,A5;
then ex z be object st lim_filter(lim_in_cod2(f,cF2),cF1) = {z}
by ZFMISC_1:131;
hence thesis by A3,A5,A4,TARSKI:def 1;
end;
theorem Th81:
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)
proof
let X1,X2 be non empty set,
cF1 be Filter of X1,
cF2 be Filter of X2,
Y be Hausdorff regular non empty TopSpace,
f be Function of [:X1,X2:],Y;
assume that
A1: lim_filter(f,<.cF1,cF2.)) <> {} and
A2: for x being Element of X2 holds lim_filter(ProjMap2(f,x),cF1) <> {};
consider y be object such that
A3: lim_filter(f,<.cF1,cF2.)) = {y} by A1,ZFMISC_1:131;
A4: lim_filter(f,<.cF1,cF2.)) c= lim_filter(lim_in_cod1(f,cF1),cF2)
by A2,Th78;
A5: y in lim_filter(f,<.cF1,cF2.)) by A3,TARSKI:def 1;
lim_filter(lim_in_cod1(f,cF1),cF2) is non empty trivial by A4,A3;
then ex z be object st lim_filter(lim_in_cod1(f,cF1),cF2) = {z}
by ZFMISC_1:131;
hence thesis by A3,A5,A4,TARSKI:def 1;
end;
theorem
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)
proof
let X1,X2 be non empty set,
cF1 be Filter of X1,
cF2 be Filter of X2,
Y be Hausdorff regular non empty TopSpace,
f be Function of [:X1,X2:],Y;
assume that
A1: lim_filter(f,<.cF1,cF2.)) <> {} and
A2: (for x being Element of X1 holds
lim_filter(ProjMap1(f,x),cF2) <> {}) and
A3: (for x being Element of X2 holds
lim_filter(ProjMap2(f,x),cF1) <> {});
lim_filter(f,<.cF1,cF2.)) = lim_filter(lim_in_cod1(f,cF1),cF2)
by A1,A3,Th81;
hence thesis by A1,A2,Th80;
end;