let sn be Real; for K0, B0 being Subset of (TOP-REAL 2)
for f being Function of ((TOP-REAL 2) | K0),((TOP-REAL 2) | B0) st - 1 < sn & sn < 1 & f = (sn -FanMorphE ) | K0 & B0 = NonZero (TOP-REAL 2) & K0 = { p where p is Point of (TOP-REAL 2) : ( p `1 <= 0 & p <> 0. (TOP-REAL 2) ) } holds
f is continuous
let K0, B0 be Subset of (TOP-REAL 2); for f being Function of ((TOP-REAL 2) | K0),((TOP-REAL 2) | B0) st - 1 < sn & sn < 1 & f = (sn -FanMorphE ) | K0 & B0 = NonZero (TOP-REAL 2) & K0 = { p where p is Point of (TOP-REAL 2) : ( p `1 <= 0 & p <> 0. (TOP-REAL 2) ) } holds
f is continuous
let f be Function of ((TOP-REAL 2) | K0),((TOP-REAL 2) | B0); ( - 1 < sn & sn < 1 & f = (sn -FanMorphE ) | K0 & B0 = NonZero (TOP-REAL 2) & K0 = { p where p is Point of (TOP-REAL 2) : ( p `1 <= 0 & p <> 0. (TOP-REAL 2) ) } implies f is continuous )
set cn = sqrt (1 - (sn ^2 ));
set p0 = |[(- (sqrt (1 - (sn ^2 )))),(- sn)]|;
assume A1:
( - 1 < sn & sn < 1 & f = (sn -FanMorphE ) | K0 & B0 = NonZero (TOP-REAL 2) & K0 = { p where p is Point of (TOP-REAL 2) : ( p `1 <= 0 & p <> 0. (TOP-REAL 2) ) } )
; f is continuous
then
sn ^2 < 1 ^2
by SQUARE_1:120;
then
1 - (sn ^2 ) > 0
by XREAL_1:52;
then
- (- (sqrt (1 - (sn ^2 )))) > 0
by SQUARE_1:93;
then A2:
( |[(- (sqrt (1 - (sn ^2 )))),(- sn)]| `1 = - (sqrt (1 - (sn ^2 ))) & - (sqrt (1 - (sn ^2 ))) < 0 )
by EUCLID:56;
then
|[(- (sqrt (1 - (sn ^2 )))),(- sn)]| in K0
by A1, JGRAPH_2:11;
then reconsider K1 = K0 as non empty Subset of (TOP-REAL 2) ;
not |[(- (sqrt (1 - (sn ^2 )))),(- sn)]| in {(0. (TOP-REAL 2))}
by A2, JGRAPH_2:11, TARSKI:def 1;
then reconsider D = B0 as non empty Subset of (TOP-REAL 2) by A1, XBOOLE_0:def 5;
A3:
K1 c= D
for p being Point of ((TOP-REAL 2) | K1)
for V being Subset of ((TOP-REAL 2) | D) st f . p in V & V is open holds
ex W being Subset of ((TOP-REAL 2) | K1) st
( p in W & W is open & f .: W c= V )
proof
let p be
Point of
((TOP-REAL 2) | K1);
for V being Subset of ((TOP-REAL 2) | D) st f . p in V & V is open holds
ex W being Subset of ((TOP-REAL 2) | K1) st
( p in W & W is open & f .: W c= V )let V be
Subset of
((TOP-REAL 2) | D);
( f . p in V & V is open implies ex W being Subset of ((TOP-REAL 2) | K1) st
( p in W & W is open & f .: W c= V ) )
assume that A6:
f . p in V
and A7:
V is
open
;
ex W being Subset of ((TOP-REAL 2) | K1) st
( p in W & W is open & f .: W c= V )
consider V2 being
Subset of
(TOP-REAL 2) such that A8:
V2 is
open
and A9:
V2 /\ ([#] ((TOP-REAL 2) | D)) = V
by A7, TOPS_2:32;
reconsider W2 =
V2 /\ ([#] ((TOP-REAL 2) | K1)) as
Subset of
((TOP-REAL 2) | K1) ;
A10:
[#] ((TOP-REAL 2) | K1) = K1
by PRE_TOPC:def 10;
then A11:
f . p = (sn -FanMorphE ) . p
by A1, FUNCT_1:72;
A12:
f .: W2 c= V
proof
let y be
set ;
TARSKI:def 3 ( not y in f .: W2 or y in V )
assume
y in f .: W2
;
y in V
then consider x being
set such that A13:
x in dom f
and A14:
x in W2
and A15:
y = f . x
by FUNCT_1:def 12;
f is
Function of
((TOP-REAL 2) | K1),
((TOP-REAL 2) | D)
;
then
dom f = K1
by A10, FUNCT_2:def 1;
then consider p4 being
Point of
(TOP-REAL 2) such that A16:
x = p4
and A17:
p4 `1 <= 0
and
p4 <> 0. (TOP-REAL 2)
by A1, A13;
A18:
p4 in V2
by A14, A16, XBOOLE_0:def 4;
p4 in [#] ((TOP-REAL 2) | K1)
by A13, A16;
then
p4 in D
by A3, A10;
then A19:
p4 in [#] ((TOP-REAL 2) | D)
by PRE_TOPC:def 10;
f . p4 =
(sn -FanMorphE ) . p4
by A1, A10, A13, A16, FUNCT_1:72
.=
p4
by A17, Th89
;
hence
y in V
by A9, A15, A16, A18, A19, XBOOLE_0:def 4;
verum
end;
p in the
carrier of
((TOP-REAL 2) | K1)
;
then consider q being
Point of
(TOP-REAL 2) such that A20:
q = p
and A21:
q `1 <= 0
and
q <> 0. (TOP-REAL 2)
by A1, A10;
(sn -FanMorphE ) . q = q
by A21, Th89;
then
p in V2
by A6, A9, A11, A20, XBOOLE_0:def 4;
then A22:
p in W2
by XBOOLE_0:def 4;
W2 is
open
by A8, TOPS_2:32;
hence
ex
W being
Subset of
((TOP-REAL 2) | K1) st
(
p in W &
W is
open &
f .: W c= V )
by A22, A12;
verum
end;
hence
f is continuous
by JGRAPH_2:20; verum