Si a, b ∈ ℝ, entonces 2ab ≤ a² + b²
Demostrar que si a, b ∈ ℝ, entonces 2ab ≤ a² + b²
Para ello, completar la siguiente teoría de Lean:
1 2 3 4 5 6 7 |
import data.real.basic import tactic variables a b : ℝ example : 2*a*b ≤ a^2 + b^2 := sorry |