|
intervals_real[T: TYPE FROM real]: THEORY
BEGIN
AUTO_REWRITE+ member
x,y: VAR T
S,S1,S2: VAR set[T]
r: VAR posreal
open_intv(a:T,b:{x:T|a<x})(x) : MACRO bool = a < x AND x < b
closed_intv(a:T,b:{x:T|a<=x})(x): MACRO bool = a <= x AND x <= b
open_interval(a:T,b:{x:T|a<x}): TYPE = (open_intv(a,b))
closed_interval(a:T,b:{x:T|a<=x}): TYPE = (closed_intv(a,b))
Open_interval(a,b:T): TYPE = {x: T | (a <= b IMPLIES (a < x AND x < b))
AND (b < a IMPLIES (b < x AND x < a))}
Closed_interval(a,b:T): TYPE = {x: T | (a <= b IMPLIES (a <= x AND x <= b))
AND (b < a IMPLIES (b <= x AND x <= a))}
above_intv(a:T)(x) : MACRO bool = x > a
below_intv(a:T)(x) : MACRO bool = x < a
a,b: VAR T
END intervals_real
¤ Dauer der Verarbeitung: 0.23 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.
|
