La semana en Calculemus (30 de septiembre de 2023)
Esta semana he publicado en Calculemus las demostraciones con Lean4 de las siguientes propiedades:
- 1. En los retículos, una distributiva del ínfimo implica la otra
- 2. En los retículos, una distributiva del supremo implica la otra
- 3. En los anillos ordenados, a ≤ b → 0 ≤ b – a
- 4. En los anillos ordenados, 0 ≤ b – a → a ≤ b
- 5. En los anillos ordenados, {a ≤ b, 0 ≤ c} ⊢ ac ≤ bc
A continuación se muestran las soluciones.
1. En los retículos, una distributiva del ínfimo implica la otra
Demostrar con Lean4 que si α es un retículo tal que se
$$(∀ x, y, z) [x ⊓ (y ⊔ z) = (x ⊓ y) ⊔ (x ⊓ z))]$$
entonces
$$(a ⊔ b) ⊓ c = (a ⊓ c) ⊔ (b ⊓ c)$$
para todos los elementos de α.
Para ello, completar la siguiente teoría de Lean4:
|
1 2 3 4 5 6 7 8 |
import Mathlib.Order.Lattice variable {α : Type _} [Lattice α] variable (a b c : α) example (h : ∀ x y z : α, x ⊓ (y ⊔ z) = (x ⊓ y) ⊔ (x ⊓ z)) : (a ⊔ b) ⊓ c = (a ⊓ c) ⊔ (b ⊓ c) := by sorry |
Demostración en lenguaje natural
Se demuestra por la siguiente cadena de igualdades
\begin{align}
(a ⊔ b) ⊓ c &= c ⊓ (a ⊔ b) &&\text{[por conmutatividad de ⊓]} \\
&= (c ⊓ a) ⊔ (c ⊓ b) &&\text{[por la hipótesis]} \\
&= (a ⊓ c) ⊔ (c ⊓ b) &&\text{[por conmutatividad de ⊓]} \\\
&= (a ⊓ c) ⊔ (b ⊓ c) &&\text{[por conmutatividad de ⊓]}
\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 |
import Mathlib.Order.Lattice variable {α : Type _} [Lattice α] variable (a b c : α) -- 1ª demostración example (h : ∀ x y z : α, x ⊓ (y ⊔ z) = (x ⊓ y) ⊔ (x ⊓ z)) : (a ⊔ b) ⊓ c = (a ⊓ c) ⊔ (b ⊓ c) := calc (a ⊔ b) ⊓ c = c ⊓ (a ⊔ b) := by rw [inf_comm] _ = (c ⊓ a) ⊔ (c ⊓ b) := by rw [h] _ = (a ⊓ c) ⊔ (c ⊓ b) := by rw [@inf_comm _ _ c a] _ = (a ⊓ c) ⊔ (b ⊓ c) := by rw [@inf_comm _ _ c b] -- 2ª demostración example (h : ∀ x y z : α, x ⊓ (y ⊔ z) = (x ⊓ y) ⊔ (x ⊓ z)) : (a ⊔ b) ⊓ c = (a ⊓ c) ⊔ (b ⊓ c) := by simp [h, inf_comm] -- Lemas usados -- ============ -- #check (inf_comm : a ⊓ b = b ⊓ a) |
Demostraciones interactivas
Se puede interactuar con las demostraciones anteriores en Lean 4 Web.
Referencias
- J. Avigad y P. Massot. Mathematics in Lean, p. 22.
2. En los retículos, una distributiva del supremo implica la otra
Demostrar con Lean4 que si \(R\) es un retículo tal que
\[ (∀ x,\ y,\ z \in R) [x ⊔ (y ⊓ z) = (x ⊔ y) ⊓ (x ⊔ z)] \]
entonces
\[ (a ⊓ b) ⊔ c = (a ⊔ c) ⊓ (b ⊔ c) \]
para todos los elementos del retículo.
Para ello, completar la siguiente teoría de Lean4:
|
1 2 3 4 5 6 7 8 |
import Mathlib.Order.Lattice variable {α : Type _} [Lattice α] variable (a b c : α) example (h : ∀ x y z : α, x ⊔ (y ⊓ z) = (x ⊔ y) ⊓ (x ⊔ z)) : (a ⊓ b) ⊔ c = (a ⊔ c) ⊓ (b ⊔ c) := by sorry |
Demostración en lenguaje natural
Se demuestra por la siguiente cadena de igualdades
\begin{align}
(a ⊓ b) ⊔ c &= c ⊔ (a ⊓ b) &&\text{[por la conmutatividad de ⊔]} \\
&= (c ⊔ a) ⊓ (c ⊔ b) &&\text{[por la hipótesis]} \\
&= (a ⊔ c) ⊓ (c ⊔ b) &&\text{[por la conmutatividad de ⊔]} \\
&= (a ⊔ c) ⊓ (b ⊔ c) &&\text{[por la conmutatividad de ⊔]}
\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 |
import Mathlib.Order.Lattice variable {α : Type _} [Lattice α] variable (a b c : α) -- 1ª demostración example (h : ∀ x y z : α, x ⊔ (y ⊓ z) = (x ⊔ y) ⊓ (x ⊔ z)) : (a ⊓ b) ⊔ c = (a ⊔ c) ⊓ (b ⊔ c) := calc (a ⊓ b) ⊔ c = c ⊔ (a ⊓ b) := by rw [sup_comm] _ = (c ⊔ a) ⊓ (c ⊔ b) := by rw [h] _ = (a ⊔ c) ⊓ (c ⊔ b) := by rw [@sup_comm _ _ c a] _ = (a ⊔ c) ⊓ (b ⊔ c) := by rw [@sup_comm _ _ c b] -- 2ª demostración example (h : ∀ x y z : α, x ⊔ (y ⊓ z) = (x ⊔ y) ⊓ (x ⊔ z)) : (a ⊓ b) ⊔ c = (a ⊔ c) ⊓ (b ⊔ c) := by simp [h, sup_comm] -- Lemas usados -- ============ -- #check (sup_comm : a ⊔ b = b ⊔ a) |
Demostraciones interactivas
Se puede interactuar con las demostraciones anteriores en Lean 4 Web.
Referencias
- J. Avigad y P. Massot. Mathematics in Lean, p. 22.
3. En los anillos ordenados, a ≤ b → 0 ≤ b – a
Demostrar con Lean4 que en los anillos ordenados se verifica que
\[ a ≤ b → 0 ≤ b – a \]
Para ello, completar la siguiente teoría de Lean4:
|
1 2 3 4 5 6 |
import Mathlib.Algebra.Order.Ring.Defs variable {R : Type _} [StrictOrderedRing R] variable (a b c : R) example : a ≤ b → 0 ≤ b - a := by sorry |
Demostración en lenguaje natural
Se usarán los siguientes lemas:
\begin{align}
&a – a = 0 \tag{L1} \\
&a ≤ b → (∀ c) [a – c ≤ b – c] \tag{L2}
\end{align}
Supongamos que
\[ a ≤ b \tag{1} \]
La demostración se tiene por la siguiente cadena de desigualdades:
\begin{align}
0 &= a – a &&\text{[por L1]} \\
&≤ b – a &&\text{[por (1) y L2]}
\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 |
import Mathlib.Algebra.Order.Ring.Defs variable {R : Type _} [StrictOrderedRing R] variable (a b c : R) -- 1ª demostración example : a ≤ b → 0 ≤ b - a := by intro h calc 0 = a - a := (sub_self a).symm _ ≤ b - a := sub_le_sub_right h a -- 2ª demostración example : a ≤ b → 0 ≤ b - a := sub_nonneg.mpr -- 3ª demostración example : a ≤ b → 0 ≤ b - a := by simp -- Lemas usados -- ============ -- #check (sub_le_sub_right : a ≤ b → ∀ (c : R), a - c ≤ b - c) -- #check (sub_nonneg : 0 ≤ a - b ↔ b ≤ a) -- #check (sub_self a : a - a = 0) |
Demostraciones interactivas
Se puede interactuar con las demostraciones anteriores en Lean 4 Web.
Referencias
- J. Avigad y P. Massot. Mathematics in Lean, p. 22.
4. En los anillos ordenados, 0 ≤ b – a → a ≤ b
Demostrar con Lean4 que en los anillos ordenados
\[ 0 ≤ b – a → a ≤ b \]
Para ello, completar la siguiente teoría de Lean4:
|
1 2 3 4 5 6 |
import Mathlib.Algebra.Order.Ring.Defs variable {R : Type _} [StrictOrderedRing R] variable (a b c : R) example : 0 ≤ b - a → a ≤ b := by sorry |
Demostración en lenguaje natural
Se usarán los siguientes lemas:
\begin{align}
&0 + a = a \tag{L1} \\
&b ≤ c → (∀ a) [b + a ≤ c + a] \tag{L2} \\
&a – b + b = -a \tag{L3}
\end{align}
Supongamos que
\[ 0 ≤ b – a \tag{1} \]
La demostración se tiene por la siguiente cadena de desigualdades:
\begin{align}
a &= 0 + a &&\text{[por L1]} \\
&≤ (b – a) + a &&\text{[por (1) y L2]} \\
&= b &&\text{[por L3]}
\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 |
import Mathlib.Algebra.Order.Ring.Defs variable {R : Type _} [StrictOrderedRing R] variable (a b c : R) -- 1ª demostración -- =============== example : 0 ≤ b - a → a ≤ b := by intro h calc a = 0 + a := (zero_add a).symm _ ≤ (b - a) + a := add_le_add_right h a _ = b := sub_add_cancel b a -- 2ª demostración -- =============== example : 0 ≤ b - a → a ≤ b := -- by apply? sub_nonneg.mp -- 3ª demostración -- =============== example : 0 ≤ b - a → a ≤ b := by simp -- Lemas usados -- ============ -- #check (zero_add a : 0 + a = a) -- #check (add_le_add_right : b ≤ c → ∀ (a : R), b + a ≤ c + a) -- #check (sub_add_cancel a b : a - b + b = a) -- #check (sub_nonneg : 0 ≤ a - b ↔ b ≤ a) |
Demostraciones interactivas
Se puede interactuar con las demostraciones anteriores en Lean 4 Web.
Referencias
- J. Avigad y P. Massot. Mathematics in Lean, p. 22.
5. En los anillos ordenados, {a ≤ b, 0 ≤ c} ⊢ ac ≤ bc
Demostrar con Lean4 que, en los anillos ordenados,
\[ \{a ≤ b, 0 ≤ c\} ⊢ ac ≤ bc \]
Para ello, completar la siguiente teoría de Lean4:
|
1 2 3 4 5 6 7 8 9 |
import Mathlib.Algebra.Order.Ring.Defs variable {R : Type _} [StrictOrderedRing R] variable (a b c : R) example (h1 : a ≤ b) (h2 : 0 ≤ c) : a * c ≤ b * c := by sorry |
Demostración en lenguaje natural
Se usarán los siguientes lemas:
\begin{align}
&0 ≤ a – b ↔ b ≤ a \tag{L1} \\
&0 ≤ a → 0 ≤ b → 0 ≤ ab \tag{L2} \\
&(a – b)c = ac – bc \tag{L3}
\end{align}
Supongamos que
\begin{align}
a &≤ b \tag{1} \\
0 &≤ c
\end{align}
De (1), por L1, se tiene
\[ 0 ≤ b – a \]
y con (2), por L2, se tiene
\[ 0 ≤ (b – a)c \]
que, por L3, da
\[ 0 ≤ bc – ac \]
y, aplicándole L1, se tiene
\[ ac ≤ bc \]
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.Algebra.Order.Ring.Defs variable {R : Type _} [StrictOrderedRing R] variable (a b c : R) -- 1ª demostración -- =============== example (h1 : a ≤ b) (h2 : 0 ≤ c) : a * c ≤ b * c := by have h3 : 0 ≤ b - a := sub_nonneg.mpr h1 have h4 : 0 ≤ b * c - a * c := calc 0 ≤ (b - a) * c := mul_nonneg h3 h2 _ = b * c - a * c := sub_mul b a c show a * c ≤ b * c exact sub_nonneg.mp h4 -- 2ª demostración -- =============== example (h1 : a ≤ b) (h2 : 0 ≤ c) : a * c ≤ b * c := by have h3 : 0 ≤ b - a := sub_nonneg.mpr h1 have h4 : 0 ≤ (b - a) * c := mul_nonneg h3 h2 -- h4 : 0 ≤ b * c - a * c rw [sub_mul] at h4 -- a * c ≤ b * c exact sub_nonneg.mp h4 -- 3ª demostración -- =============== example (h1 : a ≤ b) (h2 : 0 ≤ c) : a * c ≤ b * c := by -- 0 ≤ b * c - a * c apply sub_nonneg.mp -- 0 ≤ (b - a) * c rw [← sub_mul] apply mul_nonneg . -- 0 ≤ b - a exact sub_nonneg.mpr h1 . -- 0 ≤ c exact h2 -- 4ª demostración -- =============== example (h1 : a ≤ b) (h2 : 0 ≤ c) : a * c ≤ b * c := by apply sub_nonneg.mp rw [← sub_mul] apply mul_nonneg (sub_nonneg.mpr h1) h2 -- 5ª demostración example (h1 : a ≤ b) (h2 : 0 ≤ c) : a * c ≤ b * c := -- by apply? mul_le_mul_of_nonneg_right h1 h2 -- Lemas usados -- ============ -- #check (mul_le_mul_of_nonneg_right : a ≤ b → 0 ≤ c → a * c ≤ b * c) -- #check (mul_nonneg : 0 ≤ a → 0 ≤ b → 0 ≤ a * b) -- #check (sub_mul a b c : (a - b) * c = a * c - b * c) -- #check (sub_nonneg : 0 ≤ a - b ↔ b ≤ a) |
Demostraciones interactivas
Se puede interactuar con las demostraciones anteriores en Lean 4 Web.
Referencias
- J. Avigad y P. Massot. Mathematics in Lean, p. 22.