Si f no es monótona, entonces ∃x∃y[x ≤ y ∧ f(y) < f(x)]​

Demostrar con Lean4 que si \(f\) no es monótona, entonces \(∃x∃y[x ≤ y ∧ f(y) < f(x)]​\).

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

Demostración en lenguaje natural

Usaremos los siguientes lemas:
\begin{align}
&¬(∀x)P(x) ↔ (∃ x)¬P(x) \tag{L1} \\
&¬(p → q) ↔ p ∧ ¬q \tag{L2} \\
&(∀a, b ∈ ℝ)[¬b ≤ a → a < b] \tag{L3}
\end{align}

Por la definición de función monótona,
\[ ¬(∀x)(∀y)[x ≤ y → f(x) ≤ f(y)] \]
Aplicando L1 se tiene
\[ (∃x)¬(∀y)[x ≤ y → f(x) ≤ f(y)] \]
Sea \(a\) tal que
\[ ¬(∀y)[a ≤ y → f(a) ≤ f(y)] \]
Aplicando L1 se tiene
\[ (∃y)¬[a ≤ y → f(a) ≤ f(y)] \]
Sea \(b\) tal que
\[ ¬[a ≤ b → f(a) ≤ f(b)] \]
Aplicando L2 se tiene que
\[ a ≤ b ∧ ¬(f(a) ≤ f(b)) \]
Aplicando L3 se tiene que
\[ a ≤ b ∧ f(b) < f(a) \]
Por tanto,
\[ (∃x,y)[x ≤ y ∧ f(y) < f(x)] \]

Demostraciones con Lean4

Demostraciones interactivas

Se puede interactuar con las demostraciones anteriores en Lean 4 Web.

Referencias

Escribe un comentario