Version 1 (modified by onnopaap, 14 years ago) |
---|
Base Template LowerUpperOfNumberRange
LowerUpperOfNumberRange is a template for stating what the upper and lower bounds of a number range are.
LowerUpperOfNumberRange(a, b, c) means that a is a number range and b and c are numbers,
and that b is the lower, c the upper bound of a.
Roles:
1 hasRange NumberRange
2 hasLowerBound ArithmeticNumber
3 hasUpperBound ArithmeticNumber
Axiom:
LowerUpperOfNumberRange(x1, x2, x3) <-> NumberRange(x1) & ArithmeticNumber(x2) & ArithmeticNumber(x3) & LowerBoundOfNumberRangeTemplate(x2, x1) & UpperBoundOfNumberRangeTemplate(x3, x1) .
NOTE To represent number ranges which are not bounded, use the reference items Infinity and -Infinity (see 8.2.1).