let T be TopStruct ; for f being RealMap of T st f is continuous & not 0 in rng f holds
Inv f is continuous
let f be RealMap of T; ( f is continuous & not 0 in rng f implies Inv f is continuous )
assume that
A1:
f is continuous
and
A2:
not 0 in rng f
; Inv f is continuous
let X0 be Subset of REAL; PSCOMP_1:def 3 ( X0 is closed implies (Inv f) " X0 is closed )
0 in {0}
by TARSKI:def 1;
then
not 0 in X0 \ {0}
by XBOOLE_0:def 5;
then reconsider X = X0 \ {0} as without_zero Subset of REAL by MEASURE6:def 2;
set X9 = Inv X;
A3:
X0 \ {0} c= X0
by XBOOLE_1:36;
set X9r = (Inv X) /\ (rng f);
assume A4:
X0 is closed
; (Inv f) " X0 is closed
now for x being object holds
( ( x in (Inv X) /\ (rng f) implies x in (Cl ((Inv X) /\ (rng f))) /\ (rng f) ) & ( x in (Cl ((Inv X) /\ (rng f))) /\ (rng f) implies x in (Inv X) /\ (rng f) ) )let x be
object ;
( ( x in (Inv X) /\ (rng f) implies x in (Cl ((Inv X) /\ (rng f))) /\ (rng f) ) & ( x in (Cl ((Inv X) /\ (rng f))) /\ (rng f) implies x in (Inv X) /\ (rng f) ) )assume A7:
x in (Cl ((Inv X) /\ (rng f))) /\ (rng f)
;
x in (Inv X) /\ (rng f)then reconsider s =
x as
Real ;
x in Cl ((Inv X) /\ (rng f))
by A7, XBOOLE_0:def 4;
then consider seq being
Real_Sequence such that A8:
rng seq c= (Inv X) /\ (rng f)
and A9:
seq is
convergent
and A10:
lim seq = s
by MEASURE6:64;
assume A11:
not
x in (Inv X) /\ (rng f)
;
contradictionA12:
x in rng f
by A7, XBOOLE_0:def 4;
now not lim seq <> 0
rng (seq ") c= X
then A16:
rng (seq ") c= X0
by A3;
assume A17:
lim seq <> 0
;
contradictionnow for n being Nat holds not seq . n = 0 end; then A19:
seq is
non-zero
by SEQ_1:5;
then
seq " is
convergent
by A9, A17, SEQ_2:21;
then A20:
lim (seq ") in X0
by A4, A16;
A21:
lim (seq ") = (lim seq) "
by A9, A17, A19, SEQ_2:22;
then
lim (seq ") <> 0
by A17;
then
not
lim (seq ") in {0}
by TARSKI:def 1;
then
lim (seq ") in X
by A20, XBOOLE_0:def 5;
then
1
/ (lim (seq ")) in Inv X
;
hence
contradiction
by A12, A10, A11, A21, XBOOLE_0:def 4;
verum end; hence
contradiction
by A2, A7, A10, XBOOLE_0:def 4;
verum end;
then A22:
(Inv X) /\ (rng f) = (Cl ((Inv X) /\ (rng f))) /\ (rng f)
by TARSKI:2;
f " (Cl ((Inv X) /\ (rng f))) is closed
by A1;
then A23:
f " ((Inv X) /\ (rng f)) is closed
by A22, RELAT_1:133;
( f " (Inv X) = f " ((Inv X) /\ (rng f)) & (Inv f) " X = f " (Inv X) )
by MEASURE6:71, RELAT_1:133;
hence
(Inv f) " X0 is closed
by A23, A24, TARSKI:2; verum