{"id":1698,"date":"2023-10-18T06:00:53","date_gmt":"2023-10-18T04:00:53","guid":{"rendered":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/?p=1698"},"modified":"2023-10-10T12:51:28","modified_gmt":"2023-10-10T10:51:28","slug":"18-oct-23","status":"publish","type":"post","link":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/18-oct-23\/","title":{"rendered":"Si f es par y g es impar, entonces (f \u2218 g) es par"},"content":{"rendered":"

Demostrar con Lean4 que si \(f\) es par y \(g\) es impar, entonces \(f \u2218 g\) 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 : esPar f)\n  (h2 : esImpar g)\n  : esPar (f \u2218 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 \u2218 g\) es par; es decir, que
\n\[ (\u2200 x \u2208 \u211d) (f \u2218 g)(x) = (f \u2218 g)(-x) \]
\nSea \(x \u2208 \u211d\). Entonces,
\n\begin{align}
\n   (f \u2218 g)(x) &= f(g(x))      \\
\n              &= f(-g(-x))    &&\text{[porque \(g\) es impar]} \\
\n              &= f(g(-x))     &&\text{[porque \(f\) es par]} \\
\n              &= (f \u2218 g)(-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  : esPar (f \u2218 g) :=\nby\n  intro x\n  calc (f \u2218 g) x\n       = f (g x)      := rfl\n    _  = f (-g (-x))  := congr_arg f (h2 x)\n    _  = f (g (-x))   := (h1 (g (-x))).symm\n    _  = (f \u2218 g) (-x) := rfl\n\n-- 2\u00aa demostraci\u00f3n\nexample\n  (h1 : esPar f)\n  (h2 : esImpar g)\n  : esPar (f \u2218 g) :=\nby\n  intro x\n  calc (f \u2218 g) x\n       = f (g x)      := rfl\n     _ = f (-g (-x))  := by rw [h2]\n     _ = f (g (-x))   := by rw [\u2190 h1]\n     _ = (f \u2218 g) (-x) := rfl\n\n-- 3\u00aa demostraci\u00f3n\nexample\n  (h1 : esPar f)\n  (h2 : esImpar g)\n  : esPar (f \u2218 g) :=\nby\n  intro x\n  calc (f \u2218 g) x\n       = f (g x)      := rfl\n     _ = f (g (-x))   := by rw [h2, \u2190 h1]\n<\/pre>\n
Demostraciones interactivas<\/b><\/p>\n
Se puede interactuar con las demostraciones anteriores en Lean 4 Web<\/a>.<\/p>\n
Referencias<\/b><\/p>\n