let X, Y be non empty TopSpace; :: thesis: 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; :: thesis: 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; :: thesis: 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); :: thesis: ( f = f1 & f is continuous implies f1 is continuous )
A1:
( [#] Y <> {} & [#] (Y | P) <> {} )
;
assume A2:
( f = f1 & f is continuous )
; :: thesis: f1 is continuous
for P1 being Subset of (Y | P) st P1 is open holds
f1 " P1 is open
proof
let P1 be
Subset of
(Y | P);
:: thesis: ( P1 is open implies f1 " P1 is open )
assume
P1 is
open
;
:: thesis: f1 " P1 is open
then
P1 in the
topology of
(Y | P)
by PRE_TOPC:def 5;
then consider Q being
Subset of
Y such that A4:
(
Q in the
topology of
Y &
P1 = Q /\ ([#] (Y | P)) )
by PRE_TOPC:def 9;
reconsider Q =
Q as
Subset of
Y ;
Q is
open
by A4, PRE_TOPC:def 5;
then A5:
f " Q is
open
by A1, A2, TOPS_2:55;
A6:
[#] (Y | P) = P
by PRE_TOPC:def 10;
A7:
f " Q = f1 " ((rng f1) /\ Q)
by A2, RELAT_1:168;
A8:
f1 " P1 c= f " Q
by A2, A4, RELAT_1:178, XBOOLE_1:17;
rng f1 c= P
by A6;
then
(rng f1) /\ Q c= P /\ Q
by XBOOLE_1:26;
then
f1 " ((rng f1) /\ Q) c= f1 " P1
by A4, A6, RELAT_1:178;
hence
f1 " P1 is
open
by A5, A7, A8, XBOOLE_0:def 10;
:: thesis: verum
end;
hence
f1 is continuous
by A1, TOPS_2:55; :: thesis: verum