let X, Y be non empty TopSpace; :: thesis: for S being Scott TopAugmentation of InclPoset the topology of Y
for f being Function of X,S st *graph f is open Subset of [:X,Y:] holds
f is continuous
let S be Scott TopAugmentation of InclPoset the topology of Y; :: thesis: for f being Function of X,S st *graph f is open Subset of [:X,Y:] holds
f is continuous
let f be Function of X,S; :: thesis: ( *graph f is open Subset of [:X,Y:] implies f is continuous )
assume
*graph f is open Subset of [:X,Y:]
; :: thesis: f is continuous
then consider AA being Subset-Family of [:X,Y:] such that
A1:
*graph f = union AA
and
A2:
for e being set st e in AA holds
ex X1 being Subset of X ex Y1 being Subset of Y st
( e = [:X1,Y1:] & X1 is open & Y1 is open )
by BORSUK_1:45;
A3:
the carrier of (InclPoset the topology of Y) = the topology of Y
by YELLOW_1:1;
A4:
RelStr(# the carrier of S,the InternalRel of S #) = RelStr(# the carrier of (InclPoset the topology of Y),the InternalRel of (InclPoset the topology of Y) #)
by YELLOW_9:def 4;
A5:
dom f = the carrier of X
by FUNCT_2:def 1;
A6:
[#] S <> {}
;
now let P be
Subset of
S;
:: thesis: ( P is open implies f " P is open )assume A7:
P is
open
;
:: thesis: f " P is opennow let x be
set ;
:: thesis: ( ( x in f " P implies ex Q being Subset of X st
( Q is open & Q c= f " P & x in Q ) ) & ( ex Q being Subset of X st
( Q is open & Q c= f " P & x in Q ) implies x in f " P ) )hereby :: thesis: ( ex Q being Subset of X st
( Q is open & Q c= f " P & x in Q ) implies x in f " P )
assume A8:
x in f " P
;
:: thesis: ex Q being Subset of X st
( Q is open & Q c= f " P & x in Q )then A9:
(
x in the
carrier of
X &
f . x in P )
by FUNCT_2:46;
reconsider y =
x as
Element of
X by A8;
f . y in the
topology of
Y
by A3, A4;
then reconsider W =
f . y as
open Subset of
Y by PRE_TOPC:def 5;
defpred S1[
set ,
set ]
means (
x in $2
`1 & $1
in $2
`2 &
[:($2 `1 ),($2 `2 ):] c= *graph f );
A10:
now let e be
set ;
:: thesis: ( e in f . x implies ex u being set st
( u in [:the topology of X,the topology of Y:] & S1[e,u] ) )assume
e in f . x
;
:: thesis: ex u being set st
( u in [:the topology of X,the topology of Y:] & S1[e,u] )then
[x,e] in *graph f
by A5, A8, Th39;
then consider V being
set such that A11:
(
[x,e] in V &
V in AA )
by A1, TARSKI:def 4;
consider A being
Subset of
X,
B being
Subset of
Y such that A12:
(
V = [:A,B:] &
A is
open &
B is
open )
by A2, A11;
reconsider u =
[A,B] as
set ;
take u =
u;
:: thesis: ( u in [:the topology of X,the topology of Y:] & S1[e,u] )
(
A in the
topology of
X &
B in the
topology of
Y )
by A12, PRE_TOPC:def 5;
hence
u in [:the topology of X,the topology of Y:]
by ZFMISC_1:106;
:: thesis: S1[e,u]
(
A = u `1 &
B = u `2 )
by MCART_1:7;
hence
S1[
e,
u]
by A1, A11, A12, ZFMISC_1:92, ZFMISC_1:106;
:: thesis: verum end; consider g being
Function such that A13:
(
dom g = f . x &
rng g c= [:the topology of X,the topology of Y:] )
and A14:
for
a being
set st
a in f . x holds
S1[
a,
g . a]
from WELLORD2:sch 1(A10);
A15:
proj1 (rng g) c= the
topology of
X
by A13, FUNCT_5:13;
A16:
proj2 (rng g) c= the
topology of
Y
by A13, FUNCT_5:13;
A17:
proj2 (rng g) c= bool (f . x)
set J =
{ (union A) where A is Subset of (proj2 (rng g)) : A is finite } ;
consider A0 being
empty Subset of
(proj2 (rng g));
A21:
A0 in { (union A) where A is Subset of (proj2 (rng g)) : A is finite }
by ZFMISC_1:2;
{ (union A) where A is Subset of (proj2 (rng g)) : A is finite } c= the
topology of
Y
then reconsider J =
{ (union A) where A is Subset of (proj2 (rng g)) : A is finite } as non
empty Subset of
(InclPoset the topology of Y) by A21, YELLOW_1:1;
J is
directed
then reconsider J' =
J as non
empty directed Subset of
S by A4, WAYBEL_0:3;
union J = f . y
then
(
sup J = f . y &
ex_sup_of J,
S )
by YELLOW_0:17, YELLOW_1:22;
then
(
sup J' = f . y &
P is
inaccessible_by_directed_joins )
by A4, A7, YELLOW_0:26;
then
J meets P
by A9, WAYBEL11:def 1;
then consider a being
set such that A30:
(
a in J &
a in P )
by XBOOLE_0:3;
reconsider a =
a as
Element of
S by A30;
consider A being
Subset of
(proj2 (rng g)) such that A31:
a = union A
and A32:
A is
finite
by A30;
defpred S2[
set ,
set ]
means ex
c1 being
set st
(
[c1,$1] = g . $2 &
x in c1 & $2
in $1 & $2
in f . x &
[:c1,$1:] c= *graph f );
A33:
now let c be
set ;
:: thesis: ( c in A implies ex a being set st
( a in W & S2[c,a] ) )assume
c in A
;
:: thesis: ex a being set st
( a in W & S2[c,a] )then consider c1 being
set such that A34:
[c1,c] in rng g
by RELAT_1:def 5;
consider a being
set such that A35:
(
a in dom g &
[c1,c] = g . a )
by A34, FUNCT_1:def 5;
take a =
a;
:: thesis: ( a in W & S2[c,a] )thus
a in W
by A13, A35;
:: thesis: S2[c,a]
(
[c1,c] `1 = c1 &
[c1,c] `2 = c )
by MCART_1:7;
then
(
x in c1 &
a in c &
[:c1,c:] c= *graph f )
by A13, A14, A35;
hence
S2[
c,
a]
by A13, A35;
:: thesis: verum end; consider hh being
Function such that A36:
(
dom hh = A &
rng hh c= W )
and A37:
for
c being
set st
c in A holds
S2[
c,
hh . c]
from WELLORD2:sch 1(A33);
set B =
proj1 (g .: (rng hh));
g .: (rng hh) c= rng g
by RELAT_1:144;
then
proj1 (g .: (rng hh)) c= proj1 (rng g)
by FUNCT_5:5;
then A38:
proj1 (g .: (rng hh)) c= the
topology of
X
by A15, XBOOLE_1:1;
then reconsider B =
proj1 (g .: (rng hh)) as
Subset-Family of
X by XBOOLE_1:1;
reconsider B =
B as
Subset-Family of
X ;
reconsider Q =
Intersect B as
Subset of
X ;
take Q =
Q;
:: thesis: ( Q is open & Q c= f " P & x in Q )
g .: (rng hh) is
finite
by A32, A36, FINSET_1:17, FINSET_1:26;
then
B is
finite
by Th40;
then
Q in FinMeetCl the
topology of
X
by A38, CANTOR_1:def 4;
then
Q in the
topology of
X
by CANTOR_1:5;
hence
Q is
open
by PRE_TOPC:def 5;
:: thesis: ( Q c= f " P & x in Q )thus
Q c= f " P
:: thesis: x in Qproof
let z be
set ;
:: according to TARSKI:def 3 :: thesis: ( not z in Q or z in f " P )
assume A39:
z in Q
;
:: thesis: z in f " P
then reconsider zz =
z as
Element of
X ;
reconsider fz =
f . zz,
aa =
a as
Element of
(InclPoset the topology of Y) by A4;
a c= f . zz
proof
let p be
set ;
:: according to TARSKI:def 3 :: thesis: ( not p in a or p in f . zz )
assume
p in a
;
:: thesis: p in f . zz
then consider q being
set such that A40:
(
p in q &
q in A )
by A31, TARSKI:def 4;
consider q1 being
set such that A41:
(
[q1,q] = g . (hh . q) &
x in q1 &
hh . q in q &
hh . q in f . x &
[:q1,q:] c= *graph f )
by A37, A40;
hh . q in rng hh
by A36, A40, FUNCT_1:def 5;
then
[q1,q] in g .: (rng hh)
by A13, A41, FUNCT_1:def 12;
then
q1 in B
by RELAT_1:def 4;
then
zz in q1
by A39, SETFAM_1:58;
then
[zz,p] in [:q1,q:]
by A40, ZFMISC_1:106;
hence
p in f . zz
by A41, Th39;
:: thesis: verum
end;
then
aa <= fz
by YELLOW_1:3;
then
(
a <= f . zz &
P is
upper )
by A4, A7, YELLOW_0:1;
then
f . zz in P
by A30, WAYBEL_0:def 20;
hence
z in f " P
by FUNCT_2:46;
:: thesis: verum
end; now let c1 be
set ;
:: thesis: ( c1 in B implies x in c1 )assume
c1 in B
;
:: thesis: x in c1then consider c being
set such that A42:
[c1,c] in g .: (rng hh)
by RELAT_1:def 4;
consider b being
set such that A43:
(
b in dom g &
b in rng hh &
[c1,c] = g . b )
by A42, FUNCT_1:def 12;
consider c' being
set such that A44:
(
c' in dom hh &
b = hh . c' )
by A43, FUNCT_1:def 5;
consider c'1 being
set such that A45:
(
[c'1,c'] = g . (hh . c') &
x in c'1 &
hh . c' in c' &
hh . c' in f . x &
[:c'1,c':] c= *graph f )
by A36, A37, A44;
thus
x in c1
by A43, A44, A45, ZFMISC_1:33;
:: thesis: verum end; hence
x in Q
by A8, SETFAM_1:58;
:: thesis: verum
end; assume
ex
Q being
Subset of
X st
(
Q is
open &
Q c= f " P &
x in Q )
;
:: thesis: x in f " Phence
x in f " P
;
:: thesis: verum end; hence
f " P is
open
by TOPS_1:57;
:: thesis: verum end;
hence
f is continuous
by A6, TOPS_2:55; :: thesis: verum