let L be complete Lattice; :: thesis: for f being monotone UnOp of L
for a being Element of L st a is_a_fixpoint_of f holds
( lfp f [= a & a [= gfp f )
let f be monotone UnOp of L; :: thesis: for a being Element of L st a is_a_fixpoint_of f holds
( lfp f [= a & a [= gfp f )
let a be Element of L; :: thesis: ( a is_a_fixpoint_of f implies ( lfp f [= a & a [= gfp f ) )
defpred S1[ Ordinal] means (f,$1) +. (Bottom L) [= a;
A1: now :: thesis: for O1 being Ordinal st O1 <> 0 & O1 is limit_ordinal & ( for O2 being Ordinal st O2 in O1 holds
S1[O2] ) holds
S1[O1]
deffunc H1( Ordinal) -> Element of L = (f,$1) +. (Bottom L);
let O1 be Ordinal; :: thesis: ( O1 <> 0 & O1 is limit_ordinal & ( for O2 being Ordinal st O2 in O1 holds
S1[O2] ) implies S1[O1] )
assume that
A2: ( O1 <> 0 & O1 is limit_ordinal ) and
A3: for O2 being Ordinal st O2 in O1 holds
S1[O2] ; :: thesis: S1[O1]
consider L1 being Sequence such that
A4: ( dom L1 = O1 & ( for O3 being Ordinal st O3 in O1 holds
L1 . O3 = H1(O3) ) ) from ORDINAL2:sch 2();
A5: rng L1 is_less_than a
proof
let q be Element of L; :: according to LATTICE3:def 17 :: thesis: ( not q in rng L1 or q [= a )
assume q in rng L1 ; :: thesis: q [= a
then consider C being object such that
A6: C in dom L1 and
A7: q = L1 . C by FUNCT_1:def 3;
reconsider C = C as Ordinal by A6;
(f,C) +. (Bottom L) [= a by A3, A4, A6;
hence q [= a by A4, A6, A7; :: thesis: verum
end;
(f,O1) +. (Bottom L) = "\/" ((rng L1),L) by A2, A4, Th17;
hence S1[O1] by A5, LATTICE3:def 21; :: thesis: verum
end;
assume a is_a_fixpoint_of f ; :: thesis: ( lfp f [= a & a [= gfp f )
then A8: f . a = a ;
A9: now :: thesis: for O1 being Ordinal st S1[O1] holds
S1[ succ O1]
let O1 be Ordinal; :: thesis: ( S1[O1] implies S1[ succ O1] )
assume S1[O1] ; :: thesis: S1[ succ O1]
then f . ((f,O1) +. (Bottom L)) [= f . a by QUANTAL1:def 12;
hence S1[ succ O1] by A8, Th15; :: thesis: verum
end;
(f,{}) +. (Bottom L) = Bottom L by Th13;
then A10: S1[ 0 ] by LATTICES:16;
for O2 being Ordinal holds S1[O2] from ORDINAL2:sch 1(A10, A9, A1);
 hence lfp f [= a ; :: thesis: a [= gfp f
defpred S2[ Ordinal] means a [= (f,$1) -. (Top L);
A11: now :: thesis: for O1 being Ordinal st S2[O1] holds
S2[ succ O1]
let O1 be Ordinal; :: thesis: ( S2[O1] implies S2[ succ O1] )
assume S2[O1] ; :: thesis: S2[ succ O1]
then f . a [= f . ((f,O1) -. (Top L)) by QUANTAL1:def 12;
hence S2[ succ O1] by A8, Th16; :: thesis: verum
end;
A12: now :: thesis: for O1 being Ordinal st O1 <> 0 & O1 is limit_ordinal & ( for O2 being Ordinal st O2 in O1 holds
S2[O2] ) holds
S2[O1]
deffunc H1( Ordinal) -> Element of L = (f,$1) -. (Top L);
let O1 be Ordinal; :: thesis: ( O1 <> 0 & O1 is limit_ordinal & ( for O2 being Ordinal st O2 in O1 holds
S2[O2] ) implies S2[O1] )
assume that
A13: ( O1 <> 0 & O1 is limit_ordinal ) and
A14: for O2 being Ordinal st O2 in O1 holds
S2[O2] ; :: thesis: S2[O1]
consider L1 being Sequence such that
A15: ( dom L1 = O1 & ( for O3 being Ordinal st O3 in O1 holds
L1 . O3 = H1(O3) ) ) from ORDINAL2:sch 2();
A16: a is_less_than rng L1
proof
let q be Element of L; :: according to LATTICE3:def 16 :: thesis: ( not q in rng L1 or a [= q )
assume q in rng L1 ; :: thesis: a [= q
then consider C being object such that
A17: C in dom L1 and
A18: q = L1 . C by FUNCT_1:def 3;
reconsider C = C as Ordinal by A17;
a [= (f,C) -. (Top L) by A14, A15, A17;
hence a [= q by A15, A17, A18; :: thesis: verum
end;
(f,O1) -. (Top L) = "/\" ((rng L1),L) by A13, A15, Th18;
hence S2[O1] by A16, LATTICE3:39; :: thesis: verum
end;
(f,{}) -. (Top L) = Top L by Th14;
then A19: S2[ 0 ] by LATTICES:19;
for O2 being Ordinal holds S2[O2] from ORDINAL2:sch 1(A19, A11, A12);
 hence a [= gfp f ; :: thesis: verum