pith. machine review for the scientific record. sign in
instance definition def or abbrev

rational_computable

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

formal statement (Lean)

 141instance rational_computable (q : ℚ) : Computable (q : ℝ) where
 142  approx := ⟨fun _ => q, by

proof body

Definition body.

 143    intro k
 144    simp only [sub_self, abs_zero]
 145    exact two_zpow_pos _⟩
 146
 147/-! ## Closure Properties -/
 148
 149/-- Negation is computable: approximate -x by -f(n). -/

depends on (6)

Lean names referenced from this declaration's body.