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
Se usará el lema
(∀a,b,c)[a+b=c+b→a=c]
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
