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 "finite" endpoint.
If ⌜(inl a) ∈ (ℝ + ℝ)⌝ then the interval is "closed" at that endpoint  (written [a,..
or ...,a] and if ⌜(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

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