let NTX, NTY be NTopSpace; :: thesis: for a being Point of NTY holds NTX --> a is continuous
let a be Point of NTY; :: thesis: NTX --> a is continuous
set f = NTX --> a;
now :: thesis: ( dom (NTX --> a) = the carrier of NTX & ( for x being Point of NTX holds NTX --> a is_continuous_at x ) )
thus dom (NTX --> a) = the carrier of NTX by FUNCOP_1:13; :: thesis: for x being Point of NTX holds NTX --> a is_continuous_at x
hereby :: thesis: verum
let x be Point of NTX; :: thesis: NTX --> a is_continuous_at x
now :: thesis: for F being Filter of the carrier of NTX st x in lim_filter F holds
(NTX --> a) . x in lim_filter ((NTX --> a),F)
let F be Filter of the carrier of NTX; :: thesis: ( x in lim_filter F implies (NTX --> a) . x in lim_filter ((NTX --> a),F) )
assume x in lim_filter F ; :: thesis: (NTX --> a) . x in lim_filter ((NTX --> a),F)
{ M where M is Subset of NTY : (NTX --> a) " M in F } = { M where M is Subset of NTY : a in M }
proof
set S1 = { M where M is Subset of NTY : (NTX --> a) " M in F } ;
set S2 = { M where M is Subset of NTY : a in M } ;
now :: thesis: ( { M where M is Subset of NTY : (NTX --> a) " M in F } c= { M where M is Subset of NTY : a in M } & { M where M is Subset of NTY : a in M } c= { M where M is Subset of NTY : (NTX --> a) " M in F } )
now :: thesis: for x being object st x in { M where M is Subset of NTY : (NTX --> a) " M in F } holds
x in { M where M is Subset of NTY : a in M }
let x be object ; :: thesis: ( x in { M where M is Subset of NTY : (NTX --> a) " M in F } implies x in { M where M is Subset of NTY : a in M } )
assume x in { M where M is Subset of NTY : (NTX --> a) " M in F } ; :: thesis: x in { M where M is Subset of NTY : a in M }
then consider M being Subset of NTY such that
A1: x = M and
A2: (NTX --> a) " M in F ;
( ( a in M implies (NTX --> a) " M = the carrier of NTX ) & ( not a in M implies (NTX --> a) " M = {} ) & not {} in F ) by FUNCOP_1:14, FUNCOP_1:16, CARD_FIL:def 1;
hence x in { M where M is Subset of NTY : a in M } by A1, A2; :: thesis: verum
end;
hence { M where M is Subset of NTY : (NTX --> a) " M in F } c= { M where M is Subset of NTY : a in M } ; :: thesis: { M where M is Subset of NTY : a in M } c= { M where M is Subset of NTY : (NTX --> a) " M in F }
now :: thesis: for x being object st x in { M where M is Subset of NTY : a in M } holds
x in { M where M is Subset of NTY : (NTX --> a) " M in F }
let x be object ; :: thesis: ( x in { M where M is Subset of NTY : a in M } implies x in { M where M is Subset of NTY : (NTX --> a) " M in F } )
assume x in { M where M is Subset of NTY : a in M } ; :: thesis: x in { M where M is Subset of NTY : (NTX --> a) " M in F }
then consider M being Subset of NTY such that
A3: x = M and
A4: a in M ;
( ( a in M implies (NTX --> a) " M = the carrier of NTX ) & the carrier of NTX in F ) by FUNCOP_1:14, CARD_FIL:5;
hence x in { M where M is Subset of NTY : (NTX --> a) " M in F } by A3, A4; :: thesis: verum
end;
hence { M where M is Subset of NTY : a in M } c= { M where M is Subset of NTY : (NTX --> a) " M in F } ; :: thesis: verum
end;
hence { M where M is Subset of NTY : (NTX --> a) " M in F } = { M where M is Subset of NTY : a in M } ; :: thesis: verum
end;
then A5: filter_image ((NTX --> a),F) = { M where M is Subset of NTY : a in M } by CARDFIL2:def 13;
reconsider S3 = { M where M is Subset of NTY : a in M } as Filter of the carrier of NTY by A5;
set S4 = { y where y is Point of NTY : S3 is_filter-finer_than U_FMT y } ;
U_FMT a c= S3
proof
now :: thesis: for x being object st x in U_FMT a holds
x in S3
let x be object ; :: thesis: ( x in U_FMT a implies x in S3 )
assume A6: x in U_FMT a ; :: thesis: x in S3
then reconsider y = x as Subset of NTY ;
a in y by A6, FINTOPO7:def 3;
hence x in S3 ; :: thesis: verum
end;
hence U_FMT a c= S3 ; :: thesis: verum
end;
then S3 is_filter-finer_than U_FMT a by CARDFIL2:def 6;
then a in { y where y is Point of NTY : S3 is_filter-finer_than U_FMT y } ;
hence (NTX --> a) . x in lim_filter ((NTX --> a),F) by FUNCOP_1:7, A5; :: thesis: verum
end;
hence NTX --> a is_continuous_at x ; :: thesis: verum
end;
end;
hence NTX --> a is continuous ; :: thesis: verum