lean_workbook_plus_17534

Proved

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

If $2b - \frac{1}{c} > 1$ , then $2b > 1 + \frac{1}{c}$ $b > \frac{1}{2} + \frac{1}{2c}$ $b +1 > \frac{3}{2} + \frac{1}{2c}$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_17534  (b c : ℝ)
  (h₀ : 2 * b - 1 / c > 1) :
  2 * b > 1 + 1 / c ∧ b > 1 / 2 + 1 / (2 * c) ∧ b + 1 > 3 / 2 + 1 / (2 * c)   :=  by sorry

Source

https://huggingface.co/datasets/internlm/Lean-Workbook

View graph