|
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
expt_0 : LEMMA 0^i = 0
lt1_expt_le : LEMMA nnx < 1 => nnx^i <= nnx
sqrt_exists : LEMMA
EXISTS (x1: [nnx: nonneg_real -> {nny | nny*nny = nnx}]): TRUE
END sqrt_exists
¤ Dauer der Verarbeitung: 0.14 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.
|
