Para todo c ∈ ℝ-{0}, la función f(x) = x * c es inyectiva
Demostrar que para todo c ∈ ℝ-{0}, la función f(x) = x * c es inyectiva
Para ello, completar la siguiente teoría de Lean:
|
1 2 3 4 5 6 7 8 9 10 |
import data.real.basic open function variable {c : ℝ} example (h : c ≠ 0) : injective (λ x, c * x) := sorry |
Read More «Para todo c ∈ ℝ-{0}, la función f(x) = x * c es inyectiva»