Menu Close

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:

import data.real.basic
 
open function
 
variable {c : }
 
example
  (h : c  0)
  : injective (λ x, c * x) :=
sorry

Soluciones con Lean

import data.real.basic
 
open function
 
variable {c : }
 
-- 1ª demostración
-- ===============
 
example
  (h : c  0)
  : injective (λ x, c * x) :=
begin
  assume x1 : ,
  assume x2 : ,
  assume h1 : (λ x, c * x) x1 = (λ x, c * x) x2,
  have h2 : c * x1 = c * x2 := h1,
  show x1 = x2,
    by exact (mul_right_inj' h).mp h1,
end
 
-- 2ª demostración
-- ===============
 
example
  (h : c  0)
  : injective (λ x, c * x) :=
begin
  intros x1 x2 h',
  dsimp at h',
  apply mul_left_cancel₀ h,
  exact h',
end
 
-- 3ª demostración
-- ===============
 
example
  (h : c  0)
  : injective (λ x, c * x) :=
begin
  intros x1 x2 h',
  dsimp at h',
  exact (mul_right_inj' h).mp h'
end
 
-- 3ª demostración
-- ===============
 
example
  {c : }
  (h : c  0)
  : injective (λ x, c * x) :=
λ x1 x2 h', mul_left_cancel₀ h h'

Se puede interactuar con la prueba anterior en esta sesión con Lean.

Referencias

Escribe un comentario