let X, Y be non empty TopSpace; 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; 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; 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; 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; ( x = x0 & f is_continuous_at x implies f | X0 is_continuous_at x0 )
assume A1:
x = x0
; ( not f is_continuous_at x or f | X0 is_continuous_at x0 )
assume A2:
f is_continuous_at x
; 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
reconsider C = the
carrier of
X0 as
Subset of
X by TSEP_1:1;
let G be
Subset of
Y;
( 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
;
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:49;
then consider H being
Subset of
X such that A5:
(
H is
open &
x in H )
and A6:
f .: H c= G
by A2, A3, Th43;
reconsider H0 =
H /\ C as
Subset of
X0 by XBOOLE_1:17;
(
f .: H0 c= (f .: H) /\ (f .: C) &
(f .: H) /\ (f .: C) c= f .: H )
by RELAT_1:121, XBOOLE_1:17;
then
f .: H0 c= f .: H
by XBOOLE_1:1;
then A7:
f .: H0 c= G
by A6, XBOOLE_1:1;
take
H0
;
( H0 is open & x0 in H0 & (f | X0) .: H0 c= G )
(
H0 = H /\ ([#] X0) &
(f | X0) .: H0 c= f .: H0 )
by RELAT_1:128;
hence
(
H0 is
open &
x0 in H0 &
(f | X0) .: H0 c= G )
by A1, A5, A7, TOPS_2:24, XBOOLE_0:def 4, XBOOLE_1:1;
verum
end;
hence
f | X0 is_continuous_at x0
by Th43; verum