Demostrar con Lean4 que el producto de dos funciones impares es par.<\/p>\n
Para ello, completar la siguiente teor\u00eda de Lean4:<\/p>\n
\nimport Mathlib.Data.Real.Basic\n\nvariable (f g : \u211d \u2192 \u211d)\n\n-- (esPar f) expresa que f es par.\ndef esPar (f : \u211d \u2192 \u211d) : Prop :=\n \u2200 x, f x = f (-x)\n\n-- (esImpar f) expresa que f es impar.\ndef esImpar (f : \u211d \u2192 \u211d) : Prop :=\n \u2200 x, f x = - f (-x)\n\nexample\n (h1 : esImpar f)\n (h2 : esImpar g)\n : esPar (f * g) :=\nby sorry\n<\/pre>\n<\/p>\n
Demostraci\u00f3n en lenguaje natural<\/b><\/p>\n
\nSupongamos que \(f\) y \(g\) son funciones impares. Tenemos que demostrar que \(f\u00b7g\) es par; es decir, que
\n\[ (\u2200 x \u2208 \u211d) (f\u00b7g)(x) = (f\u00b7g)(-x) \]
\nSea \(x \u2208 \u211d\). Entonces,
\n\begin{align}
\n (f\u00b7g)(x) &= f(x)g(x) \\
\n &= (-f(-x))g(x) &&\text{[porque \(f\) es impar]} \\
\n &= (-f(-x)(-g(-x)) &&\text{[porque \(g\) es impar]} \\
\n &= f(-x)g(-x)) \\
\n &= (f\u00b7g)(-x)
\n\end{align}<\/p>\n
Demostraciones con Lean4<\/b><\/p>\n\nimport Mathlib.Data.Real.Basic\n\nvariable (f g : \u211d \u2192 \u211d)\n\n-- (esPar f) expresa que f es par.\ndef esPar (f : \u211d \u2192 \u211d) : Prop :=\n \u2200 x, f x = f (-x)\n\n-- (esImpar f) expresa que f es impar.\ndef esImpar (f : \u211d \u2192 \u211d) : Prop :=\n \u2200 x, f x = - f (-x)\n\n-- 1\u00aa demostraci\u00f3n\nexample\n (h1 : esImpar f)\n (h2 : esImpar g)\n : esPar (f * g) :=\nby\n intro x\n have h1 : f x = -f (-x) := h1 x\n have h2 : g x = -g (-x) := h2 x\n calc (f * g) x\n = f x * g x := rfl\n _ = (-f (-x)) * g x := congrArg (. * g x) h1\n _ = (-f (-x)) * (-g (-x)) := congrArg ((-f (-x)) * .) h2\n _ = f (-x) * g (-x) := neg_mul_neg (f (-x)) (g (-x))\n _ = (f * g) (-x) := rfl\n\n-- 2\u00aa demostraci\u00f3n\nexample\n (h1 : esImpar f)\n (h2 : esImpar g)\n : esPar (f * g) :=\nby\n intro x\n calc (f * g) x\n = f x * g x := rfl\n _ = (-f (-x)) * g x := congrArg (. * g x) (h1 x)\n _ = (-f (-x)) * (-g (-x)) := congrArg ((-f (-x)) * .) (h2 x)\n _ = f (-x) * g (-x) := neg_mul_neg (f (-x)) (g (-x))\n _ = (f * g) (-x) := rfl\n\n-- 3\u00aa demostraci\u00f3n\nexample\n (h1 : esImpar f)\n (h2 : esImpar g)\n : esPar (f * g) :=\nby\n intro x\n calc (f * g) x\n = f x * g x := rfl\n _ = -f (-x) * -g (-x) := by rw [h1, h2]\n _ = f (-x) * g (-x) := by rw [neg_mul_neg]\n _ = (f * g) (-x) := rfl\n\n-- 4\u00aa demostraci\u00f3n\nexample\n (h1 : esImpar f)\n (h2 : esImpar g)\n : esPar (f * g) :=\nby\n intro x\n calc (f * g) x\n = f x * g x := rfl\n _ = f (-x) * g (-x) := by rw [h1, h2, neg_mul_neg]\n _ = (f * g) (-x) := rfl\n\n-- Lemas usados\n-- ============\n\n-- variable (a b : \u211d)\n-- #check (neg_mul_neg a b : -a * -b = a * b)\n<\/pre>\nDemostraciones interactivas<\/b><\/p>\n
Se puede interactuar con las demostraciones anteriores en Lean 4 Web<\/a>.<\/p>\nReferencias<\/b><\/p>\n