Esta semana he publicado en Calculemus las demostraciones con Lean4 de las siguientes propiedades:
A continuación se muestran las soluciones.
1. El producto de dos funciones impares es par
Demostrar con Lean4 que el producto de dos funciones impares es par.
Para ello, completar la siguiente teoría de Lean4:
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 |
import Mathlib.Data.Real.Basic variable (f g : ℝ → ℝ) -- (esPar f) expresa que f es par. def esPar (f : ℝ → ℝ) : Prop := ∀ x, f x = f (-x) -- (esImpar f) expresa que f es impar. def esImpar (f : ℝ → ℝ) : Prop := ∀ x, f x = - f (-x) example (h1 : esImpar f) (h2 : esImpar g) : esPar (f * g) := by sorry |
Demostración en lenguaje natural
Supongamos que f y g son funciones impares. Tenemos que demostrar que f·g es par; es decir, que
(∀x∈ℝ)(f·g)(x)=(f·g)(−x)
Sea x∈ℝ. Entonces,
(f·g)(x)=f(x)g(x)=(−f(−x))g(x)[porque f es impar]=(−f(−x)(−g(−x))[porque g es impar]=f(−x)g(−x))=(f·g)(−x)
Demostraciones con Lean4
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 |
import Mathlib.Data.Real.Basic variable (f g : ℝ → ℝ) -- (esPar f) expresa que f es par. def esPar (f : ℝ → ℝ) : Prop := ∀ x, f x = f (-x) -- (esImpar f) expresa que f es impar. def esImpar (f : ℝ → ℝ) : Prop := ∀ x, f x = - f (-x) -- 1ª demostración example (h1 : esImpar f) (h2 : esImpar g) : esPar (f * g) := by intro x have h1 : f x = -f (-x) := h1 x have h2 : g x = -g (-x) := h2 x calc (f * g) x = f x * g x := rfl _ = (-f (-x)) * g x := congrArg (. * g x) h1 _ = (-f (-x)) * (-g (-x)) := congrArg ((-f (-x)) * .) h2 _ = f (-x) * g (-x) := neg_mul_neg (f (-x)) (g (-x)) _ = (f * g) (-x) := rfl -- 2ª demostración example (h1 : esImpar f) (h2 : esImpar g) : esPar (f * g) := by intro x calc (f * g) x = f x * g x := rfl _ = (-f (-x)) * g x := congrArg (. * g x) (h1 x) _ = (-f (-x)) * (-g (-x)) := congrArg ((-f (-x)) * .) (h2 x) _ = f (-x) * g (-x) := neg_mul_neg (f (-x)) (g (-x)) _ = (f * g) (-x) := rfl -- 3ª demostración example (h1 : esImpar f) (h2 : esImpar g) : esPar (f * g) := by intro x calc (f * g) x = f x * g x := rfl _ = -f (-x) * -g (-x) := by rw [h1, h2] _ = f (-x) * g (-x) := by rw [neg_mul_neg] _ = (f * g) (-x) := rfl -- 4ª demostración example (h1 : esImpar f) (h2 : esImpar g) : esPar (f * g) := by intro x calc (f * g) x = f x * g x := rfl _ = f (-x) * g (-x) := by rw [h1, h2, neg_mul_neg] _ = (f * g) (-x) := rfl -- Lemas usados -- ============ -- variable (a b : ℝ) -- #check (neg_mul_neg a b : -a * -b = a * b) |
Demostraciones interactivas
Se puede interactuar con las demostraciones anteriores en Lean 4 Web.
Referencias
2. El producto de una función par por una impar es impar
Demostrar con Lean4 que el producto de una función par por una impar es impar.
Para ello, completar la siguiente teoría de Lean4:
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 |
import Mathlib.Data.Real.Basic variable (f g : ℝ → ℝ) -- (esPar f) expresa que f es par. def esPar (f : ℝ → ℝ) : Prop := ∀ x, f x = f (-x) -- (esImpar f) expresa que f es impar. def esImpar (f : ℝ → ℝ) : Prop := ∀ x, f x = - f (-x) example (h1 : esPar f) (h2 : esImpar g) : esImpar (f * g) := by sorry |
Demostración en lenguaje natural
Supongamos que f es una función par y g lo es impar. Tenemos que demostrar que f·g es imppar; es decir, que
(∀x∈ℝ)(f·g)(x)=−(f·g)(−x)
Sea x∈ℝ. Entonces,
(f·g)x=f(x)g(x)=f(−x)g(x)[porque f es par]=f(−x)(−g(−x))[porque g es impar]=−f(−x)g(−x))=−(f·g)(−x)
Demostraciones con Lean4
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 |
import Mathlib.Data.Real.Basic variable (f g : ℝ → ℝ) -- (esPar f) expresa que f es par. def esPar (f : ℝ → ℝ) : Prop := ∀ x, f x = f (-x) -- (esImpar f) expresa que f es impar. def esImpar (f : ℝ → ℝ) : Prop := ∀ x, f x = - f (-x) -- 1ª demostración example (h1 : esPar f) (h2 : esImpar g) : esImpar (f * g) := by intro x have h1 : f x = f (-x) := h1 x have h2 : g x = -g (-x) := h2 x calc (f * g) x = f x * g x := rfl _ = (f (-x)) * g x := congrArg (. * g x) h1 _ = (f (-x)) * (-g (-x)) := congrArg (f (-x) * .) h2 _ = -(f (-x) * g (-x)) := mul_neg (f (-x)) (g (-x)) _ = -(f * g) (-x) := rfl -- 2ª demostración example (h1 : esPar f) (h2 : esImpar g) : esImpar (f * g) := by intro x calc (f * g) x = f x * g x := rfl _ = f (-x) * -g (-x) := by rw [h1, h2] _ = -(f (-x) * g (-x)) := by rw [mul_neg] _ = -(f * g) (-x) := rfl -- 3ª demostración example (h1 : esPar f) (h2 : esImpar g) : esImpar (f * g) := by intro x calc (f * g) x = f x * g x := rfl _ = -(f (-x) * g (-x)) := by rw [h1, h2, mul_neg] _ = -((f * g) (-x)) := rfl -- Lemas usados -- =========== -- variable (a b : ℝ) -- #check (mul_neg a b : a * -b = -(a * b)) |
Demostraciones interactivas
Se puede interactuar con las demostraciones anteriores en Lean 4 Web.
Referencias
3. Si f es par y g es impar, entonces (f ∘ g) es par
Demostrar con Lean4 que si f es par y g es impar, entonces f∘g es par.
Para ello, completar la siguiente teoría de Lean4:
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 |
import Mathlib.Data.Real.Basic variable (f g : ℝ → ℝ) -- (esPar f) expresa que f es par. def esPar (f : ℝ → ℝ) : Prop := ∀ x, f x = f (-x) -- (esImpar f) expresa que f es impar. def esImpar (f : ℝ → ℝ) : Prop := ∀ x, f x = - f (-x) example (h1 : esPar f) (h2 : esImpar g) : esPar (f ∘ g) := by sorry |
Demostración en lenguaje natural
Supongamos que f es una función par y g lo es impar. Tenemos que demostrar que f∘g es par; es decir, que
(∀x∈ℝ)(f∘g)(x)=(f∘g)(−x)
Sea x∈ℝ. Entonces,
(f∘g)(x)=f(g(x))=f(−g(−x))[porque g es impar]=f(g(−x))[porque f es par]=(f∘g)(−x)
Demostraciones con Lean4
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 |
import Mathlib.Data.Real.Basic variable (f g : ℝ → ℝ) -- (esPar f) expresa que f es par. def esPar (f : ℝ → ℝ) : Prop := ∀ x, f x = f (-x) -- (esImpar f) expresa que f es impar. def esImpar (f : ℝ → ℝ) : Prop := ∀ x, f x = - f (-x) -- 1ª demostración example (h1 : esPar f) (h2 : esImpar g) : esPar (f ∘ g) := by intro x calc (f ∘ g) x = f (g x) := rfl _ = f (-g (-x)) := congr_arg f (h2 x) _ = f (g (-x)) := (h1 (g (-x))).symm _ = (f ∘ g) (-x) := rfl -- 2ª demostración example (h1 : esPar f) (h2 : esImpar g) : esPar (f ∘ g) := by intro x calc (f ∘ g) x = f (g x) := rfl _ = f (-g (-x)) := by rw [h2] _ = f (g (-x)) := by rw [← h1] _ = (f ∘ g) (-x) := rfl -- 3ª demostración example (h1 : esPar f) (h2 : esImpar g) : esPar (f ∘ g) := by intro x calc (f ∘ g) x = f (g x) := rfl _ = f (g (-x)) := by rw [h2, ← h1] |
Demostraciones interactivas
Se puede interactuar con las demostraciones anteriores en Lean 4 Web.
Referencias
4. Para cualquier conjunto s, s ⊆ s
Demostrar con Lean4 que para cualquier conjunto s, s⊆s.
Para ello, completar la siguiente teoría de Lean4:
|
|
import Mathlib.Tactic variable {α : Type _} variable (s : Set α) example : s ⊆ s := by sorry |
Demostración en lenguaje natural
Tenemos que demostrar que
(∀x)[x∈s→×∈s]
Sea x tal que
x∈s
Entonces, por (1), se tiene que
x∈s
que es lo que teníamos que demostrar.
Demostraciones con Lean4
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 |
import Mathlib.Tactic variable {α : Type _} variable (s : Set α) -- 1ª demostración example : s ⊆ s := by intro x xs exact xs -- 2ª demostración example : s ⊆ s := fun (x : α) (xs : x ∈ s) ↦ xs -- 3ª demostración example : s ⊆ s := fun _ xs ↦ xs -- 4ª demostración example : s ⊆ s := -- by exact? rfl.subset -- 5ª demostración example : s ⊆ s := by rfl |
Demostraciones interactivas
Se puede interactuar con las demostraciones anteriores en Lean 4 Web.
Referencias
5. Si r ⊆ s y s ⊆ t, entonces r ⊆ t
Demostrar con Lean4 que si r⊆s y s⊆t, entonces r⊆t.
Para ello, completar la siguiente teoría de Lean4:
|
|
import Mathlib.Tactic open Set variable {α : Type _} variable (r s t : Set α) example (rs : r ⊆ s) (st : s ⊆ t) : r ⊆ t := by sorry |
Demostración en lenguaje natural
1ª demostración en LN
Tenemos que demostrar que
(∀x)[x∈r→x∈t]
Sea x tal que
x∈r
Puesto que r⊆s, se tiene que
x∈s
y, puesto que \(s ⊆ t), se tiene que
x∈t
que es lo que teníamos que demostrar.
2ª demostración en LN
Tenemos que demostrar que
(∀x)[x∈r→x∈t]
Sea x tal que
x∈r
Tenemos que demostrar que
x∈t
que, puesto que s⊆t, se reduce a
x∈s
que, puesto que r⊆s, se redece a
x∈r
que es lo que hemos supuesto.
Demostraciones con Lean4
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 |
import Mathlib.Tactic open Set variable {α : Type _} variable (r s t : Set α) -- 1ª demostración example (rs : r ⊆ s) (st : s ⊆ t) : r ⊆ t := by intros x xr -- xr : x ∈ r have xs : x ∈ s := rs xr show x ∈ t exact st xs -- 2ª demostración example (rs : r ⊆ s) (st : s ⊆ t) : r ⊆ t := by intros x xr -- x : α -- xr : x ∈ r apply st -- ⊢ x ∈ s apply rs -- ⊢ x ∈ r exact xr -- 3ª demostración example (rs : r ⊆ s) (st : s ⊆ t) : r ⊆ t := fun _ xr ↦ st (rs xr) -- 4ª demostración example (rs : r ⊆ s) (st : s ⊆ t) : r ⊆ t := -- by exact? Subset.trans rs st -- 5ª demostración example (rs : r ⊆ s) (st : s ⊆ t) : r ⊆ t := by tauto -- Lemas usados -- ============ -- #check (Subset.trans : r ⊆ s → s ⊆ t → r ⊆ t) |
Demostraciones interactivas
Se puede interactuar con las demostraciones anteriores en Lean 4 Web.
Referencias