|
%------------------------------------------------------------------------------
% Properties of real intervals
%
% Author: David Lester, Manchester University
%
% Version 1.0 26/2/10 Initial Version
%------------------------------------------------------------------------------
real_intervals_aux: THEORY
BEGIN
IMPORTING metric_space@real_topology,
reals@bounded_reals
X,A: VAR set[real]
b: VAR bounded_interval
u: VAR unbounded_interval
n: VAR nat
r: VAR posreal
nnr: VAR nnreal
a,x: VAR real
closed_interval?(A):bool = interval?(A) and metric_closed?(A)
open_interval?(A):bool = interval?(A) and metric_open?(A)
bounded_open_interval_def: LEMMA bounded_open_interval?(A) <=>
empty?(A) OR EXISTS x,r: A = ball(x,r)
unbounded_open_interval_def: LEMMA
(unbounded?(A) AND open_interval?(A)) <=>
(A = fullset[real] OR
(EXISTS a: A = open_inf(a)) OR
(EXISTS a: A = inf_open(a)))
length(b):nnreal = IF empty?[real](b) THEN 0 ELSE sup(b)-inf(b) ENDIF % 2.1.1
length_closed: LEMMA nonempty?[real](b) =>
length(b) = length({x | inf(b) <= x AND x <= sup(b)})
length_open: LEMMA nonempty?[real](b) =>
length(b) = length({x | inf(b) < x AND x < sup(b)})
length_empty_rew: LEMMA length(emptyset[real]) = 0
length_closed_rew: LEMMA FORALL (b:{x|a<=x}):
length({x | a <= x AND x <= b}) = b-a
length_open_rew: LEMMA FORALL (b:{x|a<=x}):
length({x | a < x AND x < b}) = b-a
left_closed_right_open_interval?(A):bool
= nonempty?(A) AND
interval?(A) AND
(above_bounded(A) => NOT A(sup(A))) AND
(below_bounded(A) => A(inf(A)))
left_closed_right_open_interval: TYPE+ = (left_closed_right_open_interval?)
CONTAINING fullset[real]
nonempty_interval?(A):bool = nonempty?(A) AND interval?(A)
nonempty_interval: TYPE+ = (nonempty_interval?) CONTAINING fullset[real]
END real_intervals_aux
¤ 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.
|
