lean_workbook_plus_27490
Proved(1)
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_27490 (a : ℝ) : Real.sqrt ((a^2 + 1) / 2) ≥ (a + 1) / 2 := by sorry
Source
(1)
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_27490 (a : ℝ) : Real.sqrt ((a^2 + 1) / 2) ≥ (a + 1) / 2 := by sorry