|
continuous_lambda [ T : TYPE FROM real ] : THEORY
BEGIN
IMPORTING continuous_functions[T],
reals@min_max
f,g : VAR continuous_fun
pos_continuous?(f):bool = FORALL (x:T) : f(x) > 0
pos_continuous_fun : TYPE = (pos_continuous?)
nzf : VAR nz_continuous_fun
pf : VAR pos_continuous_fun
x : VAR T
k : VAR real
nzk : VAR nzreal
n : VAR nat
id_cont : LEMMA
continuous?(LAMBDA(x):x)
const_cont: LEMMA
continuous?(LAMBDA(x):k)
add_cont : LEMMA
continuous?(LAMBDA(x):f(x)+g(x))
sub_cont : LEMMA
continuous?(LAMBDA(x):f(x)-g(x))
neg_cont : LEMMA
continuous?(LAMBDA(x):-f(x))
mult_cont : LEMMA
continuous?(LAMBDA(x):f(x)*g(x))
div_cont : LEMMA
continuous?(LAMBDA(x):f(x)/nzf(x))
scal_mult_cont : LEMMA
continuous?(LAMBDA(x):k*f(x))
scal_div1_cont : LEMMA
continuous?(LAMBDA(x):f(x)/nzk)
scal_div2_cont : LEMMA
continuous?(LAMBDA(x):k/nzf(x))
pow_cont : LEMMA
continuous?(LAMBDA(x):f(x)^n)
sq_cont : LEMMA
continuous?(LAMBDA (x):sq(f(x)))
IMPORTING sqrt_derivative,
composition_continuous
sqrt_cont : LEMMA
continuous?(LAMBDA(x):sqrt(pf(x)))
abs_cont : LEMMA
continuous?(LAMBDA (x):abs(f(x)))
max_cont : LEMMA
continuous?(LAMBDA (x):max(f(x),g(x)))
min_cont : LEMMA
continuous?(LAMBDA (x):min(f(x),g(x)))
END continuous_lambda
¤ 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.
|
