set A3 = { ].a,b.[ where a, b is Real : ( 0 <= a & a < b & b <= 1 ) } ;
set A2 = { ].a,1.] where a is Real : ( 0 <= a & a < 1 ) } ;
set A1 = { [.0,a.[ where a is Real : ( 0 < a & a <= 1 ) } ;
reconsider B = ( { [.0,a.[ where a is Real : ( 0 < a & a <= 1 ) } \/ { ].a,1.] where a is Real : ( 0 <= a & a < 1 ) } ) \/ { ].a,b.[ where a, b is Real : ( 0 <= a & a < b & b <= 1 ) } as Basis of I[01] by Th74;
let T be non empty TopSpace; for f being Function of T,I[01] holds
( f is continuous iff for a, b being Real st 0 <= a & a < 1 & 0 < b & b <= 1 holds
( f " [.0,b.[ is open & f " ].a,1.] is open ) )
let f be Function of T,I[01]; ( f is continuous iff for a, b being Real st 0 <= a & a < 1 & 0 < b & b <= 1 holds
( f " [.0,b.[ is open & f " ].a,1.] is open ) )
hereby ( ( for a, b being Real st 0 <= a & a < 1 & 0 < b & b <= 1 holds
( f " [.0,b.[ is open & f " ].a,1.] is open ) ) implies f is continuous )
assume A1:
f is
continuous
;
for a, b being Real st 0 <= a & a < 1 & 0 < b & b <= 1 holds
( f " [.0,b.[ is open & f " ].a,1.] is open )let a,
b be
Real;
( 0 <= a & a < 1 & 0 < b & b <= 1 implies ( f " [.0,b.[ is open & f " ].a,1.] is open ) )reconsider x =
a,
y =
b as
Real ;
assume that A2:
0 <= a
and A3:
a < 1
and A4:
0 < b
and A5:
b <= 1
;
( f " [.0,b.[ is open & f " ].a,1.] is open )
].x,1.] in { ].a,1.] where a is Real : ( 0 <= a & a < 1 ) }
by A2, A3;
then
].x,1.] in { [.0,a.[ where a is Real : ( 0 < a & a <= 1 ) } \/ { ].a,1.] where a is Real : ( 0 <= a & a < 1 ) }
by XBOOLE_0:def 3;
then A6:
].x,1.] in B
by XBOOLE_0:def 3;
[.0,y.[ in { [.0,a.[ where a is Real : ( 0 < a & a <= 1 ) }
by A4, A5;
then
[.0,y.[ in { [.0,a.[ where a is Real : ( 0 < a & a <= 1 ) } \/ { ].a,1.] where a is Real : ( 0 <= a & a < 1 ) }
by XBOOLE_0:def 3;
then
[.0,y.[ in B
by XBOOLE_0:def 3;
hence
(
f " [.0,b.[ is
open &
f " ].a,1.] is
open )
by A6, A1, YELLOW_9:34;
verum
end;
assume A7:
for a, b being Real st 0 <= a & a < 1 & 0 < b & b <= 1 holds
( f " [.0,b.[ is open & f " ].a,1.] is open )
; f is continuous
now for A being Subset of I[01] st A in B holds
f " A is open let A be
Subset of
I[01];
( A in B implies f " b1 is open )assume
A in B
;
f " b1 is open then A8:
(
A in { [.0,a.[ where a is Real : ( 0 < a & a <= 1 ) } \/ { ].a,1.] where a is Real : ( 0 <= a & a < 1 ) } or
A in { ].a,b.[ where a, b is Real : ( 0 <= a & a < b & b <= 1 ) } )
by XBOOLE_0:def 3;
per cases
( A in { [.0,a.[ where a is Real : ( 0 < a & a <= 1 ) } or A in { ].a,1.] where a is Real : ( 0 <= a & a < 1 ) } or A in { ].a,b.[ where a, b is Real : ( 0 <= a & a < b & b <= 1 ) } )
by A8, XBOOLE_0:def 3;
suppose
A in { ].a,b.[ where a, b is Real : ( 0 <= a & a < b & b <= 1 ) }
;
f " b1 is open then consider a,
b being
Real such that A9:
A = ].a,b.[
and A10:
0 <= a
and A11:
a < b
and A12:
b <= 1
;
a < 1
by A11, A12, XXREAL_0:2;
then reconsider U =
f " [.0,b.[,
V =
f " ].a,1.] as
open Subset of
T by A10, A11, A7, A12;
A = [.0,b.[ /\ ].a,1.]
by A9, A10, A12, XXREAL_1:153;
then
f " A = U /\ V
by FUNCT_1:68;
hence
f " A is
open
;
verum end; end;
hence
f is continuous
by YELLOW_9:34; verum