let X, Y be non empty TopSpace; for f being Function of X,Y
for X0 being non empty SubSpace of X
for A being Subset of X
for x being Point of X
for x0 being Point of X0 st A c= the carrier of X0 & A is a_neighborhood of x & x = x0 holds
( f is_continuous_at x iff f | X0 is_continuous_at x0 )
let f be Function of X,Y; for X0 being non empty SubSpace of X
for A being Subset of X
for x being Point of X
for x0 being Point of X0 st A c= the carrier of X0 & A is a_neighborhood of x & x = x0 holds
( f is_continuous_at x iff f | X0 is_continuous_at x0 )
let X0 be non empty SubSpace of X; for A being Subset of X
for x being Point of X
for x0 being Point of X0 st A c= the carrier of X0 & A is a_neighborhood of x & x = x0 holds
( f is_continuous_at x iff f | X0 is_continuous_at x0 )
let A be Subset of X; for x being Point of X
for x0 being Point of X0 st A c= the carrier of X0 & A is a_neighborhood of x & x = x0 holds
( f is_continuous_at x iff f | X0 is_continuous_at x0 )
let x be Point of X; for x0 being Point of X0 st A c= the carrier of X0 & A is a_neighborhood of x & x = x0 holds
( f is_continuous_at x iff f | X0 is_continuous_at x0 )
let x0 be Point of X0; ( A c= the carrier of X0 & A is a_neighborhood of x & x = x0 implies ( f is_continuous_at x iff f | X0 is_continuous_at x0 ) )
assume that
A1:
A c= the carrier of X0
and
A2:
A is a_neighborhood of x
and
A3:
x = x0
; ( f is_continuous_at x iff f | X0 is_continuous_at x0 )
thus
( f is_continuous_at x implies f | X0 is_continuous_at x0 )
by A3, Th58; ( f | X0 is_continuous_at x0 implies f is_continuous_at x )
thus
( f | X0 is_continuous_at x0 implies f is_continuous_at x )
verumproof
assume A4:
f | X0 is_continuous_at x0
;
f is_continuous_at x
for
G being
Subset of
Y st
G is
open &
f . x in G holds
ex
H being
Subset of
X st
(
H is
open &
x in H &
f .: H c= G )
proof
let G be
Subset of
Y;
( G is open & f . x in G implies ex H being Subset of X st
( H is open & x in H & f .: H c= G ) )
assume that A5:
G is
open
and A6:
f . x in G
;
ex H being Subset of X st
( H is open & x in H & f .: H c= G )
(f | X0) . x0 in G
by A3, A6, FUNCT_1:49;
then consider H0 being
Subset of
X0 such that A7:
H0 is
open
and A8:
x0 in H0
and A9:
(f | X0) .: H0 c= G
by A4, A5, Th43;
consider V being
Subset of
X such that A10:
V is
open
and A11:
V c= A
and A12:
x in V
by A2, CONNSP_2:6;
reconsider V0 =
V as
Subset of
X0 by A1, A11, XBOOLE_1:1;
A13:
H0 /\ V0 c= V
by XBOOLE_1:17;
then reconsider H =
H0 /\ V0 as
Subset of
X by XBOOLE_1:1;
A14:
for
z being
Point of
Y st
z in f .: H holds
z in G
take
H
;
( H is open & x in H & f .: H c= G )
V0 is
open
by A10, TOPS_2:25;
then
H0 /\ V0 is
open
by A7;
hence
(
H is
open &
x in H &
f .: H c= G )
by A3, A8, A10, A12, A13, A14, SUBSET_1:2, TSEP_1:9, XBOOLE_0:def 4;
verum
end;
hence
f is_continuous_at x
by Th43;
verum
end;