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:
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 |