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.
Read More “La semana en Calculemus (26 de agosto de 2023)”