Nuprl Definition : interval
An interval has two endpoint. There are three kinds of endpoints
that we represent with the type ⌜ℝ + ℝ + Top⌝.
An endpoint ⌜inr anything ⌝ represents "infinity"
(positive or negative, depending on whether it is the right or left endpoint).
An endpoint of the form ⌜inl x⌝ where ⌜x ∈ ℝ + ℝ⌝ is a "finite" endpoint.
If ⌜x = (inl a) ∈ (ℝ + ℝ)⌝ then the interval is "closed" at that endpoint (written [a,..
or ...,a] ) and if ⌜x = (inl a) ∈ (ℝ + ℝ)⌝ then the interval is "open" at
that endpoint (written (a,... or ...,a) ).
Therefore, the type ℝ + ℝ + Top × (ℝ + ℝ + Top)
represents nine kinds of intervals:
[a,b] (a,b], (-infinity, b]
[a,b), (a,b), (-infintiy, b)
[a, infinity), (a,infinity), (-infinity, infinity).⋅
Interval == ℝ + ℝ + Top × (ℝ + ℝ + Top)
Definitions occuring in Statement :
real: ℝ,
top: Top,
product: x:A × B[x],
union: left + right
Definitions occuring in definition :
product: x:A × B[x],
union: left + right,
real: ℝ,
top: Top
FDL editor aliases :
interval
interval
Latex:
Interval == \mBbbR{} + \mBbbR{} + Top \mtimes{} (\mBbbR{} + \mBbbR{} + Top)
Date html generated:
2016_11_08-AM-09_06_56
Last ObjectModification:
2016_11_07-PM-00_20_19
Theory : reals
Home
Index