A degree structure on representations of irrational numbers

Amir Ben-Amram, Lars Kristiansen

Code by ChatGPT, mostly.

noncomputable def dedekind_cut_fn (α : ℝ) : ℚ → ℕ

Equations

• dedekind_cut_fn α q = if ↑q < α then 0 else 1