let T be non empty TopSpace; :: thesis: 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 )
let s be Function of [:NAT,NAT:], the carrier of T; :: thesis: 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 )
let x be Point of T; :: thesis: ( x in lim_filter (s,(Frechet_Filter [:NAT,NAT:])) iff for A being a_neighborhood of x holds [:NAT,NAT:] \ (s " A) is finite )
hereby :: thesis: ( ( for A being a_neighborhood of x holds [:NAT,NAT:] \ (s " A) is finite ) implies x in lim_filter (s,(Frechet_Filter [:NAT,NAT:])) )
assume A1: x in lim_filter (s,(Frechet_Filter [:NAT,NAT:])) ; :: thesis: for A being a_neighborhood of x holds [:NAT,NAT:] \ (s " A) is finite
now :: thesis: for A being a_neighborhood of x holds [:NAT,NAT:] \ (s " A) is finite
let A be a_neighborhood of x; :: thesis: [:NAT,NAT:] \ (s " A) is finite
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; :: thesis: verum
end;
hence for A being a_neighborhood of x holds [:NAT,NAT:] \ (s " A) is finite ; :: thesis: verum
end;
assume A2: for A being a_neighborhood of x holds [:NAT,NAT:] \ (s " A) is finite ; :: thesis: x in lim_filter (s,(Frechet_Filter [:NAT,NAT:]))
now :: thesis: for A being a_neighborhood of x ex B being finite Subset of [:NAT,NAT:] st s " A = [:NAT,NAT:] \ B
let A be a_neighborhood of x; :: thesis: ex B being finite Subset of [:NAT,NAT:] st s " A = [:NAT,NAT:] \ B
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; :: thesis: verum
end;
hence x in lim_filter (s,(Frechet_Filter [:NAT,NAT:])) by Th45; :: thesis: verum