|
cont_if_fun[ T : TYPE FROM real] : THEORY
%------------------------------------------------------------------------------------
%
% Continuity of a function defined using an IF-THEN-ELSE
%
% G = IF <expr> THEN f1 ELSE f2 ENDIF
%
% is continuous if f1 and f2 are continuous and they are equal at all of the
% place where the <expr> is discontinuous.
%
% Author: Rick Butler NASA Langley
% Jan 22, 2009
%--------------------------------------------------------------------------------------
BEGIN
ASSUMING
connected_domain : ASSUMPTION
FORALL (x, y : T), (z : real) :
x <= z AND z <= y IMPLIES T_pred(z)
ENDASSUMING
IMPORTING continuous_functions[T]
f,f1,f2 : VAR [T -> real]
P : VAR [T -> bool]
a, b, c, d, x : VAR T
discont_pts(P): set[T] = {x:T | NOT continuous_at?(P,x)}
discont_pts_lem: LEMMA NOT discont_pts(P)(a) IMPLIES
EXISTS (delta: posreal):
(FORALL (x:T): abs(x-a) < delta IMPLIES P(x) = true) OR
(FORALL (x:T): abs(x-a) < delta IMPLIES P(x) = false)
if_fun(P: [T-> bool], f1:[T -> real], f2:[T -> real]): [T -> real] =
(LAMBDA (x:T): IF P(x) THEN f1(x) ELSE f2(x) ENDIF)
if_fun_cont: LEMMA continuous?(f1) AND continuous?(f2) AND
(FORALL (x:T): discont_pts(P)(x) IMPLIES f1(x) = f2(x))
IMPLIES
continuous?(if_fun(P,f1,f2))
discont_pts_simple: LEMMA continuous?(f1) AND continuous?(f2) AND
P = (LAMBDA (t: T): f1(t) > 0 AND f2(t) > 0) AND
discont_pts(P)(x)
IMPLIES f1(x) = 0 OR f2(x) = 0
prod_fun_lem: LEMMA continuous?(f1) AND continuous?(f2) AND
P = (LAMBDA (t: T): f1(t) > 0 AND f2(t) > 0) AND
discont_pts(P)(x)
IMPLIES
f1(x)*f2(x) = -abs(f1(x)*f2(x))
END cont_if_fun
¤ 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.
|
