let Q be Quantale; for j being UnOp of Q st j is monotone & j is idempotent & j is \/-distributive holds
ex L being complete Lattice st
( the carrier of L = rng j & ( for X being Subset of L holds "\/" X = j . ("\/" (X,Q)) ) )
let j be UnOp of Q; ( j is monotone & j is idempotent & j is \/-distributive implies ex L being complete Lattice st
( the carrier of L = rng j & ( for X being Subset of L holds "\/" X = j . ("\/" (X,Q)) ) ) )
assume A1:
( j is monotone & j is idempotent & j is \/-distributive )
; ex L being complete Lattice st
( the carrier of L = rng j & ( for X being Subset of L holds "\/" X = j . ("\/" (X,Q)) ) )
reconsider D = rng j as non empty Subset of Q ;
dom j = H1(Q)
by FUNCT_2:def 1;
then reconsider j9 = j as Function of H1(Q),D by RELSET_1:4;
deffunc H5( Subset of D) -> Element of D = j9 . ("\/" ($1,Q));
consider f being Function of (bool D),D such that
A2:
for X being Subset of D holds f . X = H5(X)
from FUNCT_2:sch 4();
A3:
dom f = bool D
by FUNCT_2:def 1;
A4:
for X being Subset-Family of D holds f . (f .: X) = f . (union X)
proof
let X be
Subset-Family of
D;
f . (f .: X) = f . (union X)
set A =
{ (j . a) where a is Element of Q : a in f .: X } ;
set B =
{ (j . b) where b is Element of Q : b in union X } ;
reconsider Y =
f .: X,
X9 =
union X as
Subset of
Q by XBOOLE_1:1;
now for a being Element of Q st a in { (j . b) where b is Element of Q : b in union X } holds
ex b being Element of the carrier of Q st
( a [= b & b in { (j . a) where a is Element of Q : a in f .: X } )let a be
Element of
Q;
( a in { (j . b) where b is Element of Q : b in union X } implies ex b being Element of the carrier of Q st
( a [= b & b in { (j . a) where a is Element of Q : a in f .: X } ) )assume
a in { (j . b) where b is Element of Q : b in union X }
;
ex b being Element of the carrier of Q st
( a [= b & b in { (j . a) where a is Element of Q : a in f .: X } )then consider b9 being
Element of
Q such that A5:
a = j . b9
and A6:
b9 in union X
;
consider Y being
set such that A7:
b9 in Y
and A8:
Y in X
by A6, TARSKI:def 4;
reconsider Y =
Y as
Subset of
D by A8;
A9:
b9 [= "\/" (
Y,
Q)
by A7, LATTICE3:38;
take b =
j . ("\/" (Y,Q));
( a [= b & b in { (j . a) where a is Element of Q : a in f .: X } )
b = f . Y
by A2;
then A10:
b in f .: X
by A3, A8, FUNCT_1:def 6;
j . b = b
by A1, Lm1;
hence
(
a [= b &
b in { (j . a) where a is Element of Q : a in f .: X } )
by A1, A5, A10, A9;
verum end;
then A11:
"\/" (
{ (j . b) where b is Element of Q : b in union X } ,
Q)
[= "\/" (
{ (j . a) where a is Element of Q : a in f .: X } ,
Q)
by LATTICE3:47;
{ (j . a) where a is Element of Q : a in f .: X } is_less_than "\/" (
{ (j . b) where b is Element of Q : b in union X } ,
Q)
proof
let a be
Element of
Q;
LATTICE3:def 17 ( not a in { (j . a) where a is Element of Q : a in f .: X } or a [= "\/" ( { (j . b) where b is Element of Q : b in union X } ,Q) )
assume
a in { (j . a) where a is Element of Q : a in f .: X }
;
a [= "\/" ( { (j . b) where b is Element of Q : b in union X } ,Q)
then consider a9 being
Element of
Q such that A12:
a = j . a9
and A13:
a9 in f .: X
;
consider x being
object such that A14:
x in dom f
and A15:
x in X
and A16:
a9 = f . x
by A13, FUNCT_1:def 6;
reconsider x =
x as
Subset of
D by A14;
reconsider Y =
x as
Subset of
Q by XBOOLE_1:1;
A17:
{ (j . b) where b is Element of Q : b in Y } c= { (j . b) where b is Element of Q : b in union X }
a9 = j . ("\/" Y)
by A2, A16;
then
a9 = "\/" (
{ (j . b) where b is Element of Q : b in Y } ,
Q)
by A1, Th10;
then
a9 [= "\/" (
{ (j . b) where b is Element of Q : b in union X } ,
Q)
by A17, LATTICE3:45;
then
a [= j . ("\/" ( { (j . b) where b is Element of Q : b in union X } ,Q))
by A1, A12;
then
a [= j . (j . ("\/" X9))
by A1, Th10;
then
a [= j . ("\/" X9)
by A1, Lm1;
hence
a [= "\/" (
{ (j . b) where b is Element of Q : b in union X } ,
Q)
by A1, Th10;
verum
end;
then A20:
"\/" (
{ (j . a) where a is Element of Q : a in f .: X } ,
Q)
[= "\/" (
{ (j . b) where b is Element of Q : b in union X } ,
Q)
by LATTICE3:def 21;
thus f . (f .: X) =
j . ("\/" Y)
by A2
.=
"\/" (
{ (j . a) where a is Element of Q : a in f .: X } ,
Q)
by A1, Th10
.=
"\/" (
{ (j . b) where b is Element of Q : b in union X } ,
Q)
by A20, A11, LATTICES:8
.=
j . ("\/" X9)
by A1, Th10
.=
f . (union X)
by A2
;
verum
end;
for a being Element of D holds f . {a} = a
then consider L being strict complete Lattice such that
A23:
H1(L) = D
and
A24:
for X being Subset of L holds "\/" X = f . X
by A4, LATTICE3:55;
take
L
; ( the carrier of L = rng j & ( for X being Subset of L holds "\/" X = j . ("\/" (X,Q)) ) )
thus
H1(L) = rng j
by A23; for X being Subset of L holds "\/" X = j . ("\/" (X,Q))
let X be Subset of L; "\/" X = j . ("\/" (X,Q))
thus "\/" X =
f . X
by A24
.=
j . ("\/" (X,Q))
by A2, A23
; verum