I was learning fixed points in the context of programming languages and the text wants on page 89 wants to show that $fix(\mathcal F)$ is a fix point by applying $\mathcal F$ to the fix point itself. Why is that?
Right now we define the fix point as the least upper bound (LUB) of a the chain $ \bot \leq \mathcal F( \bot) \leq \mathcal F^2( \bot) \leq ...$ bottomed complete partial order (BCPO). How does apply the (continuous) function to the fix point show its a LUB of the chain in question?
I would have thought the fixed point was obvious a fixed point by definition but it seems we actually have to manipulate it to show this...
Note that in wikipedia and other sources fixed points are defined as points that continuous application of a rule leads to the same element. I assume that should be a consequence of the LUB definition we gave above but thats NOT how we show fixed points YET.
I understand the steps of the proof just not the rationale of the first step, why are we applying $\mathcal F$?
