La función (x ↦ x + c) es inyectiva
Demostrar con Lean4 que la función \(x ↦ x + c\) es inyectiva.
Para ello, completar la siguiente teoría de Lean4:
|
1 2 3 4 5 6 7 |
import Mathlib.Data.Real.Basic open Function variable {c : ℝ} example : Injective ((. + c)) := by sorry |
Demostración en lenguaje natural
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
|
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 |
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.
