La semana en Calculemus (28 de octubre de 2023)
Esta semana he publicado en Calculemus las demostraciones con Lean4 de las siguientes propiedades:
- 1. Si a es una cota superior de s y a ≤ b, entonces b es una cota superior de s
- 2. La función (x ↦ x + c) es inyectiva
- 3. Si c ≠ 0, entonces la función (x ↦ cx) es inyectiva
- 4. La composición de funciones inyectivas es inyectiva
- 5. Hay algún número real entre 2 y 3
A continuación se muestran las soluciones.
1. Si a es una cota superior de s y a ≤ b, entonces b es una cota superior de s
Demostrar con Lean4 que si \(a\) es una cota superior de \(s\) y \(a ≤ b\), entonces \(b\) es una cota superior de \(s\).
Para ello, completar la siguiente teoría de Lean4:
|
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 |
import Mathlib.Tactic variable {α : Type _} [PartialOrder α] variable (s : Set α) variable (a b : α) -- (CotaSupConj s a) afirma que a es una cota superior del conjunto s. def CotaSupConj (s : Set α) (a : α) := ∀ {x}, x ∈ s → x ≤ a example (h1 : CotaSupConj s a) (h2 : a ≤ b) : CotaSupConj s b := by sorry |
Demostración en lenguaje natural
Tenemos que demostrar que
\[ (∀ x) [x ∈ s → x ≤ b] \]
Sea \(x\) tal que \(x ∈ s\). Entonces,
\begin{align}
x &≤ a &&\text{[porque \(a\) es una cota superior de \(s\)]} \\
&≤ b
\end{align}
Por tanto, \(x ≤ b\).
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 |
import Mathlib.Tactic variable {α : Type _} [PartialOrder α] variable (s : Set α) variable (a b : α) -- (CotaSupConj s a) afirma que a es una cota superior del conjunto s. def CotaSupConj (s : Set α) (a : α) := ∀ {x}, x ∈ s → x ≤ a -- 1ª demostración example (h1 : CotaSupConj s a) (h2 : a ≤ b) : CotaSupConj s b := by intro x (xs : x ∈ s) have h3 : x ≤ a := h1 xs show x ≤ b exact le_trans h3 h2 -- 2ª demostración example (h1 : CotaSupConj s a) (h2 : a ≤ b) : CotaSupConj s b := by intro x (xs : x ∈ s) calc x ≤ a := h1 xs _ ≤ b := h2 - -- Lemas usados -- ============ -- variable (c : α) -- #check (le_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. 27.
2. La función (x ↦ x + c) es inyectiva
Demostrar con Lean4 que la función \(x ↦ x + c\) es inyectiva.
Para ello, completar la siguiente teoría de Lean4:
|
1 2 3 4 5 6 7 |
import Mathlib.Data.Real.Basic open Function variable {c : ℝ} example : Injective ((. + c)) := by sorry |
Demostración en lenguaje natural
Se usará el lema
\[ (∀ a, b, c) [a + b = c + b → a = c] \tag{L1} \]
Hay que demostrar que
\[ (∀ x₁, x₂) [f(x₁) = f(x₂) → x₁ = x₂] \]
Sean \(x₁, x₂\) tales que \(f(x₁) = f(x₂)\). Entonces,
\[ x₁ + c = x₂ + c \]
y, por L1, \(x₁ = 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 |
import Mathlib.Data.Real.Basic open Function variable {c : ℝ} -- 1ª demostración example : Injective ((. + c)) := by intro (x1 : ℝ) (x2 : ℝ) (h1 : x1 + c = x2 + c) show x1 = x2 exact add_right_cancel h1 -- 2ª demostración example : Injective ((. + c)) := by intro x1 x2 h1 show x1 = x2 exact add_right_cancel h1 -- 3ª demostración example : Injective ((. + c)) := fun _ _ h ↦ add_right_cancel h -- Lemas usados -- ============ -- variable {a b : ℝ} -- #check (add_right_cancel : a + b = c + b → 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. 28.
3. Si c ≠ 0, entonces la función (x ↦ cx) es inyectiva
Demostrar con Lean4 que si \(c ≠ 0\), entonces la función \(x ↦ cx\) es inyectiva.
Para ello, completar la siguiente teoría de Lean4:
|
1 2 3 4 5 6 7 8 |
import Mathlib.Data.Real.Basic open Function variable {c : ℝ} example (h : c ≠ 0) : Injective ((c * .)) := by sorry |
Demostración en lenguaje natural
Se usará el lema
\[ (∀ a, b, c) [a ≠ 0 → (ab = ac ↔ b = c))] \tag{L1} \]
Hay que demostrar que
\[ (∀ x₁, x₂) [f(x₁) = f(x₂) → x₁ = x₂] \]
Sean \(x₁, x₂\) tales que \(f(x₁) = f(x₂)\). Entonces,
\[ cx₁ = cx₂ \]
y, por L1 y puesto que \(c ≠ 0\), se tiene que
\[ x₁ = 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 |
import Mathlib.Data.Real.Basic open Function variable {c : ℝ} -- 1ª demostración example (h : c ≠ 0) : Injective ((c * .)) := by intro (x1 : ℝ) (x2 : ℝ) (h1 : c * x1 = c * x2) show x1 = x2 exact (mul_right_inj' h).mp h1 -- 2ª demostración example (h : c ≠ 0) : Injective ((c * .)) := fun _ _ h1 ↦ mul_left_cancel₀ h h1 -- Lemas usados -- ============ -- variable (a b : ℝ) -- #check (mul_right_inj' : a ≠ 0 → (a * b = a * c ↔ b = c)) -- #check (mul_left_cancel₀ : a ≠ 0 → a * b = a * c → b = c) |
Demostraciones interactivas
Se puede interactuar con las demostraciones anteriores en Lean 4 Web.
Referencias
- J. Avigad y P. Massot. Mathematics in Lean, p. 28.
4. La composición de funciones inyectivas es inyectiva
Demostrar con Lean4 que la composición de funciones inyectivas es inyectiva.
Para ello, completar la siguiente teoría de Lean4:
|
1 2 3 4 5 6 7 8 9 10 11 12 |
import Mathlib.Tactic open Function variable {α : Type _} {β : Type _} {γ : Type _} variable {f : α → β} {g : β → γ} example (hg : Injective g) (hf : Injective f) : Injective (g ∘ f) := by sorry |
Demostraciones en lenguaje natural (LN)
1ª demostración en LN
Tenemos que demostrar que
\[ (∀ x, y) [(g ∘ f)(x) = (g ∘ f)(y) → x = y] \]
Sean \(x, y\) tales que
\[ (g ∘ f)(x) = (g ∘ f)(y) \]
Entonces, por la definición de la composición,
\[ g(f(x)) = g(f(y)) \]
y, ser \(g\) inyectiva,
\[ f(x) = f(y) \]
y, ser \(f\) inyectiva,
\[ x = y \]
2ª demostración en LN
Tenemos que demostrar que
\[ (∀ x, y) [(g ∘ f)(x) = (g ∘ f)(y) → x = y] \]
Sean \(x, y\) tales que
\[ (g ∘ f)(x) = (g ∘ f)(y) \tag{1} \]
y tenemos que demostrar que
\[ x = y \tag{2} \]
El objetivo (2), usando que \(f\) es inyectiva, se reduce a
\[ f(x) = f(y) \]
que, usando que \(g\) es inyectiva, se reduce a
\[ g(f(x)) = g(f(y)) \]
que, por la definición de la composición, coincide con (1).
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 |
import Mathlib.Tactic open Function variable {α : Type _} {β : Type _} {γ : Type _} variable {f : α → β} {g : β → γ} -- 1ª demostración (basada en la 1ª en LN) example (hg : Injective g) (hf : Injective f) : Injective (g ∘ f) := by intro (x : α) (y : α) (h1: (g ∘ f) x = (g ∘ f) y) have h2: g (f x) = g (f y) := h1 have h3: f x = f y := hg h2 show x = y exact hf h3 -- 2ª demostración example (hg : Injective g) (hf : Injective f) : Injective (g ∘ f) := by intro (x : α) (y : α) (h1: (g ∘ f) x = (g ∘ f) y) have h2: f x = f y := hg h1 show x = y exact hf h2 -- 3ª demostración example (hg : Injective g) (hf : Injective f) : Injective (g ∘ f) := by intro x y h exact hf (hg h) -- 4ª demostración example (hg : Injective g) (hf : Injective f) : Injective (g ∘ f) := fun _ _ h ↦ hf (hg h) -- 5ª demostración (basada en la 2ª en LN) example (hg : Injective g) (hf : Injective f) : Injective (g ∘ f) := by intros x y h -- x y : α -- h : (g ∘ f) x = (g ∘ f) y apply hf -- ⊢ f x = f y apply hg -- ⊢ g (f x) = g (f y) apply h -- 6ª demostración example (hg : Injective g) (hf : Injective f) : Injective (g ∘ f) := -- by exact? Injective.comp hg hf -- 7ª demostración example (hg : Injective g) (hf : Injective f) : Injective (g ∘ f) := by tauto -- Lemas usados -- ============ -- #check (Injective.comp : Injective g → Injective f → Injective (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. 28.
5. Hay algún número real entre 2 y 3
Demostrar con Lean4 que hay algún número real entre 2 y 3.
Para ello, completar la siguiente teoría de Lean4:
|
1 2 3 4 |
import Mathlib.Data.Real.Basic example : ∃ x : ℝ, 2 < x ∧ x < 3 := by sorry |
Demostración en lenguaje natural
Puesto que \(2 < 5/2 < 3\), basta elegir \(5/2\).
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.Data.Real.Basic -- 1ª demostración example : ∃ x : ℝ, 2 < x ∧ x < 3 := by have h : 2 < (5 : ℝ) / 2 ∧ (5 : ℝ) / 2 < 3 := by norm_num show ∃ x : ℝ, 2 < x ∧ x < 3 exact Exists.intro (5 / 2) h -- 2ª demostración example : ∃ x : ℝ, 2 < x ∧ x < 3 := by have h : 2 < (5 : ℝ) / 2 ∧ (5 : ℝ) / 2 < 3 := by norm_num show ∃ x : ℝ, 2 < x ∧ x < 3 exact ⟨5 / 2, h⟩ -- 3ª demostración example : ∃ x : ℝ, 2 < x ∧ x < 3 := by use 5 / 2 norm_num -- 4ª demostración example : ∃ x : ℝ, 2 < x ∧ x < 3 := ⟨5 / 2, by 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. 28.