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 los productos de los números naturales por números pares son pares.
Para ello, completar la siguiente teoría de Lean:
|
1 2 3 4 5 6 7 8 |
import Mathlib.Data.Nat.Basic import Mathlib.Data.Nat.Parity import Mathlib.Tactic open Nat example : ∀ m n : ℕ, Even n → Even (m * n) := by sorry |
Demostración en lenguaje natural
Si \(n\) es par, entonces (por la definición de Even) existe un \(k\) tal que
\[
\begin{align*}
n = k + k && (1)
\end{align*}
\]
Por tanto,
\[
\begin{align*}
mn &= m(k + k) && (\text{por (1)})\\
&= mk + mk && (\text{por la propiedad distributiva})
\end{align*}
\]
Por consiguiente, \(mn\) es par.
Soluciones 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 |
import Mathlib.Data.Nat.Basic import Mathlib.Data.Nat.Parity import Mathlib.Tactic open Nat -- 1ª demostración example : ∀ m n : ℕ, Even n → Even (m * n) := by rintro m n ⟨k, hk⟩ use m * k rw [hk] ring -- 2ª demostración example : ∀ m n : ℕ, Even n → Even (m * n) := by rintro m n ⟨k, hk⟩ use m * k rw [hk] rw [mul_add] -- 3ª demostración example : ∀ m n : ℕ, Even n → Even (m * n) := by rintro m n ⟨k, hk⟩ use m * k rw [hk, mul_add] -- 4ª demostración example : ∀ m n : Nat, Even n → Even (m * n) := by rintro m n ⟨k, hk⟩; use m * k; rw [hk, mul_add] -- 5ª demostración example : ∀ m n : ℕ, Even n → Even (m * n) := by rintro m n ⟨k, hk⟩ exact ⟨m * k, by rw [hk, mul_add]⟩ -- 6ª demostración example : ∀ m n : Nat, Even n → Even (m * n) := fun m n ⟨k, hk⟩ ↦ ⟨m * k, by rw [hk, mul_add]⟩ -- 7ª demostración example : ∀ m n : ℕ, Even n → Even (m * n) := by rintro m n ⟨k, hk⟩ use m * k rw [hk] exact mul_add m k k -- 8ª demostración example : ∀ m n : ℕ, Even n → Even (m * n) := by intros m n hn unfold Even at * cases hn with | intro k hk => use m * k rw [hk, mul_add] -- 9ª demostración example : ∀ m n : ℕ, Even n → Even (m * n) := by intros m n hn unfold Even at * cases hn with | intro k hk => use m * k calc m * n = m * (k + k) := by exact congrArg (HMul.hMul m) hk _ = m * k + m * k := by exact mul_add m k k -- 10ª demostración example : ∀ m n : Nat, Even n → Even (m * n) := by intros; simp [*, parity_simps] |
Se puede interactuar con las pruebas anteriores en Lean 4 Web.
Referencias