Las funciones f(x,y) = (x + y)² y g(x,y) = x² + 2xy + y² son iguales
Demostrar con Lean4 que las funciones \(f(x,y) = (x + y)²\) y \(g(x,y) = x² + 2xy + y\)² son iguales.
Para ello, completar la siguiente teoría de Lean4:
|
1 2 3 4 |
import Mathlib.Data.Real.Basic example : (fun x y : ℝ ↦ (x + y)^2) = (fun x y : ℝ ↦ x^2 + 2*x*y + y^2) := by sorry |
|
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 |
import Mathlib.Data.Real.Basic -- 1ª demostración -- =============== example : (fun x y : ℝ ↦ (x + y)^2) = (fun x y : ℝ ↦ x^2 + 2*x*y + y^2) := by ext u v -- u v : ℝ -- ⊢ (u + v) ^ 2 = u ^ 2 + 2 * u * v + v ^ 2 ring -- Comentario: La táctica ext transforma las conclusiones de la forma -- (fun x ↦ f x) = (fun x ↦ g x) en f x = g x. -- 2ª demostración -- =============== example : (fun x y : ℝ ↦ (x + y)^2) = (fun x y : ℝ ↦ x^2 + 2*x*y + y^2) := by { ext ; ring } |
Se puede interactuar con las demostraciones anteriores en Lean 4 Web.
Referencias
- J. Avigad y P. Massot. Mathematics in Lean, p. 41.
