summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
file |
latest |
revisions |
annotate |
diff |
comparison |
raw |
help

doc-src/Inductive/ind-defs.tex

changeset 6745 | 74e8f703f5f2 |

parent 6637 | 57abed64dc14 |

child 7829 | c2672c537894 |

equal
deleted
inserted
replaced

6744:9727e83f0578 | 6745:74e8f703f5f2 |
---|---|

217 \lfp(D,h) & = & h(\lfp(D,h)) \\ |
217 \lfp(D,h) & = & h(\lfp(D,h)) \\ |

218 \gfp(D,h) & = & h(\gfp(D,h)) |
218 \gfp(D,h) & = & h(\gfp(D,h)) |

219 \end{eqnarray*} |
219 \end{eqnarray*} |

220 These equations are instances of the Knaster-Tarski theorem, which states |
220 These equations are instances of the Knaster-Tarski theorem, which states |

221 that every monotonic function over a complete lattice has a |
221 that every monotonic function over a complete lattice has a |

222 fixedpoint~\cite{davey&priestley}. It is obvious from their definitions |
222 fixedpoint~\cite{davey-priestley}. It is obvious from their definitions |

223 that $\lfp$ must be the least fixedpoint, and $\gfp$ the greatest. |
223 that $\lfp$ must be the least fixedpoint, and $\gfp$ the greatest. |

224 |
224 |

225 This fixedpoint theory is simple. The Knaster-Tarski theorem is easy to |
225 This fixedpoint theory is simple. The Knaster-Tarski theorem is easy to |

226 prove. Showing monotonicity of~$h$ is trivial, in typical cases. We must |
226 prove. Showing monotonicity of~$h$ is trivial, in typical cases. We must |

227 also exhibit a bounding set~$D$ for~$h$. Frequently this is trivial, as when |
227 also exhibit a bounding set~$D$ for~$h$. Frequently this is trivial, as when |