Least fixed point from a directed family of maps
ID: least-fixed-point-from-a-directed-family-of-maps
Let be order-preserving and inflationary on a directed-complete partial order. Define when every set containing and closed under and directed joins contains . This is a partial order refining . The order-preserving maps satisfying form a composition-closed family . The values are directed, since bounds and . Their least upper bound lies in every such closed set containing , so . Then gives , while inflationarity gives the reverse inequality. If and , the lower set is closed, proving . Thus is the least fixed point of above .
New to topics? Read the docs here!