Homotopy Type Theory irrational numbers > history (changes)

Showing changes from revision #4 to #5: Added | Removed | Changed

Contents

< irrational numbers

Whenever editing is allowed on the nLab again, this article should be ported over there.

Definition

In set theory

Let RR be an Archimedean ordered integral domain with the integers R\mathbb{Z} \subseteq R being a integral subdomain of RR, with injection fR f \in R^\mathbb{Z}. The tight apartness relation r#sr # s in RR is defined as

r#s(r<s)(s<r)r # s \coloneqq (r \lt s) \vee (s \lt r)

An element rRr \in R is irrational if

isIrrational(r)a.b.(f(a)#0)(f(a)r#f(b))isIrrational(r) \coloneqq \forall a \in \mathbb{Z}. \forall b \in \mathbb{Z}. (f(a) # 0) \wedge (f(a) \cdot r # f(b))

The set of irrational numbers in RR is defined as

Irrational(R){rR|isIrrational(r)}Irrational(R) \coloneqq \{r \in R \vert isIrrational(r) \}

In homotopy type theory

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 RR is defined as

r#s(r<s)+(s<r)r # s \coloneqq \Vert (r \lt s) + (s \lt r) \Vert

Let us define the dependent type on RR

isIrrational(r) a: b:(f(a)#0)×(f(a)r#f(b))isIrrational(r) \coloneqq \prod_{a:\mathbb{Z}} \prod_{b:\mathbb{Z}} (f(a) # 0) \times (f(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

Last revised on June 15, 2022 at 18:46:35. See the history of this page for a list of all contributions to it.