:: by Roland Coghetto

::

:: Received June 30, 2016

:: Copyright (c) 2016-2018 Association of Mizar Users

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:]

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 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).| )

( 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).| )

( 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).|

for r, s being Real st x = <*r*> & y = <*s*> holds

dist (x,y) = |.(r - s).|

proof end;

registration
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 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 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 )

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

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 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

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;

{ [:B1,B2:] where B1 is Element of cB1, B2 is Element of cB2 : verum } is filter_base of [:X1,X2:]

end;
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 } ;

{ [:B1,B2:] where B1 is Element of cB1, B2 is Element of cB2 : verum } is filter_base of [:X1,X2:]

proof 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 } ;

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:].)

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

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

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;

ex b_{1} being Filter of [:X1,X2:] ex cB1 being filter_base of X1 ex cB2 being filter_base of X2 st

( <.cB1.) = cF1 & <.cB2.) = cF2 & b_{1} = <.[:cB1,cB2:].) )

for b_{1}, b_{2} 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 & b_{1} = <.[:cB1,cB2:].) ) & ex cB1 being filter_base of X1 ex cB2 being filter_base of X2 st

( <.cB1.) = cF1 & <.cB2.) = cF2 & b_{2} = <.[:cB1,cB2:].) ) holds

b_{1} = b_{2}
by Th22;

end;
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 cB1 being filter_base of X1 ex cB2 being filter_base of X2 st

( <.cB1.) = cF1 & <.cB2.) = cF2 & it = <.[:cB1,cB2:].) );

ex b

( <.cB1.) = cF1 & <.cB2.) = cF2 & b

proof end;

uniqueness for b

( <.cB1.) = cF1 & <.cB2.) = cF2 & b

( <.cB1.) = cF1 & <.cB2.) = cF2 & b

b

:: 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 b_{5} being Filter of [:X1,X2:] holds

( b_{5} = <.cF1,cF2.) iff ex cB1 being filter_base of X1 ex cB2 being filter_base of X2 st

( <.cB1.) = cF1 & <.cB2.) = cF2 & b_{5} = <.[:cB1,cB2:].) ) );

for X1, X2 being non empty set

for cF1 being Filter of X1

for cF2 being Filter of X2

for b

( b

( <.cB1.) = cF1 & <.cB2.) = cF2 & b

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;

ex b_{1} being basis of <.cF1,cF2.) ex cB3 being filter_base of X1 ex cB4 being filter_base of X2 st

( cB1 = cB3 & cB2 = cB4 & b_{1} = [:cB3,cB4:] )

for b_{1}, b_{2} 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 & b_{1} = [:cB3,cB4:] ) & ex cB3 being filter_base of X1 ex cB4 being filter_base of X2 st

( cB1 = cB3 & cB2 = cB4 & b_{2} = [:cB3,cB4:] ) holds

b_{1} = b_{2}
;

end;
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 cB3 being filter_base of X1 ex cB4 being filter_base of X2 st

( cB1 = cB3 & cB2 = cB4 & it = [:cB3,cB4:] );

ex b

( cB1 = cB3 & cB2 = cB4 & b

proof end;

uniqueness for b

( cB1 = cB3 & cB2 = cB4 & b

( cB1 = cB3 & cB2 = cB4 & b

b

:: 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 b_{7} being basis of <.cF1,cF2.) holds

( b_{7} = [:cB1,cB2:] iff ex cB3 being filter_base of X1 ex cB4 being filter_base of X2 st

( cB1 = cB3 & cB2 = cB4 & b_{7} = [:cB3,cB4:] ) );

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 b

( b

( cB1 = cB3 & cB2 = cB4 & b

definition

let n be Nat;

ex b_{1} being Subset of [:NAT,NAT:] st

for x being Element of [:NAT,NAT:] holds

( x in b_{1} iff ex n1, n2 being Nat st

( n1 = x `1 & n2 = x `2 & n <= n1 & n <= n2 ) )

for b_{1}, b_{2} being Subset of [:NAT,NAT:] st ( for x being Element of [:NAT,NAT:] holds

( x in b_{1} 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 b_{2} iff ex n1, n2 being Nat st

( n1 = x `1 & n2 = x `2 & n <= n1 & n <= n2 ) ) ) holds

b_{1} = b_{2}

end;
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 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 ) );

ex b

for x being Element of [:NAT,NAT:] holds

( x in b

( n1 = x `1 & n2 = x `2 & n <= n1 & n <= n2 ) )

proof end;

uniqueness for b

( x in b

( n1 = x `1 & n2 = x `2 & n <= n1 & n <= n2 ) ) ) & ( for x being Element of [:NAT,NAT:] holds

( x in b

( n1 = x `1 & n2 = x `2 & n <= n1 & n <= n2 ) ) ) holds

b

proof end;

:: deftheorem Def3 defines square-uparrow CARDFIL4:def 4 :

for n being Nat

for b_{2} being Subset of [:NAT,NAT:] holds

( b_{2} = square-uparrow n iff for x being Element of [:NAT,NAT:] holds

( x in b_{2} iff ex n1, n2 being Nat st

( n1 = x `1 & n2 = x `2 & n <= n1 & n <= n2 ) ) );

for n being Nat

for b

( b

( x in b

( n1 = x `1 & n2 = x `2 & n <= n1 & n <= n2 ) ) );

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 )

( [(i + k),j] in square-uparrow n & [i,(j + l)] in square-uparrow n )

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):]

for no being Element of OrderedNAT st no = n holds

square-uparrow n = [:(uparrow no),(uparrow no):]

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)

square-uparrow n c= (square-uparrow i) /\ (square-uparrow j)

proof end;

definition

let n be Nat;

ex b_{1} being Subset of [:NAT,NAT:] st

for x being Element of [:NAT,NAT:] holds

( x in b_{1} iff ex n1, n2 being Nat st

( n1 = x `1 & n2 = x `2 & n1 < n & n2 < n ) )

for b_{1}, b_{2} being Subset of [:NAT,NAT:] st ( for x being Element of [:NAT,NAT:] holds

( x in b_{1} 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 b_{2} iff ex n1, n2 being Nat st

( n1 = x `1 & n2 = x `2 & n1 < n & n2 < n ) ) ) holds

b_{1} = b_{2}

end;
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 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 ) );

ex b

for x being Element of [:NAT,NAT:] holds

( x in b

( n1 = x `1 & n2 = x `2 & n1 < n & n2 < n ) )

proof end;

uniqueness for b

( x in b

( n1 = x `1 & n2 = x `2 & n1 < n & n2 < n ) ) ) & ( for x being Element of [:NAT,NAT:] holds

( x in b

( n1 = x `1 & n2 = x `2 & n1 < n & n2 < n ) ) ) holds

b

proof end;

:: deftheorem Def4 defines square-downarrow CARDFIL4:def 5 :

for n being Nat

for b_{2} being Subset of [:NAT,NAT:] holds

( b_{2} = square-downarrow n iff for x being Element of [:NAT,NAT:] holds

( x in b_{2} iff ex n1, n2 being Nat st

( n1 = x `1 & n2 = x `2 & n1 < n & n2 < n ) ) );

for n being Nat

for b

( b

( x in b

( n1 = x `1 & n2 = x `2 & n1 < n & n2 < n ) ) );

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

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).) )

( cB = base_of_frechet_filter & [:cB,cB:] is basis of <.(Frechet_Filter NAT),(Frechet_Filter NAT).) )

proof end;

definition

{ (square-uparrow n) where n is Nat : verum } is filter_base of [:NAT,NAT:]
end;

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 } ;

{ (square-uparrow n) where n is Nat : verum } is filter_base of [:NAT,NAT:]

proof end;

:: deftheorem defines all-square-uparrow CARDFIL4:def 6 :

all-square-uparrow = { (square-uparrow n) where n is Nat : verum } ;

all-square-uparrow = { (square-uparrow n) where n is Nat : verum } ;

theorem Th35: :: CARDFIL4:43

<.[:base_of_frechet_filter,base_of_frechet_filter:].) = <.(Frechet_Filter NAT),(Frechet_Filter 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

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

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)

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 )

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 )

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 }

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 }

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 )

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 )

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 )

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 )

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 )

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 )

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 )

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 )

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) ) )

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) ) )

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 )

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 )

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.))

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 } )

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;

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 }

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;

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 ) )

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 )

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}

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).))

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).)) <> {} )

( 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).))

{(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;

( Rseq is P-convergent & {(P-lim Rseq)} = lim_filter ((# Rseq),<.(Frechet_Filter NAT),(Frechet_Filter NAT).)) ) by Th61, Th62;

definition

ex b_{1} being Function of [:NAT,NAT:],REAL st

for m, n being Nat holds b_{1} . (m,n) = 1 / (m + 1)

for b_{1}, b_{2} being Function of [:NAT,NAT:],REAL st ( for m, n being Nat holds b_{1} . (m,n) = 1 / (m + 1) ) & ( for m, n being Nat holds b_{2} . (m,n) = 1 / (m + 1) ) holds

b_{1} = b_{2}
end;

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 for m, n being Nat holds it . (m,n) = 1 / (m + 1);

ex b

for m, n being Nat holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def5 defines dblseq_ex_1 CARDFIL4:def 8 :

for b_{1} being Function of [:NAT,NAT:],REAL holds

( b_{1} = dblseq_ex_1 iff for m, n being Nat holds b_{1} . (m,n) = 1 / (m + 1) );

for b

( b

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

for n1, n2 being Nat st n <= n1 & n <= n2 holds

|.((dblseq_ex_1 . (n1,n2)) - 0).| < 1 / m

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) <> {} ;

ex b_{1} being Function of X2,Y st

for x being Element of X2 holds {(b_{1} . x)} = lim_filter ((ProjMap2 (f,x)),cF1)

for b_{1}, b_{2} being Function of X2,Y st ( for x being Element of X2 holds {(b_{1} . x)} = lim_filter ((ProjMap2 (f,x)),cF1) ) & ( for x being Element of X2 holds {(b_{2} . x)} = lim_filter ((ProjMap2 (f,x)),cF1) ) holds

b_{1} = b_{2}

end;
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 for x being Element of X2 holds {(it . x)} = lim_filter ((ProjMap2 (f,x)),cF1);

ex b

for x being Element of X2 holds {(b

proof end;

uniqueness for b

b

proof 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 b_{6} being Function of X2,Y holds

( b_{6} = lim_in_cod1 (f,cF1) iff for x being Element of X2 holds {(b_{6} . x)} = lim_filter ((ProjMap2 (f,x)),cF1) );

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 b

( b

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) <> {} ;

ex b_{1} being Function of X1,Y st

for x being Element of X1 holds {(b_{1} . x)} = lim_filter ((ProjMap1 (f,x)),cF2)

for b_{1}, b_{2} being Function of X1,Y st ( for x being Element of X1 holds {(b_{1} . x)} = lim_filter ((ProjMap1 (f,x)),cF2) ) & ( for x being Element of X1 holds {(b_{2} . x)} = lim_filter ((ProjMap1 (f,x)),cF2) ) holds

b_{1} = b_{2}

end;
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 for x being Element of X1 holds {(it . x)} = lim_filter ((ProjMap1 (f,x)),cF2);

ex b

for x being Element of X1 holds {(b

proof end;

uniqueness for b

b

proof 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 b_{6} being Function of X1,Y holds

( b_{6} = lim_in_cod2 (f,cF2) iff for x being Element of X1 holds {(b_{6} . x)} = lim_filter ((ProjMap1 (f,x)),cF2) );

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 b

( b

theorem :: CARDFIL4:81

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 ) ) )

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)}

for seq being Function of NAT,REAL st f = seq & lim_f f <> {} holds

lim_f f = {(lim seq)}

proof end;

theorem :: CARDFIL4:85

theorem :: CARDFIL4:86

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)}

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 )

( ( 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 )

( ( 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)))}

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)))}

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

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

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

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

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

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)

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)

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)

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)

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)

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)

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)

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;