|
linear_functions[T: TYPE FROM real]: THEORY
BEGIN
ASSUMING %% ----- restrict T to single interval ------
connected_domain : ASSUMPTION
FORALL (x, y : T), (z : real) :
x <= z AND z <= y IMPLIES T_pred(z)
not_one_element : ASSUMPTION
FORALL (x : T) : EXISTS (y : T) : x /= y
ENDASSUMING
IMPORTING reals@real_fun_props
a,b,c,x,y: VAR T
m,k: VAR real
f,g: VAR [T -> real]
linear?(f): bool = (EXISTS m,k: f = (LAMBDA x: m*x + k))
linear_on?(f,a,b): bool =
(EXISTS m,k: (FORALL x: a <= x AND x <= b IMPLIES f(x) = m*x + k))
linear_add: LEMMA linear?(f) AND linear?(g) IMPLIES
linear?(f+g)
END linear_functions
¤ Dauer der Verarbeitung: 0.16 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.
|
