let X, Y be non empty TopSpace; 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; 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 the topology of [:X,Y:] such that
A1:
for R being Element of the topology of [:X,Y:] holds F . R = H1(R)
from PBOOLE:sch 5();
A2:
rng F c= the carrier of (oContMaps (X,S))
proof
let y be
object ;
TARSKI:def 3 ( not y in rng F or y in the carrier of (oContMaps (X,S)) )
assume
y in rng F
;
y in the carrier of (oContMaps (X,S))
then consider x being
object such that A3:
x in dom F
and A4:
y = F . x
by FUNCT_1:def 3;
reconsider x =
x as
Element of the
topology of
[:X,Y:] by A3;
A5:
x is
open Subset of
[:X,Y:]
by PRE_TOPC:def 2;
y = (
x, the
carrier of
X)
*graph
by A1, A4;
then
y is
continuous Function of
X,
S
by A5, Th43;
then
y is
Element of
(oContMaps (X,S))
by Th2;
hence
y in the
carrier of
(oContMaps (X,S))
;
verum
end;
A6:
dom F = the topology of [:X,Y:]
by PARTFUN1:def 2;
A7:
the carrier of (InclPoset the topology of [:X,Y:]) = the topology of [:X,Y:]
by YELLOW_1:1;
then reconsider F = F as Function of (InclPoset the topology of [:X,Y:]),(oContMaps (X,S)) by A6, A2, FUNCT_2:2;
take
F
; ( F is monotone & ( for W being open Subset of [:X,Y:] holds F . W = (W, the carrier of X) *graph ) )
thus
F is monotone
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:]);
WAYBEL_1:def 2 ( not x <= y or F . x <= F . y )
(
x in the
topology of
[:X,Y:] &
y in the
topology of
[:X,Y:] )
by A7;
then reconsider W1 =
x,
W2 =
y as
open Subset of
[:X,Y:] by PRE_TOPC:def 2;
assume
x <= y
;
F . x <= F . y
then A8:
W1 c= W2
by YELLOW_1:3;
(
F . x = (
W1, the
carrier of
X)
*graph &
F . y = (
W2, the
carrier of
X)
*graph )
by A1, A7;
hence
F . x <= F . y
by A8, Th44;
verum
end;
let W be open Subset of [:X,Y:]; F . W = (W, the carrier of X) *graph
W in the topology of [:X,Y:]
by PRE_TOPC:def 2;
hence
F . W = (W, the carrier of X) *graph
by A1; verum