Funcion_no_acotada_inferiormente.md

Título	Autor
Si para cada a existe un x tal que f(x) < a, entonces f no tiene cota inferior.	José A. Alonso

Demostrar con Lean4 que si \(f\) es una función de \(ℝ\) en \(ℝ\) tal que para cada \(a\) existe un \(x\) tal que \(f(x) < a\), entonces \(f\) no tiene cota inferior.

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

import Mathlib.Data.Real.Basic

def CotaInferior (f : ℝ → ℝ) (a : ℝ) : Prop :=
  ∀ x, a ≤ f x

def acotadaInf (f : ℝ → ℝ) : Prop :=
  ∃ a, CotaInferior f a

variable (f : ℝ → ℝ)

example
  (h : ∀ a, ∃ x, f x < a)
  : ¬ acotadaInf f :=
by sorry

Demostración en lenguaje natural

[mathjax] Supongamos que \(f\) tiene cota inferior. Sea \(b\) una de dichas cotas inferiores. Por la hipótesis, existe un \(x\) tal que \(f(x) < b\). Además, como \(b\) es una cota inferior de \(f\), \(b ≤ f(x)\) que contradice la desigualdad anterior.

Demostraciones con Lean4

import Mathlib.Data.Real.Basic

def CotaInferior (f : ℝ → ℝ) (a : ℝ) : Prop :=
  ∀ x, a ≤ f x

def acotadaInf (f : ℝ → ℝ) : Prop :=
  ∃ a, CotaInferior f a

variable (f : ℝ → ℝ)

-- 1ª demostración
example
  (h : ∀ a, ∃ x, f x < a)
  : ¬ acotadaInf f :=
by
  intros hf
  -- hf : acotadaInf f
  -- ⊢ False
  cases' hf with b hb
  -- b : ℝ
  -- hb : CotaInferior f b
  cases' h b with x hx
  -- x : ℝ
  -- hx : f x < b
  have : b ≤ f x := hb x
  linarith

-- 2ª demostración
example
  (h : ∀ a, ∃ x, f x < a)
  : ¬ acotadaInf f :=
by
  intros hf
  -- hf : acotadaInf f
  -- ⊢ False
  rcases hf with ⟨b, hb : CotaInferior f b⟩
  rcases h b with ⟨x, hx : f x < b⟩
  have : b ≤ f x := hb x
  linarith

Demostraciones interactivas

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

Referencias

• J. Avigad y P. Massot. Mathematics in Lean, p. 32.