En ℝ, 2ab ≤ a² + b²
Sean \(a\) y \(b\) números reales. Demostrar con Lean4 que
\[2ab ≤ a^2 + b^2\]
Para ello, completar la siguiente teoría de Lean4:
|
1 2 3 4 5 6 |
import Mathlib.Data.Real.Basic variable (a b : ℝ) example : 2*a*b ≤ a^2 + b^2 := by sorry |