La semana en Calculemus (26 de agosto de 2023)

Esta semana he publicado en Calculemus las demostraciones con Lean4 de las siguientes propiedades:

1. Si G es un grupo y a, b ∈ G, tales que ab = 1 entonces a⁻¹ = b
2. Si G es un grupo y a, b ∈ G, entonces (ab)⁻¹ = b⁻¹a⁻¹
3. En ℝ, si a ≤ b, b < c, c ≤ d y d < e, entonces a < e
4. En ℝ, si 2a ≤ 3b, 1 ≤ a y c = 2, entonces c + a ≤ 5b
5. En ℝ, si 1 ≤ a y b ≤ d, entonces 2 + a + eᵇ ≤ 3a + eᵈ

A continuación se muestran las soluciones.

1. Si G es un grupo y a, b ∈ G, tales que ab = 1 entonces a⁻¹ = b

Demostrar con Lean4 que si \(G\) es un grupo y \(a, b \in G\) tales que \(ab = 1\) entonces \(a^{-1} = b\).

Para ello, completar la siguiente teoría de Lean4:

import Mathlib.Algebra.Group.Defs

variable {G : Type _} [Group G]
variable (a b : G)

example
  (h : a * b = 1)
  : a⁻¹ = b :=
sorry

import Mathlib.Algebra.Group.Defs

variable {G : Type _} [Group G]

variable (a b : G)

example

(h : a * b = 1)

: a⁻¹ = b :=

sorry

Demostración en lenguaje natural

Se tiene a partir de la siguente cadena de igualdades
\begin{align}
a⁻¹ &= a⁻¹·1 &&\text{[por producto por uno]} \\
&= a⁻¹·(a·b) &&\text{[por hipótesis]} \\
&= (a⁻¹·a)·b &&\text{[por asociativa]} \\
&= 1·b &&\text{[por producto con inverso]} \\
&= b &&\text{[por producto por uno]}
\end{align}

Demostraciones con Lean4

import Mathlib.Algebra.Group.Defs

variable {G : Type _} [Group G]
variable (a b : G)

-- 1º demostración
example
  (h : a * b = 1)
  : a⁻¹ = b :=
calc
  a⁻¹ = a⁻¹ * 1       := by rw [mul_one]
    _ = a⁻¹ * (a * b) := by rw [h]
    _ = (a⁻¹ * a) * b := by rw [mul_assoc]
    _ = 1 * b         := by rw [mul_left_inv]
    _ = b             := by rw [one_mul]

-- 2º demostración
example
  (h : a * b = 1)
  : a⁻¹ = b :=
calc
  a⁻¹ = a⁻¹ * 1       := by simp
    _ = a⁻¹ * (a * b) := by simp [h]
    _ = (a⁻¹ * a) * b := by simp
    _ = 1 * b         := by simp
    _ = b             := by simp

-- 3º demostración
example
  (h : a * b = 1)
  : a⁻¹ = b :=
calc
  a⁻¹ =  a⁻¹ * (a * b) := by simp [h]
    _ =  b             := by simp

-- 4º demostración
example
  (h : a * b = 1)
  : a⁻¹ = b :=
by exact inv_eq_of_mul_eq_one_right h

import Mathlib.Algebra.Group.Defs

variable {G : Type _} [Group G]

variable (a b : G)

-- 1º demostración

example

(h : a * b = 1)

: a⁻¹ = b :=

calc

a⁻¹ = a⁻¹ * 1 := by rw [mul_one]

_ = a⁻¹ * (a * b) := by rw [h]

_ = (a⁻¹ * a) * b := by rw [mul_assoc]

_ = 1 * b := by rw [mul_left_inv]

_ = b := by rw [one_mul]

-- 2º demostración

example

(h : a * b = 1)

: a⁻¹ = b :=

calc

a⁻¹ = a⁻¹ * 1 := by simp

_ = a⁻¹ * (a * b) := by simp [h]

_ = (a⁻¹ * a) * b := by simp

_ = 1 * b := by simp

_ = b := by simp

-- 3º demostración

example

(h : a * b = 1)

: a⁻¹ = b :=

calc

a⁻¹ = a⁻¹ * (a * b) := by simp [h]

_ = b := by simp

-- 4º demostración

example

(h : a * b = 1)

: a⁻¹ = b :=

by exact inv_eq_of_mul_eq_one_right h

Demostraciones interactivas

Se puede interactuar con las demostraciones anteriores en Lean 4 Web.

Referencias

J. Avigad y P. Massot. Mathematics in Lean, p. 12.

2. Si G es un grupo y a, b ∈ G, entonces (ab)⁻¹ = b⁻¹a⁻¹

Demostrar con Lean4 que si \(G\) es un grupo y \(a, b \in G\), entonces \((ab)^{-1} = b^{-1}a^{-1}\).

Para ello, completar la siguiente teoría de Lean4:

import Mathlib.Algebra.Group.Defs

variable {G : Type _} [Group G]
variable (a b : G)

example : (a * b)⁻¹ = b⁻¹ * a⁻¹ :=
sorry

import Mathlib.Algebra.Group.Defs

variable {G : Type _} [Group G]

variable (a b : G)

example : (a * b)⁻¹ = b⁻¹ * a⁻¹ :=

sorry

Demostración en lenguaje natural

Teniendo en cuenta la propiedad
\[∀ a\ b ∈ R, ab = 1 → a⁻¹ = b,\]
basta demostrar que
\[(a·b)·(b⁻¹·a⁻¹) = 1.\]
La identidad anterior se demuestra mediante la siguiente cadena de igualdades
\begin{align}
(a·b)·(b⁻¹·a⁻¹) &= a·(b·(b⁻¹·a⁻¹)) &&\text{[por la asociativa]} \\
&= a·((b·b⁻¹)·a⁻¹) &&\text{[por la asociativa]} \\
&= a·(1·a⁻¹) &&\text{[por producto con inverso]} \\
&= a·a⁻¹ &&\text{[por producto con uno]} \\
&= 1 &&\text{[por producto con
inverso]}
\end{align}

Demostraciones con Lean4

import Mathlib.Algebra.Group.Defs

variable {G : Type _} [Group G]
variable (a b : G)

lemma aux : (a * b) * (b⁻¹ * a⁻¹) = 1 :=
calc
  (a * b) * (b⁻¹ * a⁻¹)
    = a * (b * (b⁻¹ * a⁻¹)) := by rw [mul_assoc]
  _ = a * ((b * b⁻¹) * a⁻¹) := by rw [mul_assoc]
  _ = a * (1 * a⁻¹)         := by rw [mul_right_inv]
  _ = a * a⁻¹               := by rw [one_mul]
  _ = 1                     := by rw [mul_right_inv]

-- 1ª demostración
example : (a * b)⁻¹ = b⁻¹ * a⁻¹ :=
by
  have h1 : (a * b) * (b⁻¹ * a⁻¹) = 1 :=
    aux a b
  show (a * b)⁻¹ = b⁻¹ * a⁻¹
  exact inv_eq_of_mul_eq_one_right h1

-- 3ª demostración
example : (a * b)⁻¹ = b⁻¹ * a⁻¹ :=
by
  have h1 : (a * b) * (b⁻¹ * a⁻¹) = 1 :=
    aux a b
  show (a * b)⁻¹ = b⁻¹ * a⁻¹
  simp [h1]

-- 4ª demostración
example : (a * b)⁻¹ = b⁻¹ * a⁻¹ :=
by
  have h1 : (a * b) * (b⁻¹ * a⁻¹) = 1 :=
    aux a b
  simp [h1]

-- 5ª demostración
example : (a * b)⁻¹ = b⁻¹ * a⁻¹ :=
by
  apply inv_eq_of_mul_eq_one_right
  rw [aux]

-- 6ª demostración
example : (a * b)⁻¹ = b⁻¹ * a⁻¹ :=
by exact mul_inv_rev a b

-- 7ª demostración
example : (a * b)⁻¹ = b⁻¹ * a⁻¹ :=
by simp

import Mathlib.Algebra.Group.Defs

variable {G : Type _} [Group G]

variable (a b : G)

lemma aux : (a * b) * (b⁻¹ * a⁻¹) = 1 :=

calc

(a * b) * (b⁻¹ * a⁻¹)

= a * (b * (b⁻¹ * a⁻¹)) := by rw [mul_assoc]

_ = a * ((b * b⁻¹) * a⁻¹) := by rw [mul_assoc]

_ = a * (1 * a⁻¹) := by rw [mul_right_inv]

_ = a * a⁻¹ := by rw [one_mul]

_ = 1 := by rw [mul_right_inv]

-- 1ª demostración

example : (a * b)⁻¹ = b⁻¹ * a⁻¹ :=

have h1 : (a * b) * (b⁻¹ * a⁻¹) = 1 :=

aux a b

show (a * b)⁻¹ = b⁻¹ * a⁻¹

exact inv_eq_of_mul_eq_one_right h1

-- 3ª demostración

example : (a * b)⁻¹ = b⁻¹ * a⁻¹ :=

have h1 : (a * b) * (b⁻¹ * a⁻¹) = 1 :=

aux a b

show (a * b)⁻¹ = b⁻¹ * a⁻¹

simp [h1]

-- 4ª demostración

example : (a * b)⁻¹ = b⁻¹ * a⁻¹ :=

have h1 : (a * b) * (b⁻¹ * a⁻¹) = 1 :=

aux a b

simp [h1]

-- 5ª demostración

example : (a * b)⁻¹ = b⁻¹ * a⁻¹ :=

apply inv_eq_of_mul_eq_one_right

rw [aux]

-- 6ª demostración

example : (a * b)⁻¹ = b⁻¹ * a⁻¹ :=

by exact mul_inv_rev a b

-- 7ª demostración

example : (a * b)⁻¹ = b⁻¹ * a⁻¹ :=

by simp

Demostraciones interactivas

Se puede interactuar con las demostraciones anteriores en Lean 4 Web.

Referencias

J. Avigad y P. Massot. Mathematics in Lean, p. 12.

3. En ℝ, si a ≤ b, b < c, c ≤ d y d < e, entonces a < e

Demostrar con Lean4 que si \(a\), \(b\), \(c\), \(d\) y \(e\) son números reales tales \(a \leq b\), \(b < c\), \(c \leq d\) y \(d < e\), entonces \(a < e\).

Para ello, completar la siguiente teoría de Lean4:

import Mathlib.Data.Real.Basic

variable (a b c d e : ℝ)

example
  (h1 : a ≤ b)
  (h2 : b < c)
  (h3 : c ≤ d)
  (h4 : d < e) :
  a < e :=
sorry

import Mathlib.Data.Real.Basic

variable (a b c d e : ℝ)

example

(h1 : a ≤ b)

(h2 : b < c)

(h3 : c ≤ d)

(h4 : d < e) :

a < e :=

sorry

Demostraciones en lenguaje natural (LN)

1ª demostración en LN

Por la siguiente cadena de desigualdades
\begin{align}
a &\leq b &&\text{[por la hipótesis 1 (\(a \leq b\))]} \\
&< c &&\text{[por la hipótesis 2 (\(b < c\))]} \\
&\leq d &&\text{[por la hipótesis 3 (\(c \leq d\))]} \\
&< e &&\text{[por la hipótesis 4 (\(d < e\))]}
\end{align}

2ª demostración en LN

A partir de las hipótesis 1 (\(a \leq b\)) y 2 (\(b < c\)) se tiene
\[a < c\]
que, junto la hipótesis 3 (\(c \leq d\)) da
\[a < d\]
que, junto la hipótesis 4 (\(d < e\)) da
\[a < e.\]

3ª demostración en LN

Demostrar \(a < e\), por la hipótesis 1 (\(a \leq b\)) se reduce a
\[b < e\]
que, por la hipótesis 2 (\(b < c\)), se reduce a
\[c < e\]
que, por la hipótesis 3 (\(c \leq d\)), se reduce a
\[d < e\]
que es cierto, por la hipótesis 4.

Demostraciones con Lean4

import Mathlib.Data.Real.Basic

variable (a b c d e : ℝ)

-- 1ª demostración
-- ===============

example
  (h1 : a ≤ b)
  (h2 : b < c)
  (h3 : c ≤ d)
  (h4 : d < e) :
  a < e :=
calc
  a ≤ b := h1
  _ < c := h2
  _ ≤ d := h3
  _ < e := h4

-- 2ª demostración
-- ===============

example
  (h1 : a ≤ b)
  (h2 : b < c)
  (h3 : c ≤ d)
  (h4 : d < e) :
  a < e :=
by
  have h5 : a < c := lt_of_le_of_lt h1 h2
  have h6 : a < d := lt_of_lt_of_le h5 h3
  show a < e
  exact lt_trans h6 h4

-- 3ª demostración
-- ===============

example
  (h1 : a ≤ b)
  (h2 : b < c)
  (h3 : c ≤ d)
  (h4 : d < e) :
  a < e :=
by
  apply lt_of_le_of_lt h1
  apply lt_trans h2
  apply lt_of_le_of_lt h3
  exact h4

-- El desarrollo de la prueba es
--
--    a b c d e : ℝ,
--    h1 : a ≤ b,
--    h2 : b < c,
--    h3 : c ≤ d,
--    h4 : d < e
--    ⊢ a < e
-- apply lt_of_le_of_lt h1,
--    ⊢ b < e
-- apply lt_trans h2,
--    ⊢ c < e
-- apply lt_of_le_of_lt h3,
--    ⊢ d < e
-- exact h4,
--    no goals

-- 4ª demostración
-- ===============

example
  (h1 : a ≤ b)
  (h2 : b < c)
  (h3 : c ≤ d)
  (h4 : d < e) :
  a < e :=
by linarith

import Mathlib.Data.Real.Basic

variable (a b c d e : ℝ)

-- 1ª demostración

-- ===============

example

(h1 : a ≤ b)

(h2 : b < c)

(h3 : c ≤ d)

(h4 : d < e) :

a < e :=

calc

a ≤ b := h1

_ < c := h2

_ ≤ d := h3

_ < e := h4

-- 2ª demostración

-- ===============

example

(h1 : a ≤ b)

(h2 : b < c)

(h3 : c ≤ d)

(h4 : d < e) :

a < e :=

have h5 : a < c := lt_of_le_of_lt h1 h2

have h6 : a < d := lt_of_lt_of_le h5 h3

show a < e

exact lt_trans h6 h4

-- 3ª demostración

-- ===============

example

(h1 : a ≤ b)

(h2 : b < c)

(h3 : c ≤ d)

(h4 : d < e) :

a < e :=

apply lt_of_le_of_lt h1

apply lt_trans h2

apply lt_of_le_of_lt h3

exact h4

-- El desarrollo de la prueba es

-- a b c d e : ℝ,

-- h1 : a ≤ b,

-- h2 : b < c,

-- h3 : c ≤ d,

-- h4 : d < e

-- ⊢ a < e

-- apply lt_of_le_of_lt h1,

-- ⊢ b < e

-- apply lt_trans h2,

-- ⊢ c < e

-- apply lt_of_le_of_lt h3,

-- ⊢ d < e

-- exact h4,

-- no goals

-- 4ª demostración

-- ===============

example

(h1 : a ≤ b)

(h2 : b < c)

(h3 : c ≤ d)

(h4 : d < e) :

a < e :=

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. 14.

4. En ℝ, si 2a ≤ 3b, 1 ≤ a y c = 2, entonces c + a ≤ 5b

Demostrar con Lean4 que si \(a\), \(b\) y \(c\) son números reales tales que \(2a \leq 3b\), \(1 \leq a\) y \(c = 2\), entonces \(c + a \leq 5b\).

Para ello, completar la siguiente teoría de Lean4:

import Mathlib.Data.Real.Basic

variable (a b c : ℝ)

example
  (h1 : 2 * a ≤ 3 * b)
  (h2 : 1 ≤ a)
  (h3 : c = 2)
  : c + a ≤ 5 * b :=
sorry

import Mathlib.Data.Real.Basic

variable (a b c : ℝ)

example

(h1 : 2 * a ≤ 3 * b)

(h2 : 1 ≤ a)

(h3 : c = 2)

: c + a ≤ 5 * b :=

sorry

Demostración en lenguaje natural

Por la siguiente cadena de desigualdades
\begin{align}
c + a &= 2 + a &&\text{[por la hipótesis 3 (\(c = 2\))]} \\
&\leq 2·a + a &&\text{[por la hipótesis 2 (\(1 \leq a\))]} \\
&= 3·a \\
&\leq 9/2·b &&\text{[por la hipótesis 1 (\(2·a \leq 3·b\))]} \\
&\leq 5·b
\end{align}

Demostraciones con Lean4

import Mathlib.Data.Real.Basic

variable (a b c : ℝ)

-- 1ª demostración
example
  (h1 : 2 * a ≤ 3 * b)
  (h2 : 1 ≤ a)
  (h3 : c = 2)
  : c + a ≤ 5 * b :=
calc
  c + a = 2 + a     := by rw [h3]
      _ ≤ 2 * a + a := by linarith only [h2]
      _ = 3 * a     := by linarith only []
      _ ≤ 9/2 * b   := by linarith only [h1]
      _ ≤ 5 * b     := by linarith

-- 2ª demostración
example
  (h1 : 2 * a ≤ 3 * b)
  (h2 : 1 ≤ a)
  (h3 : c = 2)
  : c + a ≤ 5 * b :=
by linarith

import Mathlib.Data.Real.Basic

variable (a b c : ℝ)

-- 1ª demostración

example

(h1 : 2 * a ≤ 3 * b)

(h2 : 1 ≤ a)

(h3 : c = 2)

: c + a ≤ 5 * b :=

calc

c + a = 2 + a := by rw [h3]

_ ≤ 2 * a + a := by linarith only [h2]

_ = 3 * a := by linarith only []

_ ≤ 9/2 * b := by linarith only [h1]

_ ≤ 5 * b := by linarith

-- 2ª demostración

example

(h1 : 2 * a ≤ 3 * b)

(h2 : 1 ≤ a)

(h3 : c = 2)

: c + a ≤ 5 * b :=

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. 14.

5. En ℝ, si 1 ≤ a y b ≤ d, entonces 2 + a + eᵇ ≤ 3a + eᵈ

Demostrar con Lean4 que si \(a\), \(b\) y \(d\) números reales tales que \(1 \leq a\) y \(b \leq d\), entonces \(2 + a + e^b \leq 3a + e^d\).

Para ello, completar la siguiente teoría de Lean4:

import Mathlib.Analysis.SpecialFunctions.Log.Basic

open Real

variable (a b d : ℝ)

example
  (h1 : 1 ≤ a)
  (h2 : b ≤ d)
  : 2 + a + exp b ≤ 3 * a + exp d :=
by sorry

import Mathlib.Analysis.SpecialFunctions.Log.Basic

open Real

variable (a b d : ℝ)

example

(h1 : 1 ≤ a)

(h2 : b ≤ d)

: 2 + a + exp b ≤ 3 * a + exp d :=

by sorry

Demostración en lenguaje natural

De la primera hipótesis (\(1 \leq a\)), multiplicando por \(2\), se obtiene
\[2 \leq 2a\]
y, sumando a ambos lados, se tiene
\[2 + a \leq 3a \tag{1}\]

De la hipótesis 2 (\(b \leq d\)) y de la monotonía de la función exponencial se tiene
\[e^b \leq e^d \tag{2} \]

Finalmente, de (1) y (2) se tiene
\[2 + a + e^b \leq 3a + e^d\]

Demostraciones con Lean4

import Mathlib.Analysis.SpecialFunctions.Log.Basic

open Real

variable (a b d : ℝ)

-- 1ª demostración
example
  (h1 : 1 ≤ a)
  (h2 : b ≤ d)
  : 2 + a + exp b ≤ 3 * a + exp d :=
by
  have h3 : 2 + a ≤ 3 * a := calc
    2 + a = 2 * 1 + a := by linarith only []
        _ ≤ 2 * a + a := by linarith only [h1]
        _ ≤ 3 * a     := by linarith only []
  have h4 : exp b ≤ exp d := by
    linarith only [exp_le_exp.mpr h2]
  show 2 + a + exp b ≤ 3 * a + exp d
  exact add_le_add h3 h4

-- 2ª demostración
example
  (h1 : 1 ≤ a)
  (h2 : b ≤ d)
  : 2 + a + exp b ≤ 3 * a + exp d :=
calc
  2 + a + exp b
    ≤ 3 * a + exp b := by linarith only [h1]
  _ ≤ 3 * a + exp d := by linarith only [exp_le_exp.mpr h2]

-- 3ª demostración
example
  (h1 : 1 ≤ a)
  (h2 : b ≤ d)
  : 2 + a + exp b ≤ 3 * a + exp d :=
by linarith [exp_le_exp.mpr h2]

import Mathlib.Analysis.SpecialFunctions.Log.Basic

open Real

variable (a b d : ℝ)

-- 1ª demostración

example

(h1 : 1 ≤ a)

(h2 : b ≤ d)

: 2 + a + exp b ≤ 3 * a + exp d :=

have h3 : 2 + a ≤ 3 * a := calc

2 + a = 2 * 1 + a := by linarith only []

_ ≤ 2 * a + a := by linarith only [h1]

_ ≤ 3 * a := by linarith only []

have h4 : exp b ≤ exp d := by

linarith only [exp_le_exp.mpr h2]

show 2 + a + exp b ≤ 3 * a + exp d

exact add_le_add h3 h4

-- 2ª demostración

example

(h1 : 1 ≤ a)

(h2 : b ≤ d)

: 2 + a + exp b ≤ 3 * a + exp d :=

calc

2 + a + exp b

≤ 3 * a + exp b := by linarith only [h1]

_ ≤ 3 * a + exp d := by linarith only [exp_le_exp.mpr h2]

-- 3ª demostración

example

(h1 : 1 ≤ a)

(h2 : b ≤ d)

: 2 + a + exp b ≤ 3 * a + exp d :=

by linarith [exp_le_exp.mpr h2]

Demostraciones interactivas

Se puede interactuar con las demostraciones anteriores en Lean 4 Web.

Referencias

J. Avigad y P. Massot. Mathematics in Lean, p. 15.

1. Si G es un grupo y a, b ∈ G, tales que ab = 1 entonces a⁻¹ = b

2. Si G es un grupo y a, b ∈ G, entonces (ab)⁻¹ = b⁻¹a⁻¹

3. En ℝ, si a ≤ b, b < c, c ≤ d y d < e, entonces a < e

4. En ℝ, si 2a ≤ 3b, 1 ≤ a y c = 2, entonces c + a ≤ 5b

5. En ℝ, si 1 ≤ a y b ≤ d, entonces 2 + a + eᵇ ≤ 3a + eᵈ

Se puede imprimir o compartir con