Skip to main content

La función identidad no está acotada superiormente

Demostrar con Lean4 que la función identidad no está acotada superiormente.

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

import src.Funcion_no_acotada_superiormente

example : ¬ acotadaSup (fun x ↦ x) :=
by sorry

Demostración en lenguaje natural

Usando el lema de ejercicio anterior (que afirma que si para cada \(a\), existe un \(x\) tal que \(f(x) > a\), entonces \(f\) no tiene cota superior) basta demostrar que \[ (∀a ∈ ℝ)(∃x ∈ ℝ) [x > a] \] Sea \(a ∈ ℝ\). Entonces \(a + 1 > a\) y, por tanto, \((∃x ∈ ℝ) [x > a]\).

Demostraciones con Lean4

import src.Funcion_no_acotada_superiormente

-- 1ª demostración
example : ¬ acotadaSup (fun x ↦ x) :=
by
  apply sinCotaSup
  -- ⊢ ∀ (a : ℝ), ∃ x, x > a
  intro a
  -- a : ℝ
  -- ⊢ ∃ x, x > a
  use a + 1
  -- ⊢ a + 1 > a
  linarith

-- 2ª demostración
example : ¬ acotadaSup (fun x ↦ x) :=
by
  apply sinCotaSup
  -- ⊢ ∀ (a : ℝ), ∃ x, x > a
  intro a
  -- a : ℝ
  -- ⊢ ∃ x, x > a
  exact ⟨a + 1, by linarith⟩

-- 3ª demostración
example : ¬ acotadaSup (fun x ↦ x) :=
by
  apply sinCotaSup
  -- ⊢ ∀ (a : ℝ), ∃ x, x > a
  exact fun a ↦ ⟨a + 1, by linarith⟩

Demostraciones interactivas

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

Referencias