let L be complete continuous LATTICE; :: thesis: for T being Scott TopAugmentation of L holds T is injective
let T be Scott TopAugmentation of L; :: thesis: T is injective
let X be non empty TopSpace; :: according to WAYBEL18:def 5 :: thesis: for b₁ being Element of bool [:the carrier of X,the carrier of T:] holds
( not b₁ is continuous or for b₂ being TopStruct holds
( not X is SubSpace of b₂ or ex b₃ being Element of bool [:the carrier of b₂,the carrier of T:] st
( b₃ is continuous & b₃ | the carrier of X = b₁ ) ) )
let f be Function of X,T; :: thesis: ( not f is continuous or for b₁ being TopStruct holds
( not X is SubSpace of b₁ or ex b₂ being Element of bool [:the carrier of b₁,the carrier of T:] st
( b₂ is continuous & b₂ | the carrier of X = f ) ) )
assume A1: f is continuous ; :: thesis: for b₁ being TopStruct holds
( not X is SubSpace of b₁ or ex b₂ being Element of bool [:the carrier of b₁,the carrier of T:] st
( b₂ is continuous & b₂ | the carrier of X = f ) )
let Y be non empty TopSpace; :: thesis: ( not X is SubSpace of Y or ex b₁ being Element of bool [:the carrier of Y,the carrier of T:] st
( b₁ is continuous & b₁ | the carrier of X = f ) )
assume A2: X is SubSpace of Y ; :: thesis: ex b₁ being Element of bool [:the carrier of Y,the carrier of T:] st
( b₁ is continuous & b₁ | the carrier of X = f )
deffunc H₁( set ) -> Element of the carrier of T = "\/" { (inf (f .: (V /\ the carrier of X))) where V is open Subset of Y : $1 in V } ,T;
consider g being Function of the carrier of Y,the carrier of T such that
A3: for x being Element of Y holds g . x = H₁(x) from FUNCT_2:sch 4();
reconsider g = g as Function of Y,T ;
take g ; :: thesis: ( g is continuous & g | the carrier of X = f )
A4: [#] T <> {} ;
for P being Subset of T st P is open holds
g " P is open

proof

let P be Subset of T; :: thesis: ( P is open implies g " P is open )
assume P is open ; :: thesis: g " P is open
then reconsider P = P as open Subset of T ;
for x being set holds
( x in g " P iff ex Q being Subset of Y st
( Q is open & Q c= g " P & x in Q ) )

proof

let x be set ; :: thesis: ( x in g " P iff ex Q being Subset of Y st
( Q is open & Q c= g " P & x in Q ) )
thus ( x in g " P implies ex Q being Subset of Y st
( Q is open & Q c= g " P & x in Q ) ) :: thesis: ( ex Q being Subset of Y st
( Q is open & Q c= g " P & x in Q ) implies x in g " P )

proof

assume A5: x in g " P ; :: thesis: ex Q being Subset of Y st
( Q is open & Q c= g " P & x in Q )
then reconsider y = x as Point of Y ;
A6: g . y in P by A5, FUNCT_2:46;
set A = { (inf (f .: (V /\ the carrier of X))) where V is open Subset of Y : y in V } ;
{ (inf (f .: (V /\ the carrier of X))) where V is open Subset of Y : y in V } c= the carrier of T

proof

let a be set ; :: according to TARSKI:def 3 :: thesis: ( not a in { (inf (f .: (V /\ the carrier of X))) where V is open Subset of Y : y in V } or a in the carrier of T )
assume a in { (inf (f .: (V /\ the carrier of X))) where V is open Subset of Y : y in V } ; :: thesis: a in the carrier of T
then ex V being open Subset of Y st
( a = inf (f .: (V /\ the carrier of X)) & y in V ) ;
hence a in the carrier of T ; :: thesis: verum

end;

then reconsider A = { (inf (f .: (V /\ the carrier of X))) where V is open Subset of Y : y in V } as Subset of T ;
A7: g . y = sup A by A3;
A8: inf (f .: (([#] Y) /\ the carrier of X)) in A ;
A is directed

proof

let a, b be Element of T; :: according to WAYBEL_0:def 1 :: thesis: ( not a in A or not b in A or ex b₁ being Element of the carrier of T st
( b₁ in A & a <= b₁ & b <= b₁ ) )
assume a in A ; :: thesis: ( not b in A or ex b₁ being Element of the carrier of T st
( b₁ in A & a <= b₁ & b <= b₁ ) )
then consider Va being open Subset of Y such that
A9: a = inf (f .: (Va /\ the carrier of X)) and
A10: y in Va ;
assume b in A ; :: thesis: ex b₁ being Element of the carrier of T st
( b₁ in A & a <= b₁ & b <= b₁ )
then consider Vb being open Subset of Y such that
A11: b = inf (f .: (Vb /\ the carrier of X)) and
A12: y in Vb ;
take inf (f .: ((Va /\ Vb) /\ the carrier of X)) ; :: thesis: ( inf (f .: ((Va /\ Vb) /\ the carrier of X)) in A & a <= inf (f .: ((Va /\ Vb) /\ the carrier of X)) & b <= inf (f .: ((Va /\ Vb) /\ the carrier of X)) )
A13: Va /\ Vb is open by TOPS_1:38;
y in Va /\ Vb by A10, A12, XBOOLE_0:def 4;
hence inf (f .: ((Va /\ Vb) /\ the carrier of X)) in A by A13; :: thesis: ( a <= inf (f .: ((Va /\ Vb) /\ the carrier of X)) & b <= inf (f .: ((Va /\ Vb) /\ the carrier of X)) )
( (Va /\ Vb) /\ the carrier of X c= Va /\ the carrier of X & (Va /\ Vb) /\ the carrier of X c= Vb /\ the carrier of X ) by XBOOLE_1:17, XBOOLE_1:26;
then ( f .: ((Va /\ Vb) /\ the carrier of X) c= f .: (Va /\ the carrier of X) & f .: ((Va /\ Vb) /\ the carrier of X) c= f .: (Vb /\ the carrier of X) ) by RELAT_1:156;
hence ( a <= inf (f .: ((Va /\ Vb) /\ the carrier of X)) & b <= inf (f .: ((Va /\ Vb) /\ the carrier of X)) ) by A9, A11, WAYBEL_7:3; :: thesis: verum

end;

then A meets P by A6, A7, A8, WAYBEL11:def 1;
then consider b being set such that
A14: b in A and
A15: b in P by XBOOLE_0:3;
consider B being open Subset of Y such that
A16: b = inf (f .: (B /\ the carrier of X)) and
A17: y in B by A14;
reconsider b = b as Element of T by A16;
take B ; :: thesis: ( B is open & B c= g " P & x in B )
thus B is open ; :: thesis: ( B c= g " P & x in B )
thus B c= g " P :: thesis: x in B

proof

let a be set ; :: according to TARSKI:def 3 :: thesis: ( not a in B or a in g " P )
assume A18: a in B ; :: thesis: a in g " P
then reconsider a = a as Point of Y ;
A19: g . a = H₁(a) by A3;
b in { (inf (f .: (V /\ the carrier of X))) where V is open Subset of Y : a in V } by A16, A18;
then b <= g . a by A19, YELLOW_2:24;
then g . a in P by A15, WAYBEL_0:def 20;
hence a in g " P by FUNCT_2:46; :: thesis: verum

end;

thus x in B by A17; :: thesis: verum

end;

thus ( ex Q being Subset of Y st
( Q is open & Q c= g " P & x in Q ) implies x in g " P ) ; :: thesis: verum

end;

hence g " P is open by TOPS_1:57; :: thesis: verum

end;

hence g is continuous by A4, TOPS_2:55; :: thesis: g | the carrier of X = f
set gX = g | the carrier of X;
A20: the carrier of X c= the carrier of Y by A2, BORSUK_1:35;
A21: dom (g | the carrier of X) = (dom g) /\ the carrier of X by RELAT_1:90
.= the carrier of Y /\ the carrier of X by FUNCT_2:def 1
.= the carrier of X by A2, BORSUK_1:35, XBOOLE_1:28 ;
A22: dom f = the carrier of X by FUNCT_2:def 1;
for a being set st a in the carrier of X holds
(g | the carrier of X) . a = f . a

proof

let a be set ; :: thesis: ( a in the carrier of X implies (g | the carrier of X) . a = f . a )
assume A23: a in the carrier of X ; :: thesis: (g | the carrier of X) . a = f . a
then reconsider x = a as Point of X ;
reconsider y = x as Point of Y by A20, A23;
set A = { (inf (f .: (V /\ the carrier of X))) where V is open Subset of Y : y in V } ;
{ (inf (f .: (V /\ the carrier of X))) where V is open Subset of Y : y in V } c= the carrier of T

proof

let a be set ; :: according to TARSKI:def 3 :: thesis: ( not a in { (inf (f .: (V /\ the carrier of X))) where V is open Subset of Y : y in V } or a in the carrier of T )
assume a in { (inf (f .: (V /\ the carrier of X))) where V is open Subset of Y : y in V } ; :: thesis: a in the carrier of T
then ex V being open Subset of Y st
( a = inf (f .: (V /\ the carrier of X)) & y in V ) ;
hence a in the carrier of T ; :: thesis: verum

end;

then reconsider A = { (inf (f .: (V /\ the carrier of X))) where V is open Subset of Y : y in V } as Subset of T ;
A24: f . x is_>=_than A

proof

let z be Element of T; :: according to LATTICE3:def 9 :: thesis: ( not z in A or z <= f . x )
assume z in A ; :: thesis: z <= f . x
then consider V being open Subset of Y such that
A25: z = inf (f .: (V /\ the carrier of X)) and
A26: y in V ;
A27: ex_inf_of f .: (V /\ the carrier of X),T by YELLOW_0:17;
y in V /\ the carrier of X by A26, XBOOLE_0:def 4;
hence z <= f . x by A25, A27, FUNCT_2:43, YELLOW_4:2; :: thesis: verum

end;

A28: for b being Element of T st b is_>=_than A holds
f . x <= b

proof

let b be Element of T; :: thesis: ( b is_>=_than A implies f . x <= b )
assume A29: for k being Element of T st k in A holds
k <= b ; :: according to LATTICE3:def 9 :: thesis: f . x <= b
A30: for V being open Subset of X st x in V holds
inf (f .: V) <= b

proof

let V be open Subset of X; :: thesis: ( x in V implies inf (f .: V) <= b )
assume A31: x in V ; :: thesis: inf (f .: V) <= b
V in the topology of X by PRE_TOPC:def 5;
then consider Q being Subset of Y such that
A32: Q in the topology of Y and
A33: V = Q /\ ([#] X) by A2, PRE_TOPC:def 9;
reconsider Q = Q as open Subset of Y by A32, PRE_TOPC:def 5;
y in Q by A31, A33, XBOOLE_0:def 4;
then inf (f .: (Q /\ the carrier of X)) in A ;
hence inf (f .: V) <= b by A29, A33; :: thesis: verum

end;

A34: b is_>=_than waybelow (f . x)

proof

let w be Element of T; :: according to LATTICE3:def 9 :: thesis: ( not w in waybelow (f . x) or w <= b )
assume w in waybelow (f . x) ; :: thesis: w <= b
then w << f . x by WAYBEL_3:7;
then f . x in wayabove w by WAYBEL_3:8;
then A35: x in f " (wayabove w) by FUNCT_2:46;
A36: [#] T <> {} ;
wayabove w is open by WAYBEL11:36;
then f " (wayabove w) is open by A1, A36, TOPS_2:55;
then A37: inf (f .: (f " (wayabove w))) <= b by A30, A35;
( ex_inf_of wayabove w,T & ex_inf_of f .: (f " (wayabove w)),T ) by YELLOW_0:17;
then A38: inf (wayabove w) <= inf (f .: (f " (wayabove w))) by FUNCT_1:145, YELLOW_0:35;
w <= inf (wayabove w) by WAYBEL14:9;
then w <= inf (f .: (f " (wayabove w))) by A38, ORDERS_2:26;
hence w <= b by A37, ORDERS_2:26; :: thesis: verum

end;

f . x = sup (waybelow (f . x)) by WAYBEL_3:def 5;
hence f . x <= b by A34, YELLOW_0:32; :: thesis: verum

end;

thus (g | the carrier of X) . a = g . y by FUNCT_1:72
.= H₁(y) by A3
.= f . a by A24, A28, YELLOW_0:30 ; :: thesis: verum

end;

hence g | the carrier of X = f by A21, A22, FUNCT_1:9; :: thesis: verum