Demostracion_por_congruencia.md

Título	Autor
En ℝ, |a| = |a - b + b|	José A. Alonso

[mathjax]

Demostrar con Lean4 que en \(ℝ\), \(|a| = |a - b + b|\)

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

import Mathlib.Data.Real.Basic
variable (a b : ℝ)

example
  : |a| = |a - b + b| :=
by sorry

Demostraciones con Lean4

import Mathlib.Data.Real.Basic
variable (a b : ℝ)

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

example
  : |a| = |a - b + b| :=
by
  congr
  -- a = a - b + b
  ring

-- Comentario: La táctica congr sustituye una conclusión de la forma
-- A = B por las igualdades de sus subtérminos que no no iguales por
-- definición. Por ejemplo, sustituye la conclusión (x * f y = g w * f z)
-- por las conclusiones (x = g w) y (y = z).

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

example
  (a b : ℝ)
  : |a| = |a - b + b| :=
by { congr ; ring }

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

example
  (a b : ℝ)
  : |a| = |a - b + b| :=
by ring_nf

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

Referencias

• J. Avigad y P. Massot. Mathematics in Lean, p. 41.