5 diciembre 2023 – Calculemus

Si f no está acotada superiormente, entonces (∀a)(∃x)[f(x) > a]

PorJosé A. Alonso 5 diciembre 202324 noviembre 2023

Demostrar con Lean4 que si \(f\) no está acotada superiormente, entonces \((∀a)(∃x)[f(x) > a]\).

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

import Mathlib.Data.Real.Basic

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

def acotadaSup (f : ℝ → ℝ) :=
  ∃ a, CotaSuperior f a

variable (f : ℝ → ℝ)

example
  (h : ¬acotadaSup f)
  : ∀ a, ∃ x, f x > a :=
by sorry

import Mathlib.Data.Real.Basic

def CotaSuperior (f : ℝ → ℝ) (a : ℝ) : Prop :=

∀ x, f x ≤ a

def acotadaSup (f : ℝ → ℝ) :=

∃ a, CotaSuperior f a

variable (f : ℝ → ℝ)

example

(h : ¬acotadaSup f)

: ∀ a, ∃ x, f x > a :=

by sorry