:: Double Sequences and Iterated Limits in Regular Space
:: by Roland Coghetto
::
:: Received June 30, 2016
:: Copyright (c) 2016-2021 Association of Mizar Users


theorem Th1: :: CARDFIL4:1
for X, Z being set
for W being finite Subset of X st X \ W c= Z holds
X \ Z is finite
proof end;

theorem Th2: :: CARDFIL4:2
for X, Z being set st Z c= X & X \ Z is finite holds
ex W being finite Subset of X st X \ W = Z
proof end;

theorem Th3: :: CARDFIL4:3
for X1, X2 being set
for S1 being Subset-Family of X1
for S2 being Subset-Family of X2 holds { s where s is Subset of [:X1,X2:] : ex s1, s2 being set st
( s1 in S1 & s2 in S2 & s = [:s1,s2:] ) } is Subset-Family of [:X1,X2:]
proof end;

theorem Th4: :: CARDFIL4:4
for x being object
for X, Y being set st x in [:X,Y:] holds
x is pair
proof end;

theorem Th5: :: CARDFIL4:5
for r being Real st 0 < r holds
ex m being Nat st
( not m is zero & 1 / m < r )
proof end;

theorem Th6: :: CARDFIL4:6
for x, y being Point of RealSpace ex xr, yr being Real st
( x = xr & y = yr & dist (x,y) = real_dist . (x,y) & dist (x,y) = (Pitag_dist 1) . (<*x*>,<*y*>) & dist (x,y) = |.(xr - yr).| )
proof end;

theorem Th7: :: CARDFIL4:7
for x, y being Point of (TopSpaceMetr (Euclid 1)) ex x1, y1 being Point of RealSpace ex 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 end;

theorem Th8: :: CARDFIL4:8
for x, y being Point of (Euclid 1)
for r, s being Real st x = <*r*> & y = <*s*> holds
dist (x,y) = |.(r - s).|
proof end;

registration
cluster [:NAT,NAT:] -> countable ;
coherence
[:NAT,NAT:] is countable by CARD_4:7;
end;

registration
cluster [:NAT,NAT:] -> denumerable ;
coherence
[:NAT,NAT:] is denumerable ;
end;

theorem Th9: :: CARDFIL4:9
{ [0,n] where n is Nat : verum } is infinite
proof end;

theorem :: CARDFIL4:10
for i, j, k, l being Nat st i <= k & j <= l holds
[:(Segm i),(Segm j):] c= [:(Segm k),(Segm l):]
proof end;

theorem Th10: :: CARDFIL4:11
for m, n being Nat holds [:(NAT \ (Segm m)),(NAT \ (Segm n)):] c= [:NAT,NAT:] \ [:(Segm m),(Segm n):]
proof end;

theorem Th11: :: CARDFIL4:12
for m, n being Nat
for no being Element of OrderedNAT st n = no & n <= m holds
m in uparrow no
proof end;

theorem Th12: :: CARDFIL4:13
for m, n being Nat
for no being Element of OrderedNAT st n = no & m in uparrow no holds
n <= m
proof end;

theorem Th13: :: CARDFIL4:14
for n being Nat
for no being Element of OrderedNAT st n = no holds
uparrow no = NAT \ (Segm n)
proof end;

theorem Th14: :: CARDFIL4:15
for A being Subset of [:NAT,NAT:] holds proj1 A = { x where x is Element of NAT : ex y being Element of NAT st [x,y] in A }
proof end;

theorem Th15: :: CARDFIL4:16
for A being Subset of [:NAT,NAT:] holds proj2 A = { y where y is Element of NAT : ex x being Element of NAT st [x,y] in A }
proof end;

theorem Th16: :: CARDFIL4:17
for A being finite Subset of [:NAT,NAT:] ex m, n being Nat st A c= [:(Segm m),(Segm n):]
proof end;

theorem Th17: :: CARDFIL4:18
for X being non empty set
for cF being Filter of X holds cF is proper Filter of (BoolePoset X)
proof end;

theorem Th18: :: CARDFIL4:19
for X being non empty set
for cF being Filter of X ex cB being filter_base of X st
( cB = cF & <.cB.) = cF )
proof end;

theorem Th19: :: CARDFIL4:20
for x being object
for T being non empty TopSpace
for cF being Filter of the carrier of T st x in lim_filter cF holds
x is_a_cluster_point_of cF,T
proof end;

theorem Th20: :: CARDFIL4:21
for B being Element of base_of_frechet_filter ex n being Nat st B = NAT \ (Segm n)
proof end;

theorem Th21: :: CARDFIL4:22
for n being Nat
for B being Subset of NAT st B = NAT \ (Segm n) holds
B is Element of base_of_frechet_filter
proof end;

definition
let X1, X2 be non empty set ;
let cB1 be filter_base of X1;
let cB2 be filter_base of X2;
func [:cB1,cB2:] -> filter_base of [:X1,X2:] equals :: CARDFIL4:def 1
 { [:B1,B2:] where B1 is Element of cB1, B2 is Element of cB2 : verum } ;
coherence
{ [:B1,B2:] where B1 is Element of cB1, B2 is Element of cB2 : verum } is filter_base of [:X1,X2:]
proof end;
end;

:: deftheorem defines [: CARDFIL4:def 1 :
for X1, X2 being non empty set
for cB1 being filter_base of X1
for cB2 being filter_base of X2 holds [:cB1,cB2:] = { [:B1,B2:] where B1 is Element of cB1, B2 is Element of cB2 : verum } ;

theorem Th22: :: CARDFIL4:23
for X1, X2 being non empty set
for cA1, cB1 being filter_base of X1
for cA2, cB2 being filter_base of X2
for cF1 being Filter of X1
for cF2 being Filter of X2 st cF1 = <.cB1.) & cF1 = <.cA1.) & cF2 = <.cB2.) & cF2 = <.cA2.) holds
<.[:cB1,cB2:].) = <.[:cA1,cA2:].)
proof end;

theorem Th23: :: CARDFIL4:24
for X1 being non empty set
for cB1 being filter_base of X1
for cF1 being Filter of X1
for cBa1 being basis of cF1 st cBa1 = cB1 holds
<.cB1.] = cF1
proof end;

theorem Th24: :: CARDFIL4:25
for X1 being non empty set
for cF1 being Filter of X1 ex cB1 being filter_base of X1 st <.cB1.) = cF1
proof end;

definition
let X1, X2 be non empty set ;
let cF1 be Filter of X1;
let cF2 be Filter of X2;
func <.cF1,cF2.) -> Filter of [:X1,X2:] means :Def1: :: CARDFIL4:def 2
 ex cB1 being filter_base of X1 ex cB2 being filter_base of X2 st
( <.cB1.) = cF1 & <.cB2.) = cF2 & it = <.[:cB1,cB2:].) );
existence
ex b1 being Filter of [:X1,X2:] ex cB1 being filter_base of X1 ex cB2 being filter_base of X2 st
( <.cB1.) = cF1 & <.cB2.) = cF2 & b1 = <.[:cB1,cB2:].) )
proof end;
uniqueness
for b1, b2 being Filter of [:X1,X2:] st ex cB1 being filter_base of X1 ex cB2 being filter_base of X2 st
( <.cB1.) = cF1 & <.cB2.) = cF2 & b1 = <.[:cB1,cB2:].) ) & ex cB1 being filter_base of X1 ex cB2 being filter_base of X2 st
( <.cB1.) = cF1 & <.cB2.) = cF2 & b2 = <.[:cB1,cB2:].) ) holds
b1 = b2 by Th22;
end;

:: deftheorem Def1 defines <. CARDFIL4:def 2 :
for X1, X2 being non empty set
for cF1 being Filter of X1
for cF2 being Filter of X2
for b5 being Filter of [:X1,X2:] holds
( b5 = <.cF1,cF2.) iff ex cB1 being filter_base of X1 ex cB2 being filter_base of X2 st
( <.cB1.) = cF1 & <.cB2.) = cF2 & b5 = <.[:cB1,cB2:].) ) );

definition
let X1, X2 be non empty set ;
let cF1 be Filter of X1;
let cF2 be Filter of X2;
let cB1 be basis of cF1;
let cB2 be basis of cF2;
func [:cB1,cB2:] -> basis of <.cF1,cF2.) means :Def2: :: CARDFIL4:def 3
 ex cB3 being filter_base of X1 ex cB4 being filter_base of X2 st
( cB1 = cB3 & cB2 = cB4 & it = [:cB3,cB4:] );
existence
ex b1 being basis of <.cF1,cF2.) ex cB3 being filter_base of X1 ex cB4 being filter_base of X2 st
( cB1 = cB3 & cB2 = cB4 & b1 = [:cB3,cB4:] )
proof end;
uniqueness
for b1, b2 being basis of <.cF1,cF2.) st ex cB3 being filter_base of X1 ex cB4 being filter_base of X2 st
( cB1 = cB3 & cB2 = cB4 & b1 = [:cB3,cB4:] ) & ex cB3 being filter_base of X1 ex cB4 being filter_base of X2 st
( cB1 = cB3 & cB2 = cB4 & b2 = [:cB3,cB4:] ) holds
b1 = b2 ;
end;

:: deftheorem Def2 defines [: CARDFIL4:def 3 :
for X1, X2 being non empty set
for cF1 being Filter of X1
for cF2 being Filter of X2
for cB1 being basis of cF1
for cB2 being basis of cF2
for b7 being basis of <.cF1,cF2.) holds
( b7 = [:cB1,cB2:] iff ex cB3 being filter_base of X1 ex cB4 being filter_base of X2 st
( cB1 = cB3 & cB2 = cB4 & b7 = [:cB3,cB4:] ) );

definition
let n be Nat;
func square-uparrow n -> Subset of [:NAT,NAT:] means :Def3: :: CARDFIL4:def 4
 for x being Element of [:NAT,NAT:] holds
( x in it iff ex n1, n2 being Nat st
( n1 = x `1 & n2 = x `2 & n <= n1 & n <= n2 ) );
existence
ex b1 being Subset of [:NAT,NAT:] st
for x being Element of [:NAT,NAT:] holds
( x in b1 iff ex n1, n2 being Nat st
( n1 = x `1 & n2 = x `2 & n <= n1 & n <= n2 ) )
proof end;
uniqueness
for b1, b2 being Subset of [:NAT,NAT:] st ( for x being Element of [:NAT,NAT:] holds
( x in b1 iff ex n1, n2 being Nat st
( n1 = x `1 & n2 = x `2 & n <= n1 & n <= n2 ) ) ) & ( for x being Element of [:NAT,NAT:] holds
( x in b2 iff ex n1, n2 being Nat st
( n1 = x `1 & n2 = x `2 & n <= n1 & n <= n2 ) ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def3 defines square-uparrow CARDFIL4:def 4 :
for n being Nat
for b2 being Subset of [:NAT,NAT:] holds
( b2 = square-uparrow n iff for x being Element of [:NAT,NAT:] holds
( x in b2 iff ex n1, n2 being Nat st
( n1 = x `1 & n2 = x `2 & n <= n1 & n <= n2 ) ) );

theorem Th25: :: CARDFIL4:26
for n being Nat holds [n,n] in square-uparrow n
proof end;

registration
let n be Nat;
cluster square-uparrow n -> non empty ;
coherence
not square-uparrow n is empty by Th25;
end;

theorem :: CARDFIL4:27
for i, j, k, l, n being Nat st [i,j] in square-uparrow n holds
( [(i + k),j] in square-uparrow n & [i,(j + l)] in square-uparrow n )
proof end;

theorem :: CARDFIL4:28
for n being Nat holds square-uparrow n is infinite Subset of [:NAT,NAT:]
proof end;

theorem Th26: :: CARDFIL4:29
for n being Nat
for no being Element of OrderedNAT st no = n holds
square-uparrow n = [:(uparrow no),(uparrow no):]
proof end;

theorem :: CARDFIL4:30
for m, n being Nat st m = n - 1 holds
square-uparrow n c= [:NAT,NAT:] \ [:(Seg m),(Seg m):]
proof end;

theorem :: CARDFIL4:31
for n being Nat holds square-uparrow n c= [:NAT,NAT:] \ [:(Segm n),(Segm n):]
proof end;

theorem Th27: :: CARDFIL4:32
for n being Nat holds square-uparrow n = [:(NAT \ (Segm n)),(NAT \ (Segm n)):]
proof end;

theorem Th28: :: CARDFIL4:33
for i, j being Nat ex n being Nat st square-uparrow n c= [:(NAT \ (Segm i)),(NAT \ (Segm j)):]
proof end;

theorem Th29: :: CARDFIL4:34
for i, j, n being Nat st n = max (i,j) holds
square-uparrow n c= (square-uparrow i) /\ (square-uparrow j)
proof end;

definition
let n be Nat;
func square-downarrow n -> Subset of [:NAT,NAT:] means :Def4: :: CARDFIL4:def 5
 for x being Element of [:NAT,NAT:] holds
( x in it iff ex n1, n2 being Nat st
( n1 = x `1 & n2 = x `2 & n1 < n & n2 < n ) );
existence
ex b1 being Subset of [:NAT,NAT:] st
for x being Element of [:NAT,NAT:] holds
( x in b1 iff ex n1, n2 being Nat st
( n1 = x `1 & n2 = x `2 & n1 < n & n2 < n ) )
proof end;
uniqueness
for b1, b2 being Subset of [:NAT,NAT:] st ( for x being Element of [:NAT,NAT:] holds
( x in b1 iff ex n1, n2 being Nat st
( n1 = x `1 & n2 = x `2 & n1 < n & n2 < n ) ) ) & ( for x being Element of [:NAT,NAT:] holds
( x in b2 iff ex n1, n2 being Nat st
( n1 = x `1 & n2 = x `2 & n1 < n & n2 < n ) ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def4 defines square-downarrow CARDFIL4:def 5 :
for n being Nat
for b2 being Subset of [:NAT,NAT:] holds
( b2 = square-downarrow n iff for x being Element of [:NAT,NAT:] holds
( x in b2 iff ex n1, n2 being Nat st
( n1 = x `1 & n2 = x `2 & n1 < n & n2 < n ) ) );

theorem Th30: :: CARDFIL4:35
for n being Nat holds square-downarrow n = [:(Segm n),(Segm n):]
proof end;

theorem :: CARDFIL4:36
for A being finite Subset of [:NAT,NAT:] ex n being Nat st A c= square-downarrow n
proof end;

theorem :: CARDFIL4:37
for n being Nat holds square-downarrow n is finite Subset of [:NAT,NAT:]
proof end;

theorem Th31: :: CARDFIL4:38
for x being Element of [:base_of_frechet_filter,base_of_frechet_filter:] ex i, j being Nat st x = [:(NAT \ (Segm i)),(NAT \ (Segm j)):]
proof end;

theorem Th32: :: CARDFIL4:39
for x being Element of [:base_of_frechet_filter,base_of_frechet_filter:] ex n being Nat st square-uparrow n c= x
proof end;

theorem :: CARDFIL4:40
[:base_of_frechet_filter,base_of_frechet_filter:] is filter_base of [:NAT,NAT:] ;

theorem Th33: :: CARDFIL4:41
ex cB being basis of (Frechet_Filter NAT) st
( cB = base_of_frechet_filter & [:cB,cB:] is basis of <.(Frechet_Filter NAT),(Frechet_Filter NAT).) )
proof end;

definition
func all-square-uparrow -> filter_base of [:NAT,NAT:] equals :: CARDFIL4:def 6
 { (square-uparrow n) where n is Nat : verum } ;
coherence
{ (square-uparrow n) where n is Nat : verum } is filter_base of [:NAT,NAT:]
proof end;
end;

:: deftheorem defines all-square-uparrow CARDFIL4:def 6 :
all-square-uparrow = { (square-uparrow n) where n is Nat : verum } ;

theorem Th34: :: CARDFIL4:42
all-square-uparrow ,[:base_of_frechet_filter,base_of_frechet_filter:] are_equivalent_generators
proof end;

theorem Th35: :: CARDFIL4:43
<.[:base_of_frechet_filter,base_of_frechet_filter:].) = <.(Frechet_Filter NAT),(Frechet_Filter NAT).)
proof end;

theorem Th36: :: CARDFIL4:44
<.all-square-uparrow.) = <.(Frechet_Filter NAT),(Frechet_Filter NAT).) by Th34, CARDFIL2:19, Th35;

theorem Th37: :: CARDFIL4:45
<.(Frechet_Filter NAT),(Frechet_Filter NAT).) is_filter-finer_than Frechet_Filter [:NAT,NAT:]
proof end;

theorem Th38: :: CARDFIL4:46
( [:NAT,NAT:] \ { [0,n] where n is Nat : verum } in <.(Frechet_Filter NAT),(Frechet_Filter NAT).) & not [:NAT,NAT:] \ { [0,n] where n is Nat : verum } in Frechet_Filter [:NAT,NAT:] )
proof end;

theorem :: CARDFIL4:47
Frechet_Filter [:NAT,NAT:] <> <.(Frechet_Filter NAT),(Frechet_Filter NAT).) by Th38;

theorem Th39: :: CARDFIL4:48
for T being non empty TopSpace
for cF3, cF4 being Filter of the carrier of T st cF4 is_filter-finer_than cF3 holds
lim_filter cF3 c= lim_filter cF4
proof end;

theorem Th40: :: CARDFIL4:49
for X, Y being non empty set
for f being Function of X,Y
for 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 end;

theorem Th41: :: CARDFIL4:50
for T being non empty TopSpace
for s being Function of [:NAT,NAT:], the carrier of T
for M being Subset of the carrier of T holds
( s " M in Frechet_Filter [:NAT,NAT:] iff ex A being finite Subset of [:NAT,NAT:] st s " M = [:NAT,NAT:] \ A )
proof end;

theorem Th42: :: CARDFIL4:51
for T being non empty TopSpace
for s being Function of [:NAT,NAT:], the carrier of T
for M being Subset of the carrier of T holds
( s " M in <.(Frechet_Filter NAT),(Frechet_Filter NAT).) iff ex n being Nat st square-uparrow n c= s " M )
proof end;

theorem Th43: :: CARDFIL4:52
for T being non empty TopSpace
for s being Function of [:NAT,NAT:], the carrier of T holds 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 end;

theorem Th44: :: CARDFIL4:53
for T being non empty TopSpace
for s being Function of [:NAT,NAT:], the carrier of T holds 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 end;

theorem Th45: :: CARDFIL4:54
for T being non empty TopSpace
for s being Function of [:NAT,NAT:], the carrier of T
for x being Point of T holds
( x in lim_filter (s,(Frechet_Filter [:NAT,NAT:])) iff for A being a_neighborhood of x ex B being finite Subset of [:NAT,NAT:] st s " A = [:NAT,NAT:] \ B )
proof end;

theorem Th46: :: CARDFIL4:55
for T being non empty TopSpace
for s being Function of [:NAT,NAT:], the carrier of T
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 end;

theorem Th47: :: CARDFIL4:56
for T being non empty TopSpace
for s being Function of [:NAT,NAT:], the carrier of T
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 ex n being Nat st square-uparrow n c= s " A )
proof end;

theorem Th48: :: CARDFIL4:57
for T being non empty TopSpace
for s being Function of [:NAT,NAT:], the carrier of T
for x being Point of T
for 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 ex n being Nat st square-uparrow n c= s " B )
proof end;

theorem Th49: :: CARDFIL4:58
for T being non empty TopSpace
for s being Function of [:NAT,NAT:], the carrier of T
for x being Point of T
for cB being basis of (BOOL2F (NeighborhoodSystem x)) holds
( x in lim_filter (s,(Frechet_Filter [:NAT,NAT:])) iff for B being Element of cB ex A being finite Subset of [:NAT,NAT:] st s " B = [:NAT,NAT:] \ A )
proof end;

theorem Th50: :: CARDFIL4:59
for T being non empty TopSpace
for s being Function of [:NAT,NAT:], the carrier of T
for x being Point of T
for 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 ex n being Nat st s .: (square-uparrow n) c= B )
proof end;

theorem Th51: :: CARDFIL4:60
for T being non empty TopSpace
for s being Function of [:NAT,NAT:], the carrier of T
for x being Point of T
for cB being basis of (BOOL2F (NeighborhoodSystem x)) holds
( x in lim_filter (s,(Frechet_Filter [:NAT,NAT:])) iff for B being Element of cB ex A being finite Subset of [:NAT,NAT:] st s .: ([:NAT,NAT:] \ A) c= B )
proof end;

theorem Th52: :: CARDFIL4:61
for T being non empty TopSpace
for s being Function of [:NAT,NAT:], the carrier of T
for x being Point of T
for cB being basis of (BOOL2F (NeighborhoodSystem x)) holds
( x in lim_filter (s,(Frechet_Filter [:NAT,NAT:])) iff for B being Element of cB ex n, m being Nat st s .: ([:NAT,NAT:] \ [:(Segm n),(Segm m):]) c= B )
proof end;

theorem Th53: :: CARDFIL4:62
for x being object
for n being Nat
for T being non empty TopSpace
for s being Function of [:NAT,NAT:], the carrier of T holds
( x in s .: (square-uparrow n) iff ex i, j being Nat st
( n <= i & n <= j & x = s . (i,j) ) )
proof end;

theorem :: CARDFIL4:63
for x being object
for i, j being Nat
for T being non empty TopSpace
for s being Function of [:NAT,NAT:], the carrier of T holds
( 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 end;

theorem Th54: :: CARDFIL4:64
for T being non empty TopSpace
for s being Function of [:NAT,NAT:], the carrier of T
for x being Point of T
for 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 ex n being Nat st
for n1, n2 being Nat st n <= n1 & n <= n2 holds
s . (n1,n2) in B )
proof end;

theorem Th55: :: CARDFIL4:65
for T being non empty TopSpace
for s being Function of [:NAT,NAT:], the carrier of T
for x being Point of T
for cB being basis of (BOOL2F (NeighborhoodSystem x)) holds
( x in lim_filter (s,(Frechet_Filter [:NAT,NAT:])) iff for B being Element of cB ex i, j being Nat st
for m, n being Nat st ( i <= m or j <= n ) holds
s . (m,n) in B )
proof end;

theorem Th56: :: CARDFIL4:66
for T being non empty TopSpace
for s being Function of [:NAT,NAT:], the carrier of T holds lim_filter (s,(Frechet_Filter [:NAT,NAT:])) c= lim_filter (s,<.all-square-uparrow.))
proof end;

theorem Th57: :: CARDFIL4:67
for M being non empty MetrSpace
for p being Point of M
for x being Point of (TopSpaceMetr M)
for 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 end;

theorem :: CARDFIL4:68
for M being non empty MetrSpace
for p being Point of M
for x being Point of (TopSpaceMetr M)
for s being Function of [:NAT,NAT:],(TopSpaceMetr M)
for 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;

theorem :: CARDFIL4:69
for x being Point of (TopSpaceMetr (Euclid 1))
for y being Point of (Euclid 1)
for cB being basis of (BOOL2F (NeighborhoodSystem x))
for 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 end;

definition
let s be Function of [:NAT,NAT:],REAL;
func # s -> Function of [:NAT,NAT:],R^1 equals :: CARDFIL4:def 7
s;
coherence
s is Function of [:NAT,NAT:],R^1 ;
end;

:: deftheorem defines # CARDFIL4:def 7 :
for s being Function of [:NAT,NAT:],REAL holds # s = s;

theorem :: CARDFIL4:70
for m, n being Nat
for s being Function of [:NAT,NAT:],(TopSpaceMetr (Euclid 1))
for 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 end;

theorem Th58: :: CARDFIL4:71
for r being Real
for Rseq being Function of [:NAT,NAT:],REAL holds
( 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 end;

theorem Th59: :: CARDFIL4:72
for Rseq being Function of [:NAT,NAT:],REAL st lim_filter ((# Rseq),<.(Frechet_Filter NAT),(Frechet_Filter NAT).)) <> {} holds
ex x being Real st lim_filter ((# Rseq),<.(Frechet_Filter NAT),(Frechet_Filter NAT).)) = {x}
proof end;

theorem Th60: :: CARDFIL4:73
for Rseq being Function of [:NAT,NAT:],REAL st Rseq is P-convergent holds
P-lim Rseq in lim_filter ((# Rseq),<.(Frechet_Filter NAT),(Frechet_Filter NAT).))
proof end;

theorem Th61: :: CARDFIL4:74
for Rseq being Function of [:NAT,NAT:],REAL holds
( Rseq is P-convergent iff lim_filter ((# Rseq),<.(Frechet_Filter NAT),(Frechet_Filter NAT).)) <> {} )
proof end;

theorem Th62: :: CARDFIL4:75
for Rseq being Function of [:NAT,NAT:],REAL st Rseq is P-convergent holds
{(P-lim Rseq)} = lim_filter ((# Rseq),<.(Frechet_Filter NAT),(Frechet_Filter NAT).))
proof end;

theorem :: CARDFIL4:76
for Rseq being Function of [:NAT,NAT:],REAL st not lim_filter ((# Rseq),<.(Frechet_Filter NAT),(Frechet_Filter NAT).)) is empty holds
( Rseq is P-convergent & {(P-lim Rseq)} = lim_filter ((# Rseq),<.(Frechet_Filter NAT),(Frechet_Filter NAT).)) ) by Th61, Th62;

definition
func dblseq_ex_1 -> Function of [:NAT,NAT:],REAL means :Def5: :: CARDFIL4:def 8
 for m, n being Nat holds it . (m,n) = 1 / (m + 1);
existence
ex b1 being Function of [:NAT,NAT:],REAL st
for m, n being Nat holds b1 . (m,n) = 1 / (m + 1)
proof end;
uniqueness
for b1, b2 being Function of [:NAT,NAT:],REAL st ( for m, n being Nat holds b1 . (m,n) = 1 / (m + 1) ) & ( for m, n being Nat holds b2 . (m,n) = 1 / (m + 1) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def5 defines dblseq_ex_1 CARDFIL4:def 8 :
for b1 being Function of [:NAT,NAT:],REAL holds
( b1 = dblseq_ex_1 iff for m, n being Nat holds b1 . (m,n) = 1 / (m + 1) );

theorem Th63: :: CARDFIL4:77
for m being non zero Nat ex n being Nat st
for n1, n2 being Nat st n <= n1 & n <= n2 holds
|.((dblseq_ex_1 . (n1,n2)) - 0).| < 1 / m
proof end;

theorem Th64: :: CARDFIL4:78
0 in lim_filter ((# dblseq_ex_1),<.(Frechet_Filter NAT),(Frechet_Filter NAT).)) by Th63, Th58;

theorem Th65: :: CARDFIL4:79
lim_filter ((# dblseq_ex_1),(Frechet_Filter [:NAT,NAT:])) = {}
proof end;

theorem :: CARDFIL4:80
lim_filter ((# dblseq_ex_1),<.(Frechet_Filter NAT),(Frechet_Filter NAT).)) <> lim_filter ((# dblseq_ex_1),(Frechet_Filter [:NAT,NAT:])) by Th63, Th58, Th65;

definition
let X1, X2 be non empty set ;
let cF1 be Filter of X1;
let Y be non empty Hausdorff TopSpace;
let 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: :: CARDFIL4:def 9
 for x being Element of X2 holds {(it . x)} = lim_filter ((ProjMap2 (f,x)),cF1);
existence
ex b1 being Function of X2,Y st
for x being Element of X2 holds {(b1 . x)} = lim_filter ((ProjMap2 (f,x)),cF1)
proof end;
uniqueness
for b1, b2 being Function of X2,Y st ( for x being Element of X2 holds {(b1 . x)} = lim_filter ((ProjMap2 (f,x)),cF1) ) & ( for x being Element of X2 holds {(b2 . x)} = lim_filter ((ProjMap2 (f,x)),cF1) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def6 defines lim_in_cod1 CARDFIL4:def 9 :
for X1, X2 being non empty set
for cF1 being Filter of X1
for Y being non empty Hausdorff TopSpace
for f being Function of [:X1,X2:],Y st ( for x being Element of X2 holds lim_filter ((ProjMap2 (f,x)),cF1) <> {} ) holds
for b6 being Function of X2,Y holds
( b6 = lim_in_cod1 (f,cF1) iff for x being Element of X2 holds {(b6 . x)} = lim_filter ((ProjMap2 (f,x)),cF1) );

definition
let X1, X2 be non empty set ;
let cF2 be Filter of X2;
let Y be non empty Hausdorff TopSpace;
let 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: :: CARDFIL4:def 10
 for x being Element of X1 holds {(it . x)} = lim_filter ((ProjMap1 (f,x)),cF2);
existence
ex b1 being Function of X1,Y st
for x being Element of X1 holds {(b1 . x)} = lim_filter ((ProjMap1 (f,x)),cF2)
proof end;
uniqueness
for b1, b2 being Function of X1,Y st ( for x being Element of X1 holds {(b1 . x)} = lim_filter ((ProjMap1 (f,x)),cF2) ) & ( for x being Element of X1 holds {(b2 . x)} = lim_filter ((ProjMap1 (f,x)),cF2) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def7 defines lim_in_cod2 CARDFIL4:def 10 :
for X1, X2 being non empty set
for cF2 being Filter of X2
for Y being non empty Hausdorff TopSpace
for f being Function of [:X1,X2:],Y st ( for x being Element of X1 holds lim_filter ((ProjMap1 (f,x)),cF2) <> {} ) holds
for b6 being Function of X1,Y holds
( b6 = lim_in_cod2 (f,cF2) iff for x being Element of X1 holds {(b6 . x)} = lim_filter ((ProjMap1 (f,x)),cF2) );

theorem :: CARDFIL4:81
for X being non empty set
for f being Function of X,REAL holds f is Function of X,R^1 ;

theorem :: CARDFIL4:82
for s being sequence of REAL holds s is Function of NAT,R^1 ;

theorem Th70: :: CARDFIL4:83
for f being Function of ([#] OrderedNAT),R^1
for seq being Function of NAT,REAL st f = seq & lim_f f <> {} holds
( 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 end;

theorem Th71: :: CARDFIL4:84
for f being Function of ([#] OrderedNAT),R^1
for seq being Function of NAT,REAL st f = seq & lim_f f <> {} holds
lim_f f = {(lim seq)}
proof end;

theorem :: CARDFIL4:85
for T being non empty TopSpace
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 :: CARDFIL4:86
for T being non empty TopSpace
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: :: CARDFIL4:87
for seq being Function of NAT,REAL
for f being Function of NAT,R^1 st f = seq & lim_f f <> {} holds
lim_f f = {(lim seq)}
proof end;

theorem :: CARDFIL4:88
for Rseq being Function of [:NAT,NAT:],REAL holds
( ( for x being Element of NAT holds lim_filter ((ProjMap2 ((# Rseq),x)),(Frechet_Filter NAT)) <> {} ) iff Rseq is convergent_in_cod1 )
proof end;

theorem :: CARDFIL4:89
for Rseq being Function of [:NAT,NAT:],REAL holds
( ( for x being Element of NAT holds lim_filter ((ProjMap1 ((# Rseq),x)),(Frechet_Filter NAT)) <> {} ) iff Rseq is convergent_in_cod2 )
proof end;

theorem Th73: :: CARDFIL4:90
for t being Element of NAT
for 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 end;

theorem Th74: :: CARDFIL4:91
for t being Element of NAT
for 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 end;

theorem :: CARDFIL4:92
for Rseq being Function of [:NAT,NAT:],REAL
for Y being non empty Hausdorff TopSpace
for 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 end;

theorem :: CARDFIL4:93
for Rseq being Function of [:NAT,NAT:],REAL
for Y being non empty Hausdorff TopSpace
for 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 end;

theorem :: CARDFIL4:94
for X1, X2 being non empty set
for cB1 being filter_base of X1
for cB2 being filter_base of X2
for cF1 being Filter of X1
for cF2 being Filter of X2
for Y being non empty TopSpace
for x being Point of Y
for f being Function of [:X1,X2:],Y st x in lim_filter (f,<.cF1,cF2.)) & <.cB1.) = cF1 & <.cB2.) = cF2 holds
for V being Subset of Y st V is open & x in V holds
ex B1 being Element of cB1 ex B2 being Element of cB2 st f .: [:B1,B2:] c= V
proof end;

theorem Th75: :: CARDFIL4:95
for X1, X2 being non empty set
for cB1 being filter_base of X1
for cB2 being filter_base of X2
for cF1 being Filter of X1
for cF2 being Filter of X2
for Y being non empty TopSpace
for x being Point of Y
for f being Function of [:X1,X2:],Y st x in lim_filter (f,<.cF1,cF2.)) & <.cB1.) = cF1 & <.cB2.) = cF2 holds
for U being a_neighborhood of x st U is closed holds
ex B1 being Element of cB1 ex B2 being Element of cB2 st f .: [:B1,B2:] c= Int U
proof end;

theorem :: CARDFIL4:96
for X1, X2 being non empty set
for cB1 being filter_base of X1
for cB2 being filter_base of X2
for cF1 being Filter of X1
for cF2 being Filter of X2
for Y being non empty TopSpace
for x being Point of Y
for f being Function of [:X1,X2:],Y st x in lim_filter (f,<.cF1,cF2.)) & <.cB1.) = cF1 & <.cB2.) = cF2 holds
for U being a_neighborhood of x st U is closed holds
ex B1 being Element of cB1 ex B2 being Element of cB2 st
for y being Element of B1 holds f .: [:{y},B2:] c= Int U
proof end;

theorem Th76: :: CARDFIL4:97
for X1, X2 being non empty set
for cB1 being filter_base of X1
for cB2 being filter_base of X2
for cF1 being Filter of X1
for cF2 being Filter of X2
for Y being non empty TopSpace
for x being Point of Y
for f being Function of [:X1,X2:],Y st x in lim_filter (f,<.cF1,cF2.)) & <.cB1.) = cF1 & <.cB2.) = cF2 holds
for U being a_neighborhood of x st U is closed holds
ex B1 being Element of cB1 ex B2 being Element of cB2 st
for z being Element of X1
for y being Element of Y st z in B1 & y in lim_filter ((ProjMap1 (f,z)),cF2) holds
y in Cl (Int U)
proof end;

theorem Th77: :: CARDFIL4:98
for X1, X2 being non empty set
for cB1 being filter_base of X1
for cB2 being filter_base of X2
for cF1 being Filter of X1
for cF2 being Filter of X2
for Y being non empty TopSpace
for x being Point of Y
for f being Function of [:X1,X2:],Y st x in lim_filter (f,<.cF1,cF2.)) & <.cB1.) = cF1 & <.cB2.) = cF2 holds
for U being a_neighborhood of x st U is closed holds
ex B1 being Element of cB1 ex B2 being Element of cB2 st
for z being Element of X2
for y being Element of Y st z in B2 & y in lim_filter ((ProjMap2 (f,z)),cF1) holds
y in Cl (Int U)
proof end;

theorem Th78: :: CARDFIL4:99
for X1, X2 being non empty set
for cF1 being Filter of X1
for cF2 being Filter of X2
for Y being non empty Hausdorff regular TopSpace
for 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 end;

theorem Th79: :: CARDFIL4:100
for X1, X2 being non empty set
for cF1 being Filter of X1
for cF2 being Filter of X2
for Y being non empty Hausdorff regular TopSpace
for 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 end;

theorem Th80: :: CARDFIL4:101
for X1, X2 being non empty set
for cF1 being Filter of X1
for cF2 being Filter of X2
for Y being non empty Hausdorff regular TopSpace
for 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 end;

theorem Th81: :: CARDFIL4:102
for X1, X2 being non empty set
for cF1 being Filter of X1
for cF2 being Filter of X2
for Y being non empty Hausdorff regular TopSpace
for 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 end;

theorem :: CARDFIL4:103
for X1, X2 being non empty set
for cF1 being Filter of X1
for cF2 being Filter of X2
for Y being non empty Hausdorff regular TopSpace
for 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 end;