let X, Y be non empty TopSpace; for f being Function of X,Y
for P being non empty Subset of Y
for f1 being Function of X,(Y | P) st f = f1 & f is continuous holds
f1 is continuous
let f be Function of X,Y; for P being non empty Subset of Y
for f1 being Function of X,(Y | P) st f = f1 & f is continuous holds
f1 is continuous
let P be non empty Subset of Y; for f1 being Function of X,(Y | P) st f = f1 & f is continuous holds
f1 is continuous
let f1 be Function of X,(Y | P); ( f = f1 & f is continuous implies f1 is continuous )
assume that
A1:
f = f1
and
A2:
f is continuous
; f1 is continuous
A3:
[#] Y <> {}
;
A4:
for P1 being Subset of (Y | P) st P1 is open holds
f1 " P1 is open
proof
let P1 be
Subset of
(Y | P);
( P1 is open implies f1 " P1 is open )
assume
P1 is
open
;
f1 " P1 is open
then
P1 in the
topology of
(Y | P)
by PRE_TOPC:def 2;
then consider Q being
Subset of
Y such that A5:
Q in the
topology of
Y
and A6:
P1 = Q /\ ([#] (Y | P))
by PRE_TOPC:def 4;
reconsider Q =
Q as
Subset of
Y ;
A7:
f " Q = f1 " ((rng f1) /\ Q)
by A1, RELAT_1:133;
A8:
[#] (Y | P) = P
by PRE_TOPC:def 5;
then
(rng f1) /\ Q c= P /\ Q
by XBOOLE_1:26;
then A9:
f1 " ((rng f1) /\ Q) c= f1 " P1
by A6, A8, RELAT_1:143;
Q is
open
by A5, PRE_TOPC:def 2;
then A10:
f " Q is
open
by A3, A2, TOPS_2:43;
f1 " P1 c= f " Q
by A1, A6, RELAT_1:143, XBOOLE_1:17;
hence
f1 " P1 is
open
by A10, A7, A9, XBOOLE_0:def 10;
verum
end;
[#] (Y | P) <> {}
;
hence
f1 is continuous
by A4, TOPS_2:43; verum