Si `f(x) ≤ f(y) → x ≤ y`, entonces f es inyectiva
Demostrar con Lean4 que si \(f\) una función de \(ℝ\) en \(ℝ\) tal que
\[ (∀ x, y)[f(x) ≤ f(y) → x ≤ y] \]
entonces \(f\) es inyectiva.
Para ello, completar la siguiente teoría de Lean4:
|
1 2 3 4 5 6 7 8 9 |
import Mathlib.Data.Real.Basic open Function variable (f : ℝ → ℝ) example (h : ∀ {x y}, f x ≤ f y → x ≤ y) : Injective f := by sorry |
Read More «Si `f(x) ≤ f(y) → x ≤ y`, entonces f es inyectiva»