## Definition ## Given a [[strictly ordered type]] $A$ and a term $a:A$, a __lower bounded open interval__ $(a, \infty)$ is a dependent type defined as $$(a, \infty) \coloneqq \sum_{b:A} (a \lt b)$$ ## See also ## * [[strict order]] * [[open interval]] * [[upper bounded open interval]]