--- Título: La función (x ↦ x + c) es inyectiva Autor: José A. Alonso --- Demostrar con Lean4 que la función \\(x ↦ x + c\\) es inyectiva. Para ello, completar la siguiente teoría de Lean4:

import Mathlib.Data.Real.Basic
open Function

variable {c : ℝ}

example : Injective ((. + c)) :=
by sorry

Demostración en lenguaje natural [mathjax] Se usará el lema \\[ (∀ a, b, c) [a + b = c + b → a = c] \\tag{L1} \\] Hay que demostrar que \\[ (∀ x₁ x₂) [f(x₁) = f(x₂) → x₁ = x₂] \\] Sean \\(x₁, x₂\\) tales que \\(f(x₁) = f(x₂)\\). Entonces, \\[ x₁ + c = x₂ + c \\] y, por L1, \\(x₁ = x₂\\). Demostraciones con Lean4

import Mathlib.Data.Real.Basic
open Function

variable {c : ℝ}

-- 1ª demostración
example : Injective ((. + c)) :=
by
  intro (x1 : ℝ) (x2 : ℝ) (h1 : x1 + c = x2 + c)
  show x1 = x2
  exact add_right_cancel h1

-- 2ª demostración
example : Injective ((. + c)) :=
by
  intro x1 x2 h1
  show x1 = x2
  exact add_right_cancel h1

-- 3ª demostración
example : Injective ((. + c)) :=
  fun _ _ h ↦ add_right_cancel h

-- Lemas usados
-- ============

-- variable {a b : ℝ}
-- #check (add_right_cancel : a + b = c + b → a = c)

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

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