doc-src/ZF/ZF.tex
 changeset 6745 74e8f703f5f2 parent 6592 c120262044b6 child 8249 3fc32155372c
equal inserted replaced
6744:9727e83f0578 6745:74e8f703f5f2
  1171 set (Fig.\ts\ref{zf-fixedpt}).  The theory defines least and greatest
  1171 set (Fig.\ts\ref{zf-fixedpt}).  The theory defines least and greatest
  1172 fixedpoint operators with corresponding induction and coinduction rules.
  1172 fixedpoint operators with corresponding induction and coinduction rules.
  1173 These are essential to many definitions that follow, including the natural
  1173 These are essential to many definitions that follow, including the natural
  1174 numbers and the transitive closure operator.  The (co)inductive definition
  1174 numbers and the transitive closure operator.  The (co)inductive definition
  1175 package also uses the fixedpoint operators~\cite{paulson-CADE}.  See
  1175 package also uses the fixedpoint operators~\cite{paulson-CADE}.  See
  1176 Davey and Priestley~\cite{davey&priestley} for more on the Knaster-Tarski
  1176 Davey and Priestley~\cite{davey-priestley} for more on the Knaster-Tarski
  1177 Theorem and my paper~\cite{paulson-set-II} for discussion of the Isabelle
  1177 Theorem and my paper~\cite{paulson-set-II} for discussion of the Isabelle
  1178 proofs.
  1178 proofs.
  1179
  1179
  1180 Monotonicity properties are proved for most of the set-forming operations:
  1180 Monotonicity properties are proved for most of the set-forming operations:
  1181 union, intersection, Cartesian product, image, domain, range, etc.  These
  1181 union, intersection, Cartesian product, image, domain, range, etc.  These