[CST-2] T in C

[M.Y.W.Y. Becker]

--On 05 June 2001 23:29 +0100 Adam Martin <amsm2@cam.ac.uk> wrote:

> So, in that case... (with N = intersection, because Outlook won't let me
> type alt-139 for the intersection symbol....)
>
> With the minimum fixed point being the N{ S c S' | f(S) c S } why is the
> chain:
>
> f(0) c f(f(0)) c f(f(f(0))) ....
>

This hold only if the domain of f is finite,
say |P|=k and f:Pow(P)->Pow(P).

Let "c" mean subset (but not proper subset), "m" be the min. fixed point of 
f.

By monotonicity, f(0) c f^2(0) c ...
Clearly f(0) c m.
Also, f^n(0) c m => f^(n+1)(0) c m
by the pre-fixed point property of m.

So, by induction,
f(0) c f^2(0) c ... c m

Since P is finite, the chain cannot be strictly increasing, so for some p
f^p(0)=f^(p+1)(0). In particular,
f^(k)(0)=f^(k+1)(0), where k=|P|.
So f^(k)(0)=m. qed.

Mo