let T be non empty TopSpace; :: thesis: 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 )
let s be Function of [:NAT,NAT:], the carrier of T; :: thesis: 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 )
let x be Point of T; :: thesis: 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 )
let cB be basis of (BOOL2F (NeighborhoodSystem x)); :: thesis: ( 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 )
hereby :: thesis: ( ( 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 ) implies x in lim_filter (s,(Frechet_Filter [:NAT,NAT:])) )
assume A1: x in lim_filter (s,(Frechet_Filter [:NAT,NAT:])) ; :: thesis: 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
hereby :: thesis: verum
let B be Element of cB; :: thesis: ex i, j being Nat st
for m, n being Nat st ( i <= m or j <= n ) holds
s . (m,n) in B
consider i, j being Nat such that
A2: s .: ([:NAT,NAT:] \ [:(Segm i),(Segm j):]) c= B by A1, Th52;
take i = i; :: thesis: ex j being Nat st
for m, n being Nat st ( i <= m or j <= n ) holds
s . (m,n) in B
take j = j; :: thesis: for m, n being Nat st ( i <= m or j <= n ) holds
s . (m,n) in B
thus for m, n being Nat st ( i <= m or j <= n ) holds
s . (m,n) in B :: thesis: verum
proof
let m, n be Nat; :: thesis: ( ( i <= m or j <= n ) implies s . (m,n) in B )
assume A3: ( i <= m or j <= n ) ; :: thesis: s . (m,n) in B
( 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 or not 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):] ; :: thesis: contradiction
then ex a, b being object st
( a in Segm i & b in Segm j & [m,n] = [a,b] ) by ZFMISC_1:def 2;
hence contradiction by A5, XTUPLE_0:1; :: thesis: verum
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; :: thesis: verum
end;
end;
end;
assume A7: 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 ; :: thesis: x in lim_filter (s,(Frechet_Filter [:NAT,NAT:]))
now :: thesis: for B being Element of cB ex n1, n2 being Nat st s .: ([:NAT,NAT:] \ [:(Segm n1),(Segm n2):]) c= B
let B be Element of cB; :: thesis: ex n1, n2 being Nat st s .: ([:NAT,NAT:] \ [:(Segm n1),(Segm n2):]) c= B
consider i, j being Nat such that
A8: for m, n being Nat 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 ; :: according to TARSKI:def 3 :: thesis: ( not t in s .: ([:NAT,NAT:] \ [:(Segm i),(Segm j):]) or t in B )
assume t in s .: ([:NAT,NAT:] \ [:(Segm i),(Segm j):]) ; :: thesis: t in B
then consider a being 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 = a as Element of [:NAT,NAT:] by A9;
consider a1, a2 being object such that
A12: a1 in NAT and
A13: a2 in NAT and
A14: a = [a1,a2] by ZFMISC_1:def 2;
reconsider a1 = a1, a2 = a2 as Nat by A12, A13;
( not a1 in Segm i or not a2 in Segm j )
proof
assume ( a1 in Segm i & a2 in Segm j ) ; :: thesis: contradiction
then [a1,a2] in [:(Segm i),(Segm j):] by ZFMISC_1:def 2;
hence contradiction by A14, A10, XBOOLE_0:def 5; :: thesis: verum
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; :: thesis: verum
end;
hence ex n1, n2 being Nat st s .: ([:NAT,NAT:] \ [:(Segm n1),(Segm n2):]) c= B ; :: thesis: verum
end;
hence x in lim_filter (s,(Frechet_Filter [:NAT,NAT:])) by Th52; :: thesis: verum