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