let X be non empty TopSpace; :: thesis: for A being Subset of X
for x being Point of X st not x in A holds
modid (X,A) is_continuous_at x
let A be Subset of X; :: thesis: for x being Point of X st not x in A holds
modid (X,A) is_continuous_at x
let x be Point of X; :: thesis: ( not x in A implies modid (X,A) is_continuous_at x )
assume A1: not x in A ; :: thesis: modid (X,A) is_continuous_at x
now :: thesis: for W being Subset of (X modified_with_respect_to A) st W is open & (modid (X,A)) . x in W holds
ex V being Subset of X st
( V is open & x in V & (modid (X,A)) .: V c= W )
let W be Subset of (X modified_with_respect_to A); :: thesis: ( W is open & (modid (X,A)) . x in W implies ex V being Subset of X st
( V is open & x in V & (modid (X,A)) .: V c= W ) )
assume that
A2: W is open and
A3: (modid (X,A)) . x in W ; :: thesis: ex V being Subset of X st
( V is open & x in V & (modid (X,A)) .: V c= W )
consider H, G being Subset of X such that
A4: W = H \/ (G /\ A) and
A5: H in the topology of X and
G in the topology of X by A2;
A6: G /\ A c= A by XBOOLE_1:17;
A7: ( x in H or x in G /\ A ) by A3, A4, XBOOLE_0:def 3;
thus ex V being Subset of X st
( V is open & x in V & (modid (X,A)) .: V c= W ) :: thesis: verum
proof
reconsider H = H as Subset of X ;
take H ; :: thesis: ( H is open & x in H & (modid (X,A)) .: H c= W )
(modid (X,A)) .: H = H by FUNCT_1:92;
hence ( H is open & x in H & (modid (X,A)) .: H c= W ) by A1, A4, A5, A7, A6, XBOOLE_1:7; :: thesis: verum
end;
end;
hence modid (X,A) is_continuous_at x by Th43; :: thesis: verum