Showing changes from revision #3 to #4: Added | Removed | Changed
Given an ordered type AA and terms a:Aa:A and b:Ab:A a closed interval [a,b][a, b] is a dependent type defined as
order
open interval
unit interval
interval-complete Archimedean ordered field?interval-complete strict order
Revision on May 12, 2022 at 00:45:17 by Anonymous?. See the history of this page for a list of all contributions to it.