let O1 be Ordinal; for L being complete Lattice
for f being monotone UnOp of L
for a being Element of L st f . a [= a & (f,O1) -. a is_a_fixpoint_of f holds
for O2 being Ordinal st O1 c= O2 holds
(f,O1) -. a = (f,O2) -. a
let L be complete Lattice; for f being monotone UnOp of L
for a being Element of L st f . a [= a & (f,O1) -. a is_a_fixpoint_of f holds
for O2 being Ordinal st O1 c= O2 holds
(f,O1) -. a = (f,O2) -. a
let f be monotone UnOp of L; for a being Element of L st f . a [= a & (f,O1) -. a is_a_fixpoint_of f holds
for O2 being Ordinal st O1 c= O2 holds
(f,O1) -. a = (f,O2) -. a
let a be Element of L; ( f . a [= a & (f,O1) -. a is_a_fixpoint_of f implies for O2 being Ordinal st O1 c= O2 holds
(f,O1) -. a = (f,O2) -. a )
assume that
A1:
f . a [= a
and
A2:
(f,O1) -. a is_a_fixpoint_of f
; for O2 being Ordinal st O1 c= O2 holds
(f,O1) -. a = (f,O2) -. a
set fa = (f,O1) -. a;
defpred S1[ Ordinal] means ( O1 c= $1 implies (f,O1) -. a = (f,$1) -. a );
A3:
now for O2 being Ordinal st O2 <> 0 & O2 is limit_ordinal & ( for O3 being Ordinal st O3 in O2 holds
S1[O3] ) holds
S1[O2]let O2 be
Ordinal;
( O2 <> 0 & O2 is limit_ordinal & ( for O3 being Ordinal st O3 in O2 holds
S1[O3] ) implies S1[O2] )assume that A4:
(
O2 <> 0 &
O2 is
limit_ordinal )
and A5:
for
O3 being
Ordinal st
O3 in O2 holds
S1[
O3]
;
S1[O2]thus
S1[
O2]
verumproof
assume
O1 c= O2
;
(f,O1) -. a = (f,O2) -. a
then A6:
(
f,
O2)
-. a [= (
f,
O1)
-. a
by A1, Th25;
deffunc H1(
Ordinal)
-> Element of
L = (
f,$1)
-. a;
consider L1 being
Sequence such that A7:
(
dom L1 = O2 & ( for
O3 being
Ordinal st
O3 in O2 holds
L1 . O3 = H1(
O3) ) )
from ORDINAL2:sch 2();
A8:
(
f,
O1)
-. a is_less_than rng L1
(
f,
O2)
-. a = "/\" (
(rng L1),
L)
by A4, A7, Th18;
then
(
f,
O1)
-. a [= (
f,
O2)
-. a
by A8, LATTICE3:39;
hence
(
f,
O1)
-. a = (
f,
O2)
-. a
by A6, LATTICES:8;
verum
end; end;
A11:
now for O2 being Ordinal st S1[O2] holds
S1[ succ O2]let O2 be
Ordinal;
( S1[O2] implies S1[ succ O2] )assume A12:
S1[
O2]
;
S1[ succ O2]thus
S1[
succ O2]
verum end;
A14:
S1[ 0 ]
;
thus
for O2 being Ordinal holds S1[O2]
from ORDINAL2:sch 1(A14, A11, A3); verum