|
real_fun_props [T : TYPE FROM real] : THEORY
%----------------------------------------------------------------------%
% Defines several properties of functions [T -> real] %
% -> increasing/decreasing functions %
% -> upper/lower bound %
% -> maximum/minimum of a function %
%----------------------------------------------------------------------%
BEGIN
IMPORTING real_fun_ops, real_fun_preds
f : VAR [T -> real]
x, y : VAR T
a, z : VAR real
%-------------------
% Easy properties
%-------------------
strict_incr_to_incr : LEMMA strict_increasing?(f) IMPLIES increasing?(f)
strict_decr_to_decr : LEMMA strict_decreasing?(f) IMPLIES decreasing?(f)
incr_neg : LEMMA increasing?(- f) IFF decreasing?(f)
decr_neg : LEMMA decreasing?(- f) IFF increasing?(f)
strict_incr_neg: LEMMA strict_increasing?(- f) IFF strict_decreasing?(f)
strict_decr_neg: LEMMA strict_decreasing?(- f) IFF strict_increasing?(f)
%-----------------------
% Constant functions
%-----------------------
constant_to_incr : LEMMA constant?(f) IMPLIES increasing?(f)
constant_to_decr : LEMMA constant?(f) IMPLIES decreasing?(f)
constant_neg : LEMMA constant?(- f) IFF constant?(f)
%------------------------
% Relation to negative function
%------------------------
bounded_above_neg : LEMMA bounded_above?(- f) IFF bounded_below?(f)
bounded_below_neg : LEMMA bounded_below?(- f) IFF bounded_above?(f)
%------------------------
% Relation with bounds
%------------------------
max_bounded : LEMMA is_maximum?(x, f) IMPLIES bounded_above?(f)
min_bounded : LEMMA is_minimum?(x, f) IMPLIES bounded_below?(f)
%----------------------------------
% Relation with negative functions
%----------------------------------
max_neg : LEMMA is_maximum?(x, - f) IFF is_minimum?(x, f)
min_neg : LEMMA is_minimum?(x, - f) IFF is_maximum?(x, f)
%--------------------------------------------------------
% Image of a function
% redefined from function_image to avoid conversions
%--------------------------------------------------------
E: VAR setof[real]
Im(f) : setof[real] = { z | EXISTS x : z = f(x) }
Im(f, E) : setof[real] = { z | EXISTS x : E(x) AND z = f(x) }
END real_fun_props
¤ Dauer der Verarbeitung: 0.13 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.
|
