let X, Y be non empty TopSpace; :: thesis: for S being Scott TopAugmentation of InclPoset the topology of Y ex F being Function of (InclPoset the topology of [:X,Y:]),(oContMaps X,S) st
( F is monotone & ( for W being open Subset of [:X,Y:] holds F . W = W,the carrier of X *graph ) )
let S be Scott TopAugmentation of InclPoset the topology of Y; :: thesis: ex F being Function of (InclPoset the topology of [:X,Y:]),(oContMaps X,S) st
( F is monotone & ( for W being open Subset of [:X,Y:] holds F . W = W,the carrier of X *graph ) )
deffunc H1( Element of the topology of [:X,Y:]) -> Function = $1,the carrier of X *graph ;
consider F being ManySortedSet of such that
A1:
for R being Element of the topology of [:X,Y:] holds F . R = H1(R)
from PBOOLE:sch 5();
A2:
the carrier of (InclPoset the topology of [:X,Y:]) = the topology of [:X,Y:]
by YELLOW_1:1;
A3:
dom F = the topology of [:X,Y:]
by PARTFUN1:def 4;
rng F c= the carrier of (oContMaps X,S)
proof
let y be
set ;
:: according to TARSKI:def 3 :: thesis: ( not y in rng F or y in the carrier of (oContMaps X,S) )
assume
y in rng F
;
:: thesis: y in the carrier of (oContMaps X,S)
then consider x being
set such that A4:
(
x in dom F &
y = F . x )
by FUNCT_1:def 5;
reconsider x =
x as
Element of the
topology of
[:X,Y:] by A4, PARTFUN1:def 4;
(
y = x,the
carrier of
X *graph &
x is
open Subset of
[:X,Y:] )
by A1, A4, PRE_TOPC:def 5;
then
y is
continuous Function of
X,
S
by Th44;
then
y is
Element of
(oContMaps X,S)
by Th2;
hence
y in the
carrier of
(oContMaps X,S)
;
:: thesis: verum
end;
then reconsider F = F as Function of (InclPoset the topology of [:X,Y:]),(oContMaps X,S) by A2, A3, FUNCT_2:4;
take
F
; :: thesis: ( F is monotone & ( for W being open Subset of [:X,Y:] holds F . W = W,the carrier of X *graph ) )
thus
F is monotone
:: thesis: for W being open Subset of [:X,Y:] holds F . W = W,the carrier of X *graph proof
let x,
y be
Element of
(InclPoset the topology of [:X,Y:]);
:: according to WAYBEL_1:def 2 :: thesis: ( not x <= y or F . x <= F . y )
(
x in the
topology of
[:X,Y:] &
y in the
topology of
[:X,Y:] )
by A2;
then reconsider W1 =
x,
W2 =
y as
open Subset of
[:X,Y:] by PRE_TOPC:def 5;
assume
x <= y
;
:: thesis: F . x <= F . y
then
(
W1 c= W2 &
F . x = W1,the
carrier of
X *graph &
F . y = W2,the
carrier of
X *graph )
by A1, A2, YELLOW_1:3;
hence
F . x <= F . y
by Th45;
:: thesis: verum
end;
let W be open Subset of [:X,Y:]; :: thesis: F . W = W,the carrier of X *graph
W in the topology of [:X,Y:]
by PRE_TOPC:def 5;
hence
F . W = W,the carrier of X *graph
by A1; :: thesis: verum