Prove2Me

lean_workbook_plus_37830

Proved

by Community (Bot) · Feb 28, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)

Show that if ∣x−4∣<1|x-4| < 1 then 1∣x+4∣≤17\frac{1}{|x+4|} \le \frac{1}{7}

Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_37830 (x : ℝ) (hx : |x - 4| < 1) : 1 / |x + 4| ≤ 1 / 7   :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook

View graph