|
%------------------------------------------------------------------------------------------------
%
% A Special Result On Continuous Functions R x R^3 -> R
%
% Author: Anthony Narkawicz, NASA Langley
%
%
% Version 1.0 September 16, 2009
%
%------------------------------------------------------------------------------------------------
vect3_Heine: THEORY
BEGIN
IMPORTING vect3_metric_space,
analysis@real_metric_space,
analysis@cross_metric_real_fun[real,real_dist,Vect3,dist],
analysis@continuity_ms[Vect3,dist,real,real_dist]
f: VAR [[real,Vect3] -> real]
curried_min_exists_3D: LEMMA FORALL (A: real, B: {x: real | A < x}):
continuous?(f,fullset[[(closed_intv(A,B)),Vect3]])
IMPLIES (FORALL (y: Vect3):
nonempty?[real]({r: real | EXISTS (t: (LAMBDA (x: real): A <= x AND x <= B)):r = f(t, y)})
AND below_bounded[real]({r: real | EXISTS (t: (LAMBDA (x: real): A <= x AND x <= B)):r = f(t, y)})
AND ext[real]({r: real | EXISTS (t: (LAMBDA (x: real): A <= x AND x <= B)): r = f(t, y)})
(inf[real]({r: real | EXISTS (t: (LAMBDA (x: real): A <= x AND x <= B)): r = f(t, y)}))
AND (EXISTS (tmin: (closed_intv(A,B))): FORALL (s: (closed_intv(A,B))): f(tmin,y) <= f(s,y)))
curried_min_is_cont_3D: THEOREM FORALL (A: real, B: {x: real | A < x}):
continuous?(f,fullset[[(closed_intv(A,B)),Vect3]])
IMPLIES
LET unif_min_first(y: Vect3): real
= min({r: real | EXISTS (t: (closed_intv(A,B))): r = f(t,y)})
IN continuous?(unif_min_first)
curried_min_is_cont_3D_ed: THEOREM FORALL (A: real, B: {x: real | A < x}):
(FORALL (x: (closed_intv(A,B)), y: Vect3, epsilon: posreal):
EXISTS (delta: posreal):
FORALL (z: (closed_intv(A,B)), w: Vect3):
(real_dist(x,z) <= delta AND dist(y,w) <= delta) IMPLIES real_dist(f(x,y),f(z,w))<epsilon)
IMPLIES
LET unif_min_first(y: Vect3): real
= min({r: real | EXISTS (t: (closed_intv(A,B))): r = f(t,y)})
IN
(FORALL (y: Vect3): FORALL (epsilon: posreal):
EXISTS (delta: posreal): FORALL (q:Vect3):
dist(y,q) < delta IMPLIES real_dist(unif_min_first(y),unif_min_first(q)) < epsilon)
% Uniform Continuity In The First Variable
multiary_Heine_3D: THEOREM FORALL (A: real, B: {x: real | A < x}):
continuous?(f,fullset[[(closed_intv(A,B)),Vect3]])
IMPLIES uniformly_continuous_in_first?(f,closed_intv(A,B),fullset[Vect3])
multiary_Heine_3D_ed: THEOREM FORALL (A: real, B: {x: real | A < x}):
(FORALL (x: (closed_intv(A,B)), y: Vect3, epsilon: posreal):
EXISTS (delta: posreal):
FORALL (z: (closed_intv(A,B)), w: Vect3): (real_dist(x,z) <= delta AND dist(y,w) <= delta)
IMPLIES real_dist(f(x,y),f(z,w))<epsilon)
IMPLIES
FORALL (y1: Vect3, epsilon: posreal): EXISTS (delta: posreal):
FORALL (x1,x2: (closed_intv(A,B)), y2: Vect3): (real_dist(x1,x2) <= delta AND dist(y1,y2) <= delta)
IMPLIES real_dist(f(x1,y1),f(x2,y2))<epsilon
END vect3_Heine
¤ Dauer der Verarbeitung: 0.1 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.
|
