lean_workbook_plus_49510
ProvedLet and . Prove that: .
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_49510 : ∀ x y : ℝ, x ≥ 0 ∧ y ≥ 0 ∧ x + y = 1 → x^2*y^2*(x^2+y^2) ≤ 2 := by sorry
Source
Let and . Prove that: .
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_49510 : ∀ x y : ℝ, x ≥ 0 ∧ y ≥ 0 ∧ x + y = 1 → x^2*y^2*(x^2+y^2) ≤ 2 := by sorry