25 octubre 2023 – Calculemus

Si c ≠ 0, entonces la función (x ↦ cx) es inyectiva

PorJosé A. Alonso 25 octubre 202318 octubre 2023

Demostrar con Lean4 que si $c ≠ 0$ , entonces la función $x ↦ cx$ es inyectiva.

Para ello, completar la siguiente teoría de Lean4:

import Mathlib.Data.Real.Basic
open Function
variable {c : ℝ}

example
  (h : c ≠ 0)
  : Injective ((c * .)) :=
by sorry

import Mathlib.Data.Real.Basic

open Function

variable {c : ℝ}

example

(h : c ≠ 0)

: Injective ((c * .)) :=

by sorry