Sea una función \(f\) de \(ℝ\) en \(ℝ\).

• Se dice que \(f\) es creciente si para todo \(x\) e \(y\) tales que \(x ≤ y\) se tiene que \(f(x) ≤ f(y)\).
• Se dice que \(f\) es involutiva si para todo \(x\) se tiene que \(f(f(x)) = x\).

En Lean4 que \(f\) sea creciente se representa por Monotone f y que sea involutiva por Involutive f

Demostrar con Lean4 que si \(f\) es creciente e involutiva, entonces \(f\) es la identidad.

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

Read More «Si una función es creciente e involutiva, entonces es la identidad»