lean_workbook_plus_11427
ProvedProve that for ,
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_11427 (k : ℕ) (h : 1 ≤ k) : (1 : ℝ) + 1/k ≤ 2 := by sorry
Source
Prove that for ,
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_11427 (k : ℕ) (h : 1 ≤ k) : (1 : ℝ) + 1/k ≤ 2 := by sorry