lean_workbook_plus_55862
ProvedLet and Prove that
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_55862 : ∀ x y : ℝ, x + y = 1 ∧ x >= 0 ∧ y >= 0 → x ^ 2 + y ^ 2 + x ^ 2 * y ^ 2 >= 9 / 16 := by sorry
Source
Let and Prove that
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_55862 : ∀ x y : ℝ, x + y = 1 ∧ x >= 0 ∧ y >= 0 → x ^ 2 + y ^ 2 + x ^ 2 * y ^ 2 >= 9 / 16 := by sorry