Showing changes from revision #0 to #1: Added | Removed | Changed
Given a decidable strictly ordered set AA and terms a:Aa:A and b:Ab:A, an element c:Ac:A is strictly between aa and bb if (a<c)=1(a \lt c) = 1 and (c<b)=1(c \lt b) = 1 and a decidable open interval (a,b)(a, b) is a dependent type defined as
decidable strict order
decidable closed interval?
decidable lower bounded open interval?
decidable upper bounded open interval?
Revision on April 28, 2022 at 20:11:37 by Anonymous?. See the history of this page for a list of all contributions to it.