|
%------------------------------------------------------------------------------
% Continuous functions [T->real]
%
% Author: David Lester, Manchester University
%
% Version 1.0 15/09/08 Initial Version
%------------------------------------------------------------------------------
real_continuity[T:TYPE,(IMPORTING metric_def[T]) d:metric]: THEORY
BEGIN
IMPORTING
metric_continuity[T,d,real,(lambda (x,y:real): abs(x-y))],
topology@constant_continuity[T,metric_induced_topology[T,d],
real,metric_induced_topology[real,
(lambda (x,y:real) :abs(x-y))]],
reals@real_fun_ops_aux[T],
power@real_expt,
power@log,
power@real_fun_power[T]
g,g1,g2: VAR metric_continuous
n: VAR nat
u: VAR sequence[metric_continuous]
c: VAR real
a: VAR posreal
x: VAR T
h: VAR {g | FORALL x: g(x) >= 0}
%;
% ^(g,a): MACRO [T->real] = real_fun_power.^(g,a);
sum_continuous: JUDGEMENT +(g1,g2) HAS_TYPE metric_continuous
opp_continuous: JUDGEMENT -(g) HAS_TYPE metric_continuous
diff_continuous: JUDGEMENT -(g1,g2) HAS_TYPE metric_continuous
scal_continuous: JUDGEMENT *(c,g) HAS_TYPE metric_continuous
abs_continuous: JUDGEMENT abs(g) HAS_TYPE metric_continuous
expt_real_continuous: JUDGEMENT ^(h,a) HAS_TYPE metric_continuous
expt_nat_continuous: JUDGEMENT expt(g,n) HAS_TYPE metric_continuous
sq_continuous: JUDGEMENT sq(g) HAS_TYPE metric_continuous
min_continuous: JUDGEMENT min(g1,g2) HAS_TYPE metric_continuous
max_continuous: JUDGEMENT max(g1,g2) HAS_TYPE metric_continuous
minimum_continuous: JUDGEMENT minimum(u,n) HAS_TYPE metric_continuous
maximum_continuous: JUDGEMENT maximum(u,n) HAS_TYPE metric_continuous
plus_continuous: JUDGEMENT plus(g) HAS_TYPE metric_continuous
minus_continuous: JUDGEMENT minus(g) HAS_TYPE metric_continuous
prod_continuous: JUDGEMENT *(g1,g2) HAS_TYPE metric_continuous
END real_continuity
¤ Dauer der Verarbeitung: 0.0 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.
|
