La semana en Calculemus (25 de noviembre de 2023)
Esta semana he publicado en Calculemus las demostraciones con Lean4 de las siguientes propiedades:
- 1. La función identidad no está acotada superiormente
- 2. Si f es monótona y f(a) < f(b), entonces a < b
- 3. Si a, b ∈ ℝ tales que a ≤ b y f(b) < f(a), entonces f no es monótona
- 4. No para toda f : ℝ → ℝ monótona, (∀a,b)(f(a) ≤ f(b) → a ≤ b)
- 5. Si (∀ε > 0)(x ≤ ε), entonces x ≤ 0
A continuación se muestran las soluciones.
1. La función identidad no está acotada superiormente
Demostrar con Lean4 que la función identidad no está acotada superiormente.
Para ello, completar la siguiente teoría de Lean4:
|
1 2 3 4 |
import src.Funcion_no_acotada_superiormente example : ¬ acotadaSup (fun x ↦ x) := by sorry |
Demostración en lenguaje natural
Usando el lema de ejercicio anterior (que afirma que si para cada \(a\), existe un \(x\) tal que \(f(x) > a\), entonces \(f\) no tiene cota superior) basta demostrar que
\[ (∀a ∈ ℝ)(∃x ∈ ℝ) [x > a] \]
Sea \(a ∈ ℝ\). Entonces \(a + 1 > a\) y, por tanto, \((∃x ∈ ℝ) [x > a]\).
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 |
import src.Funcion_no_acotada_superiormente -- 1ª demostración example : ¬ acotadaSup (fun x ↦ x) := by apply sinCotaSup -- ⊢ ∀ (a : ℝ), ∃ x, x > a intro a -- a : ℝ -- ⊢ ∃ x, x > a use a + 1 -- ⊢ a + 1 > a linarith -- 2ª demostración example : ¬ acotadaSup (fun x ↦ x) := by apply sinCotaSup -- ⊢ ∀ (a : ℝ), ∃ x, x > a intro a -- a : ℝ -- ⊢ ∃ x, x > a exact ⟨a + 1, by linarith⟩ -- 3ª demostración example : ¬ acotadaSup (fun x ↦ x) := by apply sinCotaSup -- ⊢ ∀ (a : ℝ), ∃ x, x > a exact fun a ↦ ⟨a + 1, by 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.
2. Si f es monótona y f(a) < f(b), entonces a < b
Demostrar con Lean4 que si \(f\) es monótona y \(f(a) < f(b)\), entonces \(a < b\).
Para ello, completar la siguiente teoría de Lean4:
|
1 2 3 4 5 6 7 8 9 |
import Mathlib.Data.Real.Basic variable (f : ℝ → ℝ) variable (a b : ℝ) example (h1 : Monotone f) (h2 : f a < f b) : a < b := by sorry |
Demostración en lenguaje natural
Usaremos los lemas
\begin{align}
&a ≱ b → a < b \tag{L1} \\
&a ≥ b → a ≮ b \tag{L2}
\end{align}
Por el lema L1, basta demostrar que \(a ≱ b\). Lo haremos reducción al absurdo. Para ello, supongamos que \(a ≥ b\). Como \(f\) es monótona, se tiene \(f(a) ≥ f(b)\) y, aplicando el lema L2, \(f(a) ≮ f(b)\), que contradice a la hipótesis.
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 |
import Mathlib.Data.Real.Basic variable (f : ℝ → ℝ) variable (a b : ℝ) -- 1ª demostración -- =============== example (h1 : Monotone f) (h2 : f a < f b) : a < b := by apply lt_of_not_ge -- ⊢ ¬a ≥ b intro h3 -- h3 : a ≥ b -- ⊢ False have h4 : f a ≥ f b := h1 h3 have h5 : ¬ f a < f b := not_lt_of_ge h4 exact h5 h2 -- 2ª demostración -- =============== example (h1 : Monotone f) (h2 : f a < f b) : a < b := by apply lt_of_not_ge -- ⊢ ¬a ≥ b intro h3 -- h3 : a ≥ b -- ⊢ False have h5 : ¬ f a < f b := not_lt_of_ge (h1 h3) exact h5 h2 -- 3ª demostración -- =============== example (h1 : Monotone f) (h2 : f a < f b) : a < b := by apply lt_of_not_ge -- ⊢ ¬a ≥ b intro h3 -- h3 : a ≥ b -- ⊢ False exact (not_lt_of_ge (h1 h3)) h2 -- 4ª demostración -- =============== example (h1 : Monotone f) (h2 : f a < f b) : a < b := by apply lt_of_not_ge -- ⊢ ¬a ≥ b exact fun h3 ↦ (not_lt_of_ge (h1 h3)) h2 -- 5ª demostración -- =============== example (h1 : Monotone f) (h2 : f a < f b) : a < b := lt_of_not_ge (fun h3 ↦ (not_lt_of_ge (h1 h3)) h2) -- Lemas usados -- ============ -- #check (lt_of_not_ge : ¬ a ≥ b → a < b) -- #check (not_lt_of_ge : a ≥ b → ¬ a < b) |
Demostraciones interactivas
Se puede interactuar con las demostraciones anteriores en Lean 4 Web.
Referencias
- J. Avigad y P. Massot. Mathematics in Lean, p. 32.
3. Si a, b ∈ ℝ tales que a ≤ b y f(b) < f(a), entonces f no es monótona
Demostrar con Lean4 que si \(a, b ∈ ℝ\) tales que \(a ≤ b\) y \(f(b) < f(a)\), entonces \(f\) no es monótona
Para ello, completar la siguiente teoría de Lean4:
|
1 2 3 4 5 6 7 8 9 |
import Mathlib.Data.Real.Basic variable (f : ℝ → ℝ) variable (a b : ℝ) example (h1 : a ≤ b) (h2 : f b < f a) : ¬ Monotone f := by sorry |
Demostración en lenguaje natural
Usaremos el lema
\[ a ≥ b → a ≮ b \tag{L1} \]
Lo demostraremos por reducción al absurdo. Para ello, supongamos que \(f\) es monótona. Entonces, como \(a ≤ b\), se tiene \(f(a) ≤ f(b)\) y, por el lema L1, \(f(b) ≮ f(a)\), en contradicción con la hipótesis.
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 |
import Mathlib.Data.Real.Basic variable (f : ℝ → ℝ) variable (a b : ℝ) -- 1ª demostración -- =============== example (h1 : a ≤ b) (h2 : f b < f a) : ¬ Monotone f := by intro h3 -- h3 : Monotone f -- ⊢ False have h4 : f a ≤ f b := h3 h1 have h5 : ¬(f b < f a) := not_lt_of_ge h4 exact h5 h2 -- 2ª demostración -- =============== example (h1 : a ≤ b) (h2 : f b < f a) : ¬ Monotone f := by intro h3 -- h3 : Monotone f -- ⊢ False have h5 : ¬(f b < f a) := not_lt_of_ge (h3 h1) exact h5 h2 -- 3ª demostración -- =============== example (h1 : a ≤ b) (h2 : f b < f a) : ¬ Monotone f := by intro h3 -- h3 : Monotone f -- ⊢ False exact (not_lt_of_ge (h3 h1)) h2 -- 4ª demostración -- =============== example (h1 : a ≤ b) (h2 : f b < f a) : ¬ Monotone f := fun h3 ↦ (not_lt_of_ge (h3 h1)) h2 -- Lemas usados -- ============ -- #check (not_lt_of_ge : a ≥ b → ¬a < b) |
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. No para toda f : ℝ → ℝ monótona, (∀a,b)[f(a) ≤ f(b) → a ≤ b]
Demostrar con Lean4 que no para toda \(f : ℝ → ℝ\) monótona, \((∀a,b)[f(a) ≤ f(b) → a ≤ b]\).
Para ello, completar la siguiente teoría de Lean4:
|
1 2 3 4 5 |
import Mathlib.Data.Real.Basic example : ¬∀ {f : ℝ → ℝ}, Monotone f → ∀ {a b}, f a ≤ f b → a ≤ b := by sorry |
Demostración en lenguaje natural
Supongamos que
\[ (∀f)[f \text{ es monótona } → (∀a, b)[f(a) ≤ f(b) → a ≤ b]] \tag{1} \]
Sea \(f : ℝ → ℝ\) la función constante igual a cero; es decir,
\[ (∀x ∈ ℝ)[f(x) = 0] \]
Entonces, \(f\) es monótona y \(f(1) ≤ f(0)\) (ya que \(f(1) = 0 ≤ 0 = f(0)\)). Luego, por (1), \(1 ≤ 0\) que es una contradicción.
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 |
import Mathlib.Data.Real.Basic -- 1ª demostración -- =============== example : ¬∀ {f : ℝ → ℝ}, Monotone f → ∀ {a b}, f a ≤ f b → a ≤ b := by intro h1 -- h1 : ∀ {f : ℝ → ℝ}, Monotone f → ∀ {a b : ℝ}, f a ≤ f b → a ≤ b -- ⊢ False let f := fun _ : ℝ ↦ (0 : ℝ) have h2 : Monotone f := monotone_const have h3 : f 1 ≤ f 0 := le_refl 0 have h4 : 1 ≤ 0 := h1 h2 h3 linarith -- Lemas usados -- ============ -- variable (a c : ℝ) -- #check (le_refl a : a ≤ a) -- #check (monotone_const : Monotone fun _ : ℝ ↦ 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.
5. Si (∀ε > 0)[x ≤ ε], entonces x ≤ 0
Demostrar con Lean4 que si \((∀ε > 0)[x ≤ ε]\), entonces \(x ≤ 0\).
Para ello, completar la siguiente teoría de Lean4:
|
1 2 3 4 5 6 7 |
import Mathlib.Data.Real.Basic variable (x : ℝ) example (h : ∀ ε > 0, x ≤ ε) : x ≤ 0 := by sorry |
Demostración en lenguaje natural
Basta demostrar que \(x ≯ 0\). Para ello, supongamos que \(x > 0\) y vamos a demostrar que
\[ ¬(∀ε)[ε > 0 → x ≤ ε] \tag{1} \]
que es una contradicción con la hipótesis. Interiorizando la negación, (1) es equivalente a
\[ (∃ε)[ε > 0 ∧ ε < x] \tag{2} \]
Para demostrar (2), elegimos \(ε = \dfrac{x}{2}\) ya que, como \(x > 0\), se tiene
\[ 0 < \dfrac{x}{2} < 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 |
import Mathlib.Data.Real.Basic variable (x : ℝ) -- 1ª demostración -- =============== example (h : ∀ ε > 0, x ≤ ε) : x ≤ 0 := by apply le_of_not_gt -- ⊢ ¬x > 0 intro hx0 -- hx0 : x > 0 -- ⊢ False apply absurd h -- ⊢ ¬∀ (ε : ℝ), ε > 0 → x ≤ ε push_neg -- ⊢ ∃ ε, ε > 0 ∧ ε < x use x /2 -- ⊢ x / 2 > 0 ∧ x / 2 < x constructor { show x / 2 > 0 exact half_pos hx0 } { show x / 2 < x exact half_lt_self hx0 } -- 2ª demostración -- =============== example (x : ℝ) (h : ∀ ε > 0, x ≤ ε) : x ≤ 0 := by contrapose! h -- ⊢ ∃ ε, ε > 0 ∧ ε < x use x / 2 -- ⊢ x / 2 > 0 ∧ x / 2 < x constructor { show x / 2 > 0 exact half_pos h } { show x / 2 < x exact half_lt_self h } -- Lemas usados -- ============ -- variable (a b : ℝ) -- variable (p q : Prop) -- #check (le_of_not_gt : ¬a > b → a ≤ b) -- #check (half_lt_self : 0 < a → a / 2 < a) -- #check (half_pos : 0 < a → 0 < a / 2) -- #check (absurd : p → ¬p → q) |
Demostraciones interactivas
Se puede interactuar con las demostraciones anteriores en Lean 4 Web.
Referencias
- J. Avigad y P. Massot. Mathematics in Lean, p. 32.