Homotopy Type Theory irrational numbers > history (Rev #2, changes)

Skip the Navigation Links | Home Page | All Pages | Latest Revisions | Authors |

Showing changes from revision #1 to #2: Added | Removed | Changed

Definition

Let RR be an Archimedean ordered integral domain with the integers ℤ⊆R\mathbb{Z} \subseteq R being a integral subdomain of RR, with monic function f:ℤ→Rf:\mathbb{Z} \to R. The tight apartness relation r#sr # s in ℤ R \mathbb{Z} R and RR is defined as

r#s≔(r<s)×(s<r)r # s \coloneqq (r \lt s) \times (s \lt r)

and Let us define the non-zero dependent integers type are on defined asRR

ℤ #0isIrrational(r)≔ ∑ ∏ a:ℤ∏ b:ℤ(f(a)#0)×(f(a)⋅r#f(b)) \mathbb{Z}_{#0} isIrrational(r) \coloneqq \sum_{a:\mathbb{Z}} \prod_{a:\mathbb{Z}} a \prod_{b:\mathbb{Z}} (f(a) # 0 0) \times (f(a) \cdot r # f(b))

with monic function rri:ℤ #0→ℤi:\mathbb{Z}_{#0} \to \mathbb{Z} is irrational if the type .isIrrational(r)isIrrational(r) has a term.

Let The us define the dependent type on ofRRirrational numbers in RR is defined as:

Irrational(R)≔∑ r:RisIrrational(r)≔∏ a:ℤ #0∏ b:ℤf(i(a))⋅r#f(b) isIrrational(r) Irrational(R) \coloneqq \prod_{a:\mathbb{Z}_{#0}} \sum_{r:R} \prod_{b:\mathbb{Z}} isIrrational(r) {f(i(a)) \cdot r # f(b)}

rr is irrational if the type isIrrational(r)isIrrational(r) has a term.

The type of irrational numbers in RR is defined as:
Irrational(R)≔∑ r:RisIrrational(r)Irrational(R) \coloneqq \sum_{r:R} isIrrational(r)

See also

Revision on March 15, 2022 at 16:38:09 by Anonymous?. See the history of this page for a list of all contributions to it.

DiscussNext revision (3 more)Previous revision (1 more)Current version of pageHide changesHistory (4 revisions)Rollback Source