Una función creciente e involutiva es la identidad

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 Lean que f sea creciente se representa por monotone f y que sea involutiva por involutive f

Demostrar que si f es creciente e involutiva, entonces f es la identidad.

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

[expand title=»Soluciones con Lean»]

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

En los comentarios se pueden escribir otras soluciones, escribiendo el código entre una línea con <pre lang="lean"> y otra con </pre>
[/expand]

[expand title=»Soluciones con Isabelle/HOL»]

En los comentarios se pueden escribir otras soluciones, escribiendo el código entre una línea con <pre lang="isar"> y otra con </pre>
[/expand]

La composición de una función creciente y una decreciente es decreciente

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 decreciente si para todo x e y tales que x ≤ y se tiene que f(x) ≥ f(y).

Demostrar que si f es creciente y g es decreciente, entonces (g ∘ f) es decreciente.

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

[expand title=»Soluciones con Lean»]

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

En los comentarios se pueden escribir otras soluciones, escribiendo el código entre una línea con <pre lang="lean"> y otra con </pre>
[/expand]

[expand title=»Soluciones con Isabelle/HOL»]

En los comentarios se pueden escribir otras soluciones, escribiendo el código entre una línea con <pre lang="isar"> y otra con </pre>
[/expand]

La composición de crecientes es creciente

Se dice que una función f de ℝ en ℝ es creciente si para todo x e y tales que x ≤ y se tiene que f(x) ≤ f(y).

En Lean que f sea creciente se representa por monotone f.

Demostrar que la composición de dos funciones crecientes es una función creciente.

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

[expand title=»Soluciones con Lean»]

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

En los comentarios se pueden escribir otras soluciones, escribiendo el código entre una línea con <pre lang="lean"> y otra con </pre>
[/expand]

[expand title=»Soluciones con Isabelle/HOL»]

En los comentarios se pueden escribir otras soluciones, escribiendo el código entre una línea con <pre lang="isar"> y otra con </pre>
[/expand]

Teorema del emparedado

En Lean, una sucesión u₀, u₁, u₂, … se puede representar mediante una función (u : ℕ → ℝ) de forma que u(n) es uₙ.

Se define que a es el límite de la sucesión u, por

donde se usa la notación |x| para el valor absoluto de x

Demostrar el teorema del emparedado; es decir, que si para todo n, u(n) ≤ v(n) ≤ w(n) y u(n) tiene el mismo límite que w(n), entonces v(n) también tiene dicho límite.

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

[expand title=»Soluciones con Lean»]

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

En los comentarios se pueden escribir otras soluciones, escribiendo el código entre una línea con <pre lang="lean"> y otra con </pre>
[/expand]

[expand title=»Soluciones con Isabelle/HOL»]

En los comentarios se pueden escribir otras soluciones, escribiendo el código entre una línea con <pre lang="isar"> y otra con </pre>
[/expand]

Producto de sucesiones convergentes a cero

En Lean, una sucesión u₀, u₁, u₂, … se puede representar mediante una función (u : ℕ → ℝ) de forma que u(n) es uₙ.

Se define que a es el límite de la sucesión u, por

donde se usa la notación |x| para el valor absoluto de x

Demostrar que si las sucesiones u(n) y v(n) convergen a cero, entonces u(n)·v(n) también converge a cero.

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

[expand title=»Soluciones con Lean»]

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

En los comentarios se pueden escribir otras soluciones, escribiendo el código entre una línea con <pre lang="lean"> y otra con </pre>
[/expand]

[expand title=»Soluciones con Isabelle/HOL»]

En los comentarios se pueden escribir otras soluciones, escribiendo el código entre una línea con <pre lang="isar"> y otra con </pre>
[/expand]