DAO: La semana en Calculemus (23 de septiembre de 2022)

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

A continuación se muestran las soluciones.

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

Demostrar que si G es un grupo y a, b ∈ G, entonces

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

Soluciones con Lean

Se puede interactuar con la prueba anterior en esta sesión con Lean.

Referencias

2. Si a, b, c, d, e ∈ ℝ tales que a ≤ b, b < c, c ≤ d, d < e, entonces a < e

Demostrar que si a, b, c, d, e ∈ ℝ tales que

entonces

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

Soluciones con Lean

Se puede interactuar con la prueba anterior en esta sesión con Lean.

Referencias

3. Si a, b, d ∈ ℝ tales que 1 ≤ a y b ≤ d, entonces 2 + a + eᵇ ≤ 3a + eᵈ

Demostrar que si a, b, d ∈ ℝ 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 Lean:

Nota: Se pueden usar los lemas

Soluciones con Lean

Se puede interactuar con la prueba anterior en esta sesión con Lean.

Referencias

4. Si a, b, c, d, f ∈ ℝ tales que a ≤ b y c < d, entonces a + eᶜ + f < b + eᵈ + f

Demostrar que si a, b, c, d, f ∈ ℝ tales que

entonces

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

Soluciones con Lean

Se puede interactuar con la prueba anterior en esta sesión con Lean.

Referencias

5. Si a, b ∈ ℝ tales que a ≤ b, entonces log(1 + eᵃ) ≤ log(1 + eᵇ)

Demostrar que si a, b ∈ ℝ tales que a ≤ b, entonces log(1 + eᵃ) ≤ log(1 + eᵇ).

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

Soluciones con Lean

Se puede interactuar con la prueba anterior en esta sesión con Lean.

Referencias