deriv_domains: THEORY %----------------------------------------------------------------------------------------- % % The derivatives library has been generalized to handle a larger class of domains. % Previously the domain had to be a connected domain defined by the following % predicate: % % connected_domain : ASSUMPTION % FORALL (x, y : T), (z : real) : % x <= z AND z <= y IMPLIES T_pred(z) % % The following more general domain definition is now used % % deriv_domain : ASSUMPTION FORALL (e: posreal, x:T): % EXISTS (y: {u: nzreal | T_pred(u + x)}): abs(y) < e % % This definition allows unions of closed and open intervals % %----------------------------------------------------------------------------------------- BEGIN
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
