|
deriv_domain_def[T : TYPE FROM real]: THEORY
BEGIN
deriv_domain?: bool = FORALL (e: posreal, x:T):
EXISTS (y: {u: nzreal | T_pred(u + x)}): abs(y) < e
not_one_element?: bool = (FORALL (x: T): EXISTS (y: T): x /= y)
connected?: bool = FORALL (x, y : T), (z : real): x <= z AND z <= y IMPLIES T_pred[T](z)
connected_deriv_domain: LEMMA connected? AND not_one_element?
IMPLIES deriv_domain?
del_neigh_all?: bool = FORALL (a: T): EXISTS (del: posreal): FORALL (xx:real):
abs(xx-a) < del IMPLIES T_pred[T](xx)
% The following lemma shows that our derivative domain is more general than just
% having a delta neighborhood around every point.
del_neigh_all_lem : LEMMA del_neigh_all? IMPLIES deriv_domain?
END deriv_domain_def
¤ Dauer der Verarbeitung: 0.16 Sekunden
(vorverarbeitet)
¤
|
Haftungshinweis
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.
|
