What this says at a high level; or what it implies given the above condition; is that the application of the monotone operator to the closure set \(\mu f\) doesn't shrink the set any further, in other words its operation stabilizes at this set such that each member in this set maps precisely to some other member in the set not more (i.e. outside as that would mean it's not closed) and not less (as that would imply it's not minimal).
\[
f(\mu f) \subseteq \mu f
\]
What this says at a high level; or what it implies given the above condition; is that the application of the monotone operator to the closure set \(\mu f\) doesn't shrink the set any further, in other words its operation stabilizes at this set such that each member in this set maps precisely to some other member in the set not more (i.e. outside as that would mean it's not closed) and not less (as that would imply it's not minimal). A question I had here was:
But why does this actually happen?
A nice perspective to have firstly is seeing the set \(\mu f\) here as a generating set for the function \(f\). In other words if we view the function \(f\) as a set of rules which generate new members in the set from existing members, then the closure \(\mu f\) represents the most precise set of members which can be generated by these rules without introducing any extraneous members.
The effect of this is that because the members in \(\mu f\) are precisely those which can be generated by the rules in \(f\), applying \(f\) to this set will simply regenerate the same members, hence why we have that \(\mu f \subseteq f(\mu f)\) since all the members in \(\mu f\) already correspond to members generated by the members of \(\mu f\) under the rules of \(f\)
Furthermore, since we are working in the context of a complete lattice, as we take the intersection of more and more closed subsets under \(f\) we eventually reach a point where if we take some further intersection (move down more) we end up losing the closed property, but if we move up (i.e. take the union of more closed sets) we end up introducing extraneous members which violate the minimalism property, hence the idea that we stabilize at this set i.e. we are a fixed point on the lattice under the operator.