José A. AlonsoDemostrar que para todo c ∈ ℝ-{0}, la función f(x) = x * c es inyectiva
Para ello, completar la siguiente teoría de Lean:
import data.real.basic open function variable {c : ℝ} example (h : c ≠ 0) : injective (λ x, c * x) := sorry |
Demostrar que para todo c ∈ ℝ-{0}, la función f(x) = x * c es inyectiva
Para ello, completar la siguiente teoría de Lean:
import data.real.basic open function variable {c : ℝ} example (h : c ≠ 0) : injective (λ x, c * x) := sorry |