sqrt_exists: THEORY %-------------------------------------------------------------------------------- % % This theory provides a non-constructive proof of the existence of the % square root function. The proof has been adapted from Rosenlicht's % Introduction to Analysis. % %--------------------------------------------------------------------------------
BEGIN
e: VAR posreal
x, y: VAR real
nnx, nny: VAR nonneg_real
i: var posnat
epsilon_delta: LEMMA (FORALL e: abs(x - y) < e) => x = y
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.
