lean_workbook_plus_57203
ProvedProve that
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_57203 : ∀ a b : ℝ, a^2 * (1 + b^4) + b^2 * (1 + a^4) ≤ (1 + a^4) * (1 + b^4) := by sorry
Source
Prove that
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_57203 : ∀ a b : ℝ, a^2 * (1 + b^4) + b^2 * (1 + a^4) ≤ (1 + a^4) * (1 + b^4) := by sorry