lean_workbook_plus_12207
ProvedFor and , prove that
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_12207 (a b : ℝ) (hab : a > 0 ∧ b > 0 ∧ a + b = 1) : (1 + 1 / a) * (1 + 1 / b) ≥ 9 := by sorry
Source
For and , prove that
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_12207 (a b : ℝ) (hab : a > 0 ∧ b > 0 ∧ a + b = 1) : (1 + 1 / a) * (1 + 1 / b) ≥ 9 := by sorry