let Y, X be non empty TopSpace; :: thesis: for f being Function of X,Y
for X0 being non empty SubSpace of X
for x being Point of X
for x0 being Point of X0 st x = x0 & f is_continuous_at x holds
f | X0 is_continuous_at x0
let f be Function of X,Y; :: thesis: for X0 being non empty SubSpace of X
for x being Point of X
for x0 being Point of X0 st x = x0 & f is_continuous_at x holds
f | X0 is_continuous_at x0
let X0 be non empty SubSpace of X; :: thesis: for x being Point of X
for x0 being Point of X0 st x = x0 & f is_continuous_at x holds
f | X0 is_continuous_at x0
let x be Point of X; :: thesis: for x0 being Point of X0 st x = x0 & f is_continuous_at x holds
f | X0 is_continuous_at x0
let x0 be Point of X0; :: thesis: ( x = x0 & f is_continuous_at x implies f | X0 is_continuous_at x0 )
assume A1:
x = x0
; :: thesis: ( not f is_continuous_at x or f | X0 is_continuous_at x0 )
assume A2:
f is_continuous_at x
; :: thesis: f | X0 is_continuous_at x0
for G being Subset of Y st G is open & (f | X0) . x0 in G holds
ex H0 being Subset of X0 st
( H0 is open & x0 in H0 & (f | X0) .: H0 c= G )
proof
let G be
Subset of
Y;
:: thesis: ( G is open & (f | X0) . x0 in G implies ex H0 being Subset of X0 st
( H0 is open & x0 in H0 & (f | X0) .: H0 c= G ) )
assume that A3:
G is
open
and A4:
(f | X0) . x0 in G
;
:: thesis: ex H0 being Subset of X0 st
( H0 is open & x0 in H0 & (f | X0) .: H0 c= G )
f . x in G
by A1, A4, FUNCT_1:72;
then consider H being
Subset of
X such that A5:
H is
open
and A6:
x in H
and A7:
f .: H c= G
by A2, A3, Th48;
reconsider C = the
carrier of
X0 as
Subset of
X by TSEP_1:1;
reconsider H0 =
H /\ C as
Subset of
X0 by XBOOLE_1:17;
take
H0
;
:: thesis: ( H0 is open & x0 in H0 & (f | X0) .: H0 c= G )
A8:
(
H0 = H /\ ([#] X0) &
x in H0 )
by A1, A6, XBOOLE_0:def 4;
A9:
(f | X0) .: H0 c= f .: H0
by RELAT_1:161;
(
f .: H0 c= (f .: H) /\ (f .: C) &
(f .: H) /\ (f .: C) c= f .: H )
by RELAT_1:154, XBOOLE_1:17;
then
f .: H0 c= f .: H
by XBOOLE_1:1;
then
f .: H0 c= G
by A7, XBOOLE_1:1;
hence
(
H0 is
open &
x0 in H0 &
(f | X0) .: H0 c= G )
by A1, A5, A8, A9, TOPS_2:32, XBOOLE_1:1;
:: thesis: verum
end;
hence
f | X0 is_continuous_at x0
by Th48; :: thesis: verum