|
omega_v2[D:posreal,B:nnreal,T: {AB: posreal|AB>B}] : THEORY
BEGIN
IMPORTING omega_2D[D,B,T],
analysis@continuity_of_max_min,
analysis@metric_space_real_fun
s,v : VAR Vect2
% The Definition Of omega_v2
omega_v2(s)(v): real =
IF on_D?(s) AND B = 0 THEN s*v
ELSE omega_2D(s)(v) ENDIF
omega_v2_generic: LEMMA
NOT (on_D?(s) AND B = 0) IMPLIES
omega_v2(s)(v) = omega_2D(s)(v)
% Characterizes Conflict
omega_v2_conflict: LEMMA
omega_v2(s)(v) < 0 IFF conflict_2D?(s,v)
omega_v2_2D_eq_0: LEMMA omega_v2(s)(v) = 0
IMPLIES omega_2D(s)(v) = 0
omega_v2_critical_points: LEMMA
omega_v2(s)(v) = 0 IMPLIES horizontal_sep?(s) AND line_solution?(s,v) OR
circle_solution_2D?(s,v,T,Entry) OR
(B>0 AND circle_solution_2D?(s,v,B,Exit))
% Continuity
omega_v2_continuous: LEMMA
continuous?(omega_v2(s))
END omega_v2
¤ Dauer der Verarbeitung: 0.15 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.
|
