Si ¬(∀a)(∃x)[f(x) > a], entonces f está acotada superiormente
Demostrar con Lean4 que si \(¬(∀a)(∃x)[f(x) > a]\), entonces \(f\) está acotada superiormente.
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 : ℝ → ℝ) := ∃ a, CotaSuperior f a variable (f : ℝ → ℝ) example (h : ¬∀ a, ∃ x, f x > a) : acotadaSup f := by sorry |
Read More «Si ¬(∀a)(∃x)[f(x) > a], entonces f está acotada superiormente»