Si para cada a existe un x tal que f(x) > a, entonces f no tiene cota superior
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 superior.
Para ello, completar la siguiente teoría de Lean4:
|
1 2 3 4 5 6 7 8 9 10 11 12 13 14 |
import Mathlib.Data.Real.Basic def CotaSuperior (f : ℝ → ℝ) (a : ℝ) : Prop := ∀ x, f x ≤ a def acotadaSup (f : ℝ → ℝ) : Prop := ∃ a, CotaSuperior f a variable (f : ℝ → ℝ) example (h : ∀ a, ∃ x, f x > a) : ¬ acotadaSup f := by sorry |
Read More «Si para cada a existe un x tal que f(x) > a, entonces f no tiene cota superior»