let L be complete Lattice; :: thesis: for f being monotone UnOp of L ex a being Element of L st a is_a_fixpoint_of f
let f be monotone UnOp of L; :: thesis: ex a being Element of L st a is_a_fixpoint_of f
set H = { h where h is Element of L : h [= f . h } ;
set fH = { (f . h) where h is Element of L : h [= f . h } ;
set uH = "\/" ( { h where h is Element of L : h [= f . h } ,L);
set fuH = "\/" ( { (f . h) where h is Element of L : h [= f . h } ,L);
take "\/" ( { h where h is Element of L : h [= f . h } ,L) ; :: thesis: "\/" ( { h where h is Element of L : h [= f . h } ,L) is_a_fixpoint_of f
now :: thesis: for fh being Element of L st fh in { (f . h) where h is Element of L : h [= f . h } holds
fh [= f . ("\/" ( { h where h is Element of L : h [= f . h } ,L))
let fh be Element of L; :: thesis: ( fh in { (f . h) where h is Element of L : h [= f . h } implies fh [= f . ("\/" ( { h where h is Element of L : h [= f . h } ,L)) )
assume fh in { (f . h) where h is Element of L : h [= f . h } ; :: thesis: fh [= f . ("\/" ( { h where h is Element of L : h [= f . h } ,L))
then consider h being Element of L such that
A1: fh = f . h and
A2: h [= f . h ;
h in { h where h is Element of L : h [= f . h } by A2;
then h [= "\/" ( { h where h is Element of L : h [= f . h } ,L) by LATTICE3:38;
hence fh [= f . ("\/" ( { h where h is Element of L : h [= f . h } ,L)) by A1, QUANTAL1:def 12; :: thesis: verum
end;
then { (f . h) where h is Element of L : h [= f . h } is_less_than f . ("\/" ( { h where h is Element of L : h [= f . h } ,L)) ;
then A3: "\/" ( { (f . h) where h is Element of L : h [= f . h } ,L) [= f . ("\/" ( { h where h is Element of L : h [= f . h } ,L)) by LATTICE3:def 21;
now :: thesis: for a being Element of L st a in { h where h is Element of L : h [= f . h } holds
ex fh being Element of L st
( a [= fh & fh in { (f . h) where h is Element of L : h [= f . h } )
let a be Element of L; :: thesis: ( a in { h where h is Element of L : h [= f . h } implies ex fh being Element of L st
( a [= fh & fh in { (f . h) where h is Element of L : h [= f . h } ) )
assume a in { h where h is Element of L : h [= f . h } ; :: thesis: ex fh being Element of L st
( a [= fh & fh in { (f . h) where h is Element of L : h [= f . h } )
then consider h being Element of L such that
A4: ( a = h & h [= f . h ) ;
reconsider fh = f . h as Element of L ;
take fh = fh; :: thesis: ( a [= fh & fh in { (f . h) where h is Element of L : h [= f . h } )
thus ( a [= fh & fh in { (f . h) where h is Element of L : h [= f . h } ) by A4; :: thesis: verum
end;
then "\/" ( { h where h is Element of L : h [= f . h } ,L) [= "\/" ( { (f . h) where h is Element of L : h [= f . h } ,L) by LATTICE3:47;
then A5: "\/" ( { h where h is Element of L : h [= f . h } ,L) [= f . ("\/" ( { h where h is Element of L : h [= f . h } ,L)) by A3, LATTICES:7;
then f . ("\/" ( { h where h is Element of L : h [= f . h } ,L)) [= f . (f . ("\/" ( { h where h is Element of L : h [= f . h } ,L))) by QUANTAL1:def 12;
then f . ("\/" ( { h where h is Element of L : h [= f . h } ,L)) in { h where h is Element of L : h [= f . h } ;
then f . ("\/" ( { h where h is Element of L : h [= f . h } ,L)) [= "\/" ( { h where h is Element of L : h [= f . h } ,L) by LATTICE3:38;
hence "\/" ( { h where h is Element of L : h [= f . h } ,L) = f . ("\/" ( { h where h is Element of L : h [= f . h } ,L)) by A5, LATTICES:8; :: according to ABIAN:def 4 :: thesis: verum