Commit ef669d81 by Ralf Jung

### docs: fix COFE limit axiom

parent 0a1c37a3
 ... @@ -15,7 +15,7 @@ This definition varies slightly from the original one in~\cite{catlogic}. ... @@ -15,7 +15,7 @@ This definition varies slightly from the original one in~\cite{catlogic}. \All n. (\nequiv{n}) ~& \text{is an equivalence relation} \tagH{cofe-equiv} \\ \All n. (\nequiv{n}) ~& \text{is an equivalence relation} \tagH{cofe-equiv} \\ \All n, m.& n \geq m \Ra (\nequiv{n}) \subseteq (\nequiv{m}) \tagH{cofe-mono} \\ \All n, m.& n \geq m \Ra (\nequiv{n}) \subseteq (\nequiv{m}) \tagH{cofe-mono} \\ \All x, y.& x = y \Lra (\All n. x \nequiv{n} y) \tagH{cofe-limit} \\ \All x, y.& x = y \Lra (\All n. x \nequiv{n} y) \tagH{cofe-limit} \\ \All n, c.& \lim(c) \nequiv{n} c(n+1) \tagH{cofe-compl} \All n, c.& \lim(c) \nequiv{n} c(n) \tagH{cofe-compl} \end{align*} \end{align*} \end{defn} \end{defn} ... ...
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!