La semana en Calculemus (18 de noviembre de 2023)
Esta semana he publicado en Calculemus las demostraciones con Lean4 de las siguientes propiedades:
- 1. Si f: ℝ → ℝ es suprayectiva, entonces ∃x ∈ ℝ tal que f(x)² = 9
- 2. La composición de funciones suprayectivas es suprayectiva
- 3. En ℝ, a < b → ¬(b < a)
- 4. Si para cada a existe un x tal que f(x) > a, entonces f no tiene cota superior
- 5. Si para cada a existe un x tal que f(x) < a, entonces f no tiene cota inferior
A continuación se muestran las soluciones.
1. Si f: ℝ → ℝ es suprayectiva, entonces ∃x ∈ ℝ tal que f(x)² = 9
Demostrar con Lean4 que si \(f: ℝ → ℝ\) es suprayectiva, entonces \(∃x ∈ ℝ\) tal que \(f(x)² = 9\).
Para ello, completar la siguiente teoría de Lean4:
|
1 2 3 4 5 6 7 8 |
import Mathlib.Data.Real.Basic open Function example {f : ℝ → ℝ} (h : Surjective f) : ∃ x, (f x)^2 = 9 := by sorry |
Demostración en lenguaje natural
Al ser \(f\) suprayectiva, existe un \(y\) tal que \(f(y) = 3\). Por tanto, \(f(y)² = 9\).
Demostraciones con Lean4
|
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 |
import Mathlib.Data.Real.Basic open Function example {f : ℝ → ℝ} (h : Surjective f) : ∃ x, (f x)^2 = 9 := by cases' h 3 with y hy -- y : ℝ -- hy : f y = 3 use y -- ⊢ f y ^ 2 = 9 rw [hy] -- ⊢ 3 ^ 2 = 9 norm_num |
Demostraciones interactivas
Se puede interactuar con las demostraciones anteriores en Lean 4 Web.
Referencias
- J. Avigad y P. Massot. Mathematics in Lean, p. 31.
2. La composición de funciones suprayectivas es suprayectiva
Demostrar con Lean4 que la composición de funciones suprayectivas es suprayectiva.
Para ello, completar la siguiente teoría de Lean4:
|
1 2 3 4 5 6 7 8 9 10 |
import Mathlib.Tactic open Function variable {α : Type _} {β : Type _} {γ : Type _} variable {f : α → β} {g : β → γ} example (hg : Surjective g) (hf : Surjective f) : Surjective (g ∘ f) := by sorry |
Demostración en lenguaje natural
Supongamos que \(f : A → B\) y \(g : B → C\) son suprayectivas. Tenemosque demostrar que
\[ (∀z ∈ C)(∃x ∈ A)[g(f(x)) = z] \]
Sea \(z ∈ C\). Por ser \(g\) suprayectiva, existe un \(y ∈ B\) tal que
\[ g(y) = z \tag{1} \]
Por ser \(f\) suprayectiva, existe un \(x ∈ A\) tal que
\[ f(x) = y \tag{2} \]
Por tanto,
\begin{align}
g(f(x)) &= g(y) &&\text{[por (2)]} \\
&= z &&\text{[por (1)]}
\end{align}
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 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 |
import Mathlib.Tactic open Function variable {α : Type _} {β : Type _} {γ : Type _} variable {f : α → β} {g : β → γ} -- 1ª demostración example (hg : Surjective g) (hf : Surjective f) : Surjective (g ∘ f) := by intro z -- z : γ -- ⊢ ∃ a, (g ∘ f) a = z cases' hg z with y hy -- y : β -- hy : g y = z cases' hf y with x hx -- x : α -- hx : f x = y use x -- ⊢ (g ∘ f) x = z dsimp -- ⊢ g (f x) = z rw [hx] -- ⊢ g y = z exact hy -- 2ª demostración example (hg : Surjective g) (hf : Surjective f) : Surjective (g ∘ f) := by intro z -- z : γ -- ⊢ ∃ a, (g ∘ f) a = z cases' hg z with y hy -- y : β -- hy : g y = z cases' hf y with x hx -- x : α -- hx : f x = y use x -- ⊢ (g ∘ f) x = z dsimp -- ⊢ g (f x) = z rw [hx, hy] -- 3ª demostración example (hg : Surjective g) (hf : Surjective f) : Surjective (g ∘ f) := by intro z -- z : γ -- ⊢ ∃ a, (g ∘ f) a = z cases' hg z with y hy -- y : β -- hy : g y = z cases' hf y with x hx -- x : α -- hx : f x = y exact ⟨x, by dsimp ; rw [hx, hy]⟩ -- 4ª demostración example (hg : Surjective g) (hf : Surjective f) : Surjective (g ∘ f) := by intro z -- z : γ -- ⊢ ∃ a, (g ∘ f) a = z rcases hg z with ⟨y, hy : g y = z⟩ rcases hf y with ⟨x, hx : f x = y⟩ exact ⟨x, by dsimp ; rw [hx, hy]⟩ -- 5ª demostración example (hg : Surjective g) (hf : Surjective f) : Surjective (g ∘ f) := Surjective.comp hg hf -- Lemas usados -- ============ -- #check (Surjective.comp : Surjective g → Surjective f → Surjective (g ∘ f)) |
Demostraciones interactivas
Se puede interactuar con las demostraciones anteriores en Lean 4 Web.
Referencias
- J. Avigad y P. Massot. Mathematics in Lean, p. 31.
3. En ℝ, a < b → ¬(b < a)
Demostrar con Lean4 que en \(ℝ\), \(a < b → ¬(b < a)\).
Para ello, completar la siguiente teoría de Lean4:
|
1 2 3 4 5 6 7 8 |
import Mathlib.Data.Real.Basic variable (a b : ℝ) example (h : a < b) : ¬ b < a := by sorry |
Demostración en lenguaje natural
Por hipótesis \(a < b\) y tenemos que demostrar que \(¬(b < a)\). Supongamos que \(b < a\). Entonces, por la propiedad transiva \(a < a\) que es una contradicción con la propiedad irreflexiva.
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 |
import Mathlib.Data.Real.Basic variable (a b : ℝ) -- 1ª demostración example (h : a < b) : ¬ b < a := by intro h1 -- h1 : b < a -- ⊢ False have : a < a := lt_trans h h1 apply lt_irrefl a this -- 2ª demostración example (h : a < b) : ¬ b < a := by intro h1 -- h1 : b < a -- ⊢ False exact lt_irrefl a (lt_trans h h1) -- 3ª demostración example (h : a < b) : ¬ b < a := fun h1 ↦ lt_irrefl a (lt_trans h h1) -- 4ª demostración example (h : a < b) : ¬ b < a := lt_asymm h -- Lemas usados -- ============ -- variable (c : ℝ) -- #check (lt_asymm : a < b → ¬b < a) -- #check (lt_irrefl a : ¬a < a) -- #check (lt_trans : a < b → b < c → a < c) |
Demostraciones interactivas
Se puede interactuar con las demostraciones anteriores en Lean 4 Web.
Referencias
- J. Avigad y P. Massot. Mathematics in Lean, p. 32.
4. Si para cada a existe un x tal que f(x) > a, entonces f no tiene cota superior
Demostrar con Lean4 que si \(f\) es una función de \(ℝ\) en \(ℝ\) tal que para cada \(a\) existe un \(x\) tal que \(f(x) > a\), entonces \(f\) no tiene cota superior.
Para ello, completar la siguiente teoría de Lean4:
|
1 2 3 4 5 6 7 8 9 10 11 12 13 14 |
import Mathlib.Data.Real.Basic def CotaSuperior (f : ℝ → ℝ) (a : ℝ) : Prop := ∀ x, f x ≤ a def acotadaSup (f : ℝ → ℝ) : Prop := ∃ a, CotaSuperior f a variable (f : ℝ → ℝ) example (h : ∀ a, ∃ x, f x > a) : ¬ acotadaSup f := by sorry |
Demostración en lenguaje natural
Supongamos que \(f\) tiene cota superior. Sea \(b\) una de dichas cotas superiores. Por la hipótesis, existe un \(x\) tal que \(f(x) > b\). Además, como \(b\) es una cota superior de \(f\), \(f(x) ≤ b\) que contradice la desigualdad anterior.
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 |
import Mathlib.Data.Real.Basic def CotaSuperior (f : ℝ → ℝ) (a : ℝ) : Prop := ∀ x, f x ≤ a def acotadaSup (f : ℝ → ℝ) : Prop := ∃ a, CotaSuperior f a variable (f : ℝ → ℝ) -- 1ª demostración example (h : ∀ a, ∃ x, f x > a) : ¬ acotadaSup f := by intros hf -- hf : acotadaSup f -- ⊢ False cases' hf with b hb -- b : ℝ -- hb : CotaSuperior f b cases' h b with x hx -- x : ℝ -- hx : f x > b have : f x ≤ b := hb x linarith -- 2ª demostración theorem sinCotaSup (h : ∀ a, ∃ x, f x > a) : ¬ acotadaSup f := by intros hf -- hf : acotadaSup f -- ⊢ False rcases hf with ⟨b, hb : CotaSuperior f b⟩ rcases h b with ⟨x, hx : f x > b⟩ have : f x ≤ b := hb x linarith |
Demostraciones interactivas
Se puede interactuar con las demostraciones anteriores en Lean 4 Web.
Referencias
- J. Avigad y P. Massot. Mathematics in Lean, p. 32.
5. Si para cada a existe un x tal que f(x) < a, entonces f no tiene cota inferior
Demostrar con Lean4 que si \(f\) es una función de \(ℝ\) en \(ℝ\) tal que para cada \(a\) existe un \(x\) tal que \(f(x) < a\), entonces \(f\) no tiene cota inferior.
Para ello, completar la siguiente teoría de Lean4:
|
1 2 3 4 5 6 7 8 9 10 11 12 13 14 |
import Mathlib.Data.Real.Basic def CotaInferior (f : ℝ → ℝ) (a : ℝ) : Prop := ∀ x, a ≤ f x def acotadaInf (f : ℝ → ℝ) : Prop := ∃ a, CotaInferior f a variable (f : ℝ → ℝ) example (h : ∀ a, ∃ x, f x < a) : ¬ acotadaInf f := by sorry |
Demostración en lenguaje natural
Supongamos que \(f\) tiene cota inferior. Sea \(b\) una de dichas cotas inferiores. Por la hipótesis, existe un \(x\) tal que \(f(x) < b\). Además, como \(b\) es una cota inferior de \(f\), \(b ≤ f(x)\) que contradice la desigualdad anterior.
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 |
import Mathlib.Data.Real.Basic def CotaInferior (f : ℝ → ℝ) (a : ℝ) : Prop := ∀ x, a ≤ f x def acotadaInf (f : ℝ → ℝ) : Prop := ∃ a, CotaInferior f a variable (f : ℝ → ℝ) -- 1ª demostración example (h : ∀ a, ∃ x, f x < a) : ¬ acotadaInf f := by intros hf -- hf : acotadaInf f -- ⊢ False cases' hf with b hb -- b : ℝ -- hb : CotaInferior f b cases' h b with x hx -- x : ℝ -- hx : f x < b have : b ≤ f x := hb x linarith -- 2ª demostración example (h : ∀ a, ∃ x, f x < a) : ¬ acotadaInf f := by intros hf -- hf : acotadaInf f -- ⊢ False rcases hf with ⟨b, hb : CotaInferior f b⟩ rcases h b with ⟨x, hx : f x < b⟩ have : b ≤ f x := hb x linarith |
Demostraciones interactivas
Se puede interactuar con las demostraciones anteriores en Lean 4 Web.
Referencias
- J. Avigad y P. Massot. Mathematics in Lean, p. 32.