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