Demostrar con Lean4 que si a, b, c y d son números reales tales
|
1 2 |
c = b * a - d d = a * b |
entonces
|
1 |
c = 0 |
Para ello, completar la siguiente teoría de Lean4:
|
1 2 3 4 5 6 7 8 9 |
import Mathlib.Data.Real.Basic import Mathlib.Tactic example (a b c d : ℝ) (h1 : c = b * a - d) (h2 : d = a * b) : c = 0 := by sorry |
Demostrar con Lean4 que si bc = ef, entonces ((ab)c)d = ((ae)f)d.
Para ello, completar la siguiente teoría de Lean4:
|
1 2 3 4 5 6 7 8 |
import Mathlib.Data.Real.Basic import Mathlib.Tactic example (a b c d e f : ℝ) (h : b * c = e * f) : ((a * b) * c) * d = ((a * e) * f) * d := by sorry |
Demostrar con Lean4 que si ab = cd y e = f, entonces a(be) = c(df)
Para ello, completar la siguiente teoría de Lean4:
|
1 2 3 4 5 6 7 8 9 |
import Mathlib.Tactic import Mathlib.Data.Real.Basic example (a b c d e f : ℝ) (h1 : a * b = c * d) (h2 : e = f) : a * (b * e) = c * (d * f) := by sorry |
Demostrar con Lean4 que ∀ a b c ∈ ℝ, a * (b * c) = b * (a * c)
Para ello, completar la siguiente teoría de Lean4:
|
1 2 3 4 5 6 |
import Mathlib.Tactic import Mathlib.Data.Real.Basic example (a b c : ℝ) : a * (b * c) = b * (a * c) := by sorry |
Demostrar con Lean4 que los números reales tienen la siguiente propiedad
|
1 |
(c * b) * a = b * (a * c) |
Para ello, completar la siguiente teoría de Lean:
|
1 2 3 4 5 |
import Mathlib.Tactic import Mathlib.Data.Real.Basic example (a b c : ℝ) : (c * b) * a = b * (a * c) := by sorry |
Demostración en lenguaje natural
Por la siguiente cadena de igualdades:
\begin{align}
(cb)a
&= (bc)a &&\text{[por la conmutativa]} \\
&= b(ca) &&\text{[por la asociativa]} \\
&= b(ac) &&\text{[por la conmutativa]}
\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 |
import Mathlib.Tactic import Mathlib.Data.Real.Basic -- 1ª demostración example (a b c : ℝ) : (c * b) * a = b * (a * c) := calc (c * b) * a = (b * c) * a := by rw [mul_comm c b] _ = b * (c * a) := by rw [mul_assoc] _ = b * (a * c) := by rw [mul_comm c a] -- 2ª demostración example (a b c : ℝ) : (c * b) * a = b * (a * c) := by rw [mul_comm c b] rw [mul_assoc] rw [mul_comm c a] -- 3ª demostración example (a b c : ℝ) : (c * b) * a = b * (a * c) := by ring |
Demostraciones interactivas
Se puede interactuar con las demostraciones anteriores en Lean 4 Web.
Referencias
Demostrar con Lean4 que los números reales tienen la siguiente propiedad
|
1 |
(a * b) * c = b * (a * c) |
Para ello, completar la siguiente teoría de Lean4:
|
1 2 3 4 5 |
import Mathlib.Tactic import Mathlib.Data.Real.Basic example (a b c : ℝ) : (a * b) * c = b * (a * c) := by sorry |
Demostración en lenguaje natural
Por la siguiente cadena de igualdades
\begin{align*}
(ab)c &= (ba)c &&\text{[por la conmutativa]} \\
&= b(ac) &&\text{[por la asociativa]}
\end{align*}
Demostraciones con Lean4
|
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 |
import Mathlib.Tactic import Mathlib.Data.Real.Basic -- 1ª demostración example (a b c : ℝ) : (a * b) * c = b * (a * c) := calc (a * b) * c = (b * a) * c := by rw [mul_comm a b] _ = b * (a * c) := by rw [mul_assoc b a c] -- 2ª demostración example (a b c : ℝ) : (a * b) * c = b * (a * c) := by rw [mul_comm a b] rw [mul_assoc b a c] -- 3ª demostración example (a b c : ℝ) : (a * b) * c = b * (a * c) := by ring |
Demostraciones interactivas
Se puede interactuar con las demostraciones anteriores en Lean 4 Web.
Referencias
Demostrar que si a divide a b y a c, entonces también divide a b + c.
Para ello, completar la siguiente teoría de Lean:
|
1 2 3 4 5 6 7 8 9 |
import tactic variables {a b c : ℕ} example (divab : a ∣ b) (divac : a ∣ c) : a ∣ (b + c) := sorry |
Read More «Si a divide a b y a c, entonces también divide a b + c»
Demostrar que la relación de divisibilidad es transitiva.
Para ello, completar la siguiente teoría de Lean:
|
1 2 3 4 5 6 7 8 9 |
import tactic variables {a b c : ℕ} example (hab : a ∣ b) (hbc : b ∣ c) : a ∣ c := sorry |
Demostrar que si x e y son sumas de dos cuadrados, entonces xy también lo es.
Para ello, completar la siguiente teoría de Lean:
|
1 2 3 4 5 6 7 8 9 10 11 12 13 |
import tactic variables {α : Type*} [comm_ring α] variables {x y : α} -- (es_suma_de_cuadrados x) se verifica si x se puede escribir como la -- suma de dos cuadrados. def es_suma_de_cuadrados (x : α) := ∃ a b, x = a^2 + b^2 example (hx : es_suma_de_cuadrados x) (hy : es_suma_de_cuadrados y) : es_suma_de_cuadrados (x * y) := sorry |
Read More «Si x e y son sumas de dos cuadrados, entonces xy también lo es»
Demostrar que si c ≥ 0 y f está acotada superiormente, entonces c * f también lo está.
Para ello, completar la siguiente teoría de Lean:
|
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 |
import data.real.basic variables {f : ℝ → ℝ} variables {a c : ℝ} -- (cota_superior f a) se verifica si a es una cota superior de f. def cota_superior (f : ℝ → ℝ) (a : ℝ) : Prop := ∀ x, f x ≤ a -- (acotada_sup f) se verifica si f tiene cota superior. def acotada_sup (f : ℝ → ℝ) := ∃ a, cota_superior f a example (hf : acotada_sup f) (h : c ≥ 0) : acotada_sup (λ x, c * f x) := sorry |
Read More «Si c ≥ 0 y f está acotada superiormente, entonces c * f también lo está»