mathlib documentation

lean_problem_sheets / 2020.sets.real_numbers

structure mynnreal :

Type

floor : ℕ
frac : ℕ → fin 10
no_nines : ∀ (B : ℕ), ∃ (N : ℕ), B ≤ N ∧ self.frac N ≠ 9

The non-negative real numbers in the mind of a schoolkid

def mynnreal.to_real (x : mynnreal) :

Equations

x.to_real = ↑(x.floor) + 0