let X, Y be non empty TopSpace; :: thesis: 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; :: thesis: 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; :: thesis: 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; :: thesis: 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; :: thesis: ( 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 A1:
( 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 ) ) )
; :: thesis: 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
let p be
Point of
X;
:: thesis: 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;
:: thesis: ( 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 A2:
(
f . p in V &
V is
open )
;
:: thesis: ex W being Subset of X st
( p in W & W is open & f .: W c= V )
A3:
the
carrier of
(X | D) = D
by PRE_TOPC:29;
per cases
( p = p0 or p <> p0 )
;
suppose A4:
p <> p0
;
:: thesis: 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 A5:
p in (D ` ) `
by SUBSET_1:def 5;
then
f . p <> f . p0
by A1, A3;
then consider G1,
G2 being
Subset of
Y such that A6:
(
G1 is
open &
G2 is
open &
f . p in G1 &
f . p0 in G2 &
G1 misses G2 )
by A1, PRE_TOPC:def 16;
consider h being
Function of
(X | D),
(Y | E) such that A7:
(
h = f | D &
h is
continuous )
by A1;
A8:
[#] (X | D) = D
by PRE_TOPC:def 10;
then reconsider p22 =
p as
Point of
(X | D) by A5;
A9:
[#] (Y | E) = E
by PRE_TOPC:def 10;
then reconsider V20 =
(G1 /\ V) /\ E as
Subset of
(Y | E) by XBOOLE_1:17;
A10:
h . p = f . p
by A5, A7, FUNCT_1:72;
f . p <> f . p0
by A1, A5, A8;
then
not
f . p in E `
by A1, TARSKI:def 1;
then
not
f . p in the
carrier of
Y \ E
by SUBSET_1:def 5;
then A11:
h . p22 in E
by A10, XBOOLE_0:def 5;
h . p22 in G1 /\ V
by A2, A6, A10, XBOOLE_0:def 4;
then A12:
h . p22 in V20
by A11, XBOOLE_0:def 4;
G1 /\ V is
open
by A2, A6, TOPS_1:38;
then
V20 is
open
by A9, TOPS_2:32;
then consider W2 being
Subset of
(X | D) such that A13:
(
p22 in W2 &
W2 is
open &
h .: W2 c= V20 )
by A7, A12, JGRAPH_2:20;
consider W3b being
Subset of
X such that A14:
(
W3b is
open &
W2 = W3b /\ ([#] (X | D)) )
by A13, TOPS_2:32;
A15:
p22 in W3b
by A13, A14, XBOOLE_0:def 4;
consider H1,
H2 being
Subset of
X such that A16:
(
H1 is
open &
H2 is
open &
p in H1 &
p0 in H2 &
H1 misses H2 )
by A1, A4, PRE_TOPC:def 16;
A17:
H1 /\ W3b is
open
by A14, A16, TOPS_1:38;
A18:
p in H1 /\ W3b
by A15, A16, XBOOLE_0:def 4;
reconsider W3 =
H1 /\ W3b as
Subset of
X ;
A19:
W3 c= W3b
by XBOOLE_1:17;
A20:
f .: W3 c= h .: W2
proof
let xx be
set ;
:: according to TARSKI:def 3 :: thesis: ( not xx in f .: W3 or xx in h .: W2 )
assume
xx in f .: W3
;
:: thesis: xx in h .: W2
then consider yy being
set such that A21:
(
yy in dom f &
yy in W3 &
xx = f . yy )
by FUNCT_1:def 12;
A22:
dom h = (dom f) /\ D
by A7, RELAT_1:90;
A23:
W3 c= H1
by XBOOLE_1:17;
H2 c= H1 `
by A16, SUBSET_1:43;
then
D ` c= H1 `
by A1, A16, ZFMISC_1:37;
then
H1 c= D
by SUBSET_1:31;
then A24:
W3 c= D
by A23, XBOOLE_1:1;
then A25:
yy in dom h
by A21, A22, XBOOLE_0:def 4;
then A26:
h . yy = f . yy
by A7, FUNCT_1:70;
yy in W2
by A8, A14, A19, A21, A24, XBOOLE_0:def 4;
hence
xx in h .: W2
by A21, A25, A26, FUNCT_1:def 12;
:: thesis: verum
end; A27:
(G1 /\ V) /\ E c= G1 /\ V
by XBOOLE_1:17;
A28:
G1 /\ V c= V
by XBOOLE_1:17;
h .: W2 c= G1 /\ V
by A13, A27, XBOOLE_1:1;
then
h .: W2 c= V
by A28, XBOOLE_1:1;
hence
ex
W being
Subset of
X st
(
p in W &
W is
open &
f .: W c= V )
by A17, A18, A20, XBOOLE_1:1;
:: thesis: verum end;
end;
hence
f is continuous
by JGRAPH_2:20; :: thesis: verum