Quellcode-Bibliothek
© Kompilation durch diese Firma
[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]
Datei:
sigma_countable.prf
Sprache: Lisp
|
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
[ Seitenstruktur0.0Drucken
etwas mehr zur Ethik
]
|
|
