lean_workbook_plus_26199

Disproved

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

( $(\\sqrt2-t))(\\frac{5}{\\sqrt2}-t)\\geq0,$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_26199 : ∀ t : ℝ, (Real.sqrt 2 - t) * (5 / Real.sqrt 2 - t) ≥ 0   :=  by sorry

Source