Demostrar con Lean4 que el producto de una funci\u00f3n par por una impar es impar.<\/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 : esPar f)\n (h2 : esImpar g)\n : esImpar (f * g) :=\nby sorry\n<\/pre>\n<\/p>\n
Demostraci\u00f3n en lenguaje natural<\/b><\/p>\n
\nSupongamos que \(f\) es una funci\u00f3n par y \(g\) lo es impar. Tenemos que demostrar que \(f\u00b7g\) es imppar; 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 par]} \\
\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 : esPar f)\n (h2 : esImpar g)\n : esImpar (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)) := mul_neg (f (-x)) (g (-x))\n _ = -(f * g) (-x) := rfl\n\n-- 2\u00aa demostraci\u00f3n\nexample\n (h1 : esPar f)\n (h2 : esImpar g)\n : esImpar (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 [mul_neg]\n _ = -(f * g) (-x) := rfl\n\n-- 3\u00aa demostraci\u00f3n\nexample\n (h1 : esPar f)\n (h2 : esImpar g)\n : esImpar (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, mul_neg]\n _ = -((f * g) (-x)) := rfl\n\n-- Lemas usados\n-- ===========\n\n-- variable (a b : \u211d)\n-- #check (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