lean_workbook_plus_24391
ProvedLet . Prove using calculus that:
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_24391 : ∀ x y : ℝ, 0 ≤ x ∧ x ≤ y ∧ y ≤ 1 → 1 / 4 ≥ y * x ^ 2 - x * y ^ 2 := by sorry
Source
Let . Prove using calculus that:
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_24391 : ∀ x y : ℝ, 0 ≤ x ∧ x ≤ y ∧ y ≤ 1 → 1 / 4 ≥ y * x ^ 2 - x * y ^ 2 := by sorry