let X, Y be non empty TopSpace; for p0 being Point of X
for D being non empty Subset of X
for E being non empty Subset of Y
for f being Function of X,Y st D ` = {p0} & E ` = {(f . p0)} & X is T_2 & Y is T_2 & ( for p being Point of (X | D) holds f . p <> f . p0 ) & f | D is continuous Function of (X | D),(Y | E) & ( for V being Subset of Y st f . p0 in V & V is open holds
ex W being Subset of X st
( p0 in W & W is open & f .: W c= V ) ) holds
f is continuous
let p0 be Point of X; for D being non empty Subset of X
for E being non empty Subset of Y
for f being Function of X,Y st D ` = {p0} & E ` = {(f . p0)} & X is T_2 & Y is T_2 & ( for p being Point of (X | D) holds f . p <> f . p0 ) & f | D is continuous Function of (X | D),(Y | E) & ( for V being Subset of Y st f . p0 in V & V is open holds
ex W being Subset of X st
( p0 in W & W is open & f .: W c= V ) ) holds
f is continuous
let D be non empty Subset of X; for E being non empty Subset of Y
for f being Function of X,Y st D ` = {p0} & E ` = {(f . p0)} & X is T_2 & Y is T_2 & ( for p being Point of (X | D) holds f . p <> f . p0 ) & f | D is continuous Function of (X | D),(Y | E) & ( for V being Subset of Y st f . p0 in V & V is open holds
ex W being Subset of X st
( p0 in W & W is open & f .: W c= V ) ) holds
f is continuous
let E be non empty Subset of Y; for f being Function of X,Y st D ` = {p0} & E ` = {(f . p0)} & X is T_2 & Y is T_2 & ( for p being Point of (X | D) holds f . p <> f . p0 ) & f | D is continuous Function of (X | D),(Y | E) & ( for V being Subset of Y st f . p0 in V & V is open holds
ex W being Subset of X st
( p0 in W & W is open & f .: W c= V ) ) holds
f is continuous
let f be Function of X,Y; ( D ` = {p0} & E ` = {(f . p0)} & X is T_2 & Y is T_2 & ( for p being Point of (X | D) holds f . p <> f . p0 ) & f | D is continuous Function of (X | D),(Y | E) & ( for V being Subset of Y st f . p0 in V & V is open holds
ex W being Subset of X st
( p0 in W & W is open & f .: W c= V ) ) implies f is continuous )
assume that
A1:
D ` = {p0}
and
A2:
E ` = {(f . p0)}
and
A3:
X is T_2
and
A4:
Y is T_2
and
A5:
for p being Point of (X | D) holds f . p <> f . p0
and
A6:
f | D is continuous Function of (X | D),(Y | E)
and
A7:
for V being Subset of Y st f . p0 in V & V is open holds
ex W being Subset of X st
( p0 in W & W is open & f .: W c= V )
; f is continuous
for p being Point of X
for V being Subset of Y st f . p in V & V is open holds
ex W being Subset of X st
( p in W & W is open & f .: W c= V )
proof
A8:
the
carrier of
(X | D) = D
by PRE_TOPC:8;
let p be
Point of
X;
for V being Subset of Y st f . p in V & V is open holds
ex W being Subset of X st
( p in W & W is open & f .: W c= V )let V be
Subset of
Y;
( f . p in V & V is open implies ex W being Subset of X st
( p in W & W is open & f .: W c= V ) )
assume that A9:
f . p in V
and A10:
V is
open
;
ex W being Subset of X st
( p in W & W is open & f .: W c= V )
per cases
( p = p0 or p <> p0 )
;
suppose A11:
p <> p0
;
ex W being Subset of X st
( p in W & W is open & f .: W c= V )then
not
p in D `
by A1, TARSKI:def 1;
then
p in the
carrier of
X \ (D `)
by XBOOLE_0:def 5;
then A12:
p in (D `) `
by SUBSET_1:def 4;
then
f . p <> f . p0
by A5, A8;
then consider G1,
G2 being
Subset of
Y such that A13:
G1 is
open
and
G2 is
open
and A14:
f . p in G1
and
f . p0 in G2
and
G1 misses G2
by A4, PRE_TOPC:def 10;
A15:
[#] (X | D) = D
by PRE_TOPC:def 5;
then reconsider p22 =
p as
Point of
(X | D) by A12;
consider h being
Function of
(X | D),
(Y | E) such that A16:
h = f | D
and A17:
h is
continuous
by A6;
A18:
h . p = f . p
by A12, A16, FUNCT_1:49;
A19:
[#] (Y | E) = E
by PRE_TOPC:def 5;
then reconsider V20 =
(G1 /\ V) /\ E as
Subset of
(Y | E) by XBOOLE_1:17;
G1 /\ V is
open
by A10, A13, TOPS_1:11;
then A20:
V20 is
open
by A19, TOPS_2:24;
f . p <> f . p0
by A5, A12, A15;
then
not
f . p in E `
by A2, TARSKI:def 1;
then
not
f . p in the
carrier of
Y \ E
by SUBSET_1:def 4;
then A21:
h . p22 in E
by A18, XBOOLE_0:def 5;
h . p22 in G1 /\ V
by A9, A14, A18, XBOOLE_0:def 4;
then
h . p22 in V20
by A21, XBOOLE_0:def 4;
then consider W2 being
Subset of
(X | D) such that A22:
p22 in W2
and A23:
W2 is
open
and A24:
h .: W2 c= V20
by A17, A20, JGRAPH_2:10;
consider W3b being
Subset of
X such that A25:
W3b is
open
and A26:
W2 = W3b /\ ([#] (X | D))
by A23, TOPS_2:24;
consider H1,
H2 being
Subset of
X such that A27:
H1 is
open
and
H2 is
open
and A28:
p in H1
and A29:
p0 in H2
and A30:
H1 misses H2
by A3, A11, PRE_TOPC:def 10;
p22 in W3b
by A22, A26, XBOOLE_0:def 4;
then A31:
p in H1 /\ W3b
by A28, XBOOLE_0:def 4;
reconsider W3 =
H1 /\ W3b as
Subset of
X ;
A32:
W3 c= W3b
by XBOOLE_1:17;
A33:
f .: W3 c= h .: W2
proof
let xx be
object ;
TARSKI:def 3 ( not xx in f .: W3 or xx in h .: W2 )
assume
xx in f .: W3
;
xx in h .: W2
then consider yy being
object such that A34:
yy in dom f
and A35:
yy in W3
and A36:
xx = f . yy
by FUNCT_1:def 6;
H2 c= H1 `
by A30, SUBSET_1:23;
then
D ` c= H1 `
by A1, A29, ZFMISC_1:31;
then
(
W3 c= H1 &
H1 c= D )
by SUBSET_1:12, XBOOLE_1:17;
then A37:
W3 c= D
;
then A38:
yy in W2
by A15, A26, A32, A35, XBOOLE_0:def 4;
dom h = (dom f) /\ D
by A16, RELAT_1:61;
then A39:
yy in dom h
by A34, A35, A37, XBOOLE_0:def 4;
then
h . yy = f . yy
by A16, FUNCT_1:47;
hence
xx in h .: W2
by A36, A39, A38, FUNCT_1:def 6;
verum
end;
(G1 /\ V) /\ E c= G1 /\ V
by XBOOLE_1:17;
then
(
G1 /\ V c= V &
h .: W2 c= G1 /\ V )
by A24, XBOOLE_1:17;
then A40:
h .: W2 c= V
;
H1 /\ W3b is
open
by A25, A27, TOPS_1:11;
hence
ex
W being
Subset of
X st
(
p in W &
W is
open &
f .: W c= V )
by A31, A33, A40, XBOOLE_1:1;
verum end;
end;
hence
f is continuous
by JGRAPH_2:10; verum