|
continuous_functions_aux[T : TYPE FROM real] : THEORY
BEGIN
f : VAR [T -> real]
x, x0 : VAR T
n: VAR nat
epsilon, delta: VAR posreal
IMPORTING analysis@continuous_functions[T],
analysis@convergence_ops
right_continuous?(f,x0): bool
= FORALL epsilon: EXISTS delta: FORALL x: x0 <= x AND x - x0 < delta
IMPLIES abs(f(x) - f(x0)) < epsilon
left_continuous?(f,x0): bool
= FORALL epsilon: EXISTS delta: FORALL x: x <= x0 AND x0 - x < delta
IMPLIES abs(f(x) - f(x0)) < epsilon
right_continuous?(f): bool = FORALL x0 : right_continuous?(f, x0)
left_continuous?(f): bool = FORALL x0 : left_continuous?(f, x0)
continuous_lr_def: LEMMA continuous?(f) IFF
right_continuous?(f) AND left_continuous?(f)
END continuous_functions_aux
¤ Dauer der Verarbeitung: 0.18 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.
|
