Si f no está acotada superiormente, entonces (∀a)(∃x)[f(x) > a]
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:
|
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 : ¬acotadaSup f) : ∀ a, ∃ x, f x > a := by sorry |
Demostración en lenguaje natural
1ª demostración en LN
Usaremos los siguientes lemas
\begin{align}
&¬(∃x)P(x) → (∀x)¬P(x) \tag{L1} \\
&¬a > b → a ≤ b \tag{L2}
\end{align}
Sea \(a ∈ ℝ\). Tenemos que demostrar que
\[ (∃x)[f(x) > a] \]
Lo haremos por reducción al absurdo. Para ello, suponemos que
\[ ¬(∃x)[f(x) > a] \tag{1} \]
y tenemos que obtener una contradicción. Aplicando L1 a (1) se tiene
\[ (∀x)[¬ f(x) > a] \]
y, aplicando L2, se tiene
\[ (∀x)[f(x) ≤ a] \]
Lo que significa que \(a\) es una cota superior de \(f\) y, por tanto \(f\) está acotada superiormente, en cotradicción con la hipótesis.
2ª demostración en LN
Por la contrarecíproca, se supone que
\[ ¬(∀a)(∃x)[f(x) > a] \tag{1} \]
y tenemos que demostrar que \(f\) está acotada superiormente.
Interiorizando la negación en (1) y simplificando, se tiene que
\[ (∃a)(∀x)[f x ≤ a] \]
que es lo que teníamos que demostrar.
Demostraciones con Lean4
|
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 |
import Mathlib.Data.Real.Basic def CotaSuperior (f : ℝ → ℝ) (a : ℝ) : Prop := ∀ x, f x ≤ a def acotadaSup (f : ℝ → ℝ) := ∃ a, CotaSuperior f a variable (f : ℝ → ℝ) -- 1ª demostración -- =============== example (h : ¬acotadaSup f) : ∀ a, ∃ x, f x > a := by intro a -- a : ℝ -- ⊢ ∃ x, f x > a by_contra h1 -- h1 : ¬∃ x, f x > a -- ⊢ False have h2 : ∀ x, ¬ f x > a := forall_not_of_not_exists h1 have h3 : ∀ x, f x ≤ a := by intro x have h3a : ¬ f x > a := h2 x show f x ≤ a exact le_of_not_gt h3a have h4 : CotaSuperior f a := h3 have h5 : ∃ b, CotaSuperior f b := ⟨a, h4⟩ have h6 : acotadaSup f := h5 show False exact h h6 -- 2ª demostración -- =============== example (h : ¬acotadaSup f) : ∀ a, ∃ x, f x > a := by intro a -- a : ℝ -- ⊢ ∃ x, f x > a by_contra h1 -- h1 : ¬∃ x, f x > a -- ⊢ False apply h -- ⊢ acotadaSup f use a -- ⊢ CotaSuperior f a intro x -- x : ℝ -- ⊢ f x ≤ a apply le_of_not_gt -- ⊢ ¬f x > a intro h2 -- h2 : f x > a -- ⊢ False apply h1 -- ⊢ ∃ x, f x > a use x -- ⊢ f x > a exact h2 -- 3ª demostración -- =============== example (h : ¬acotadaSup f) : ∀ a, ∃ x, f x > a := by unfold acotadaSup at h -- h : ¬∃ a, CotaSuperior f a unfold CotaSuperior at h -- h : ¬∃ a, ∀ (x : ℝ), f x ≤ a push_neg at h -- ∀ (a : ℝ), ∃ x, f x > a exact h -- 4ª demostración -- =============== example (h : ¬acotadaSup f) : ∀ a, ∃ x, f x > a := by simp only [acotadaSup, CotaSuperior] at h -- h : ¬∃ a, ∀ (x : ℝ), f x ≤ a push_neg at h -- ∀ (a : ℝ), ∃ x, f x > a exact h -- 5ª demostración -- =============== example (h : ¬acotadaSup f) : ∀ a, ∃ x, f x > a := by contrapose h -- h : ¬∀ (a : ℝ), ∃ x, f x > a -- ⊢ ¬¬acotadaSup f push_neg at * -- h : ∃ a, ∀ (x : ℝ), f x ≤ a -- ⊢ acotadaSup f exact h -- 6ª demostración -- =============== example (h : ¬acotadaSup f) : ∀ a, ∃ x, f x > a := by contrapose! h -- h : ∃ a, ∀ (x : ℝ), f x ≤ a -- ⊢ acotadaSup f exact h -- Lemas usados -- ============ -- variable {α : Type _} -- variable (P : α → Prop) -- #check (forall_not_of_not_exists : (¬∃ x, P x) → ∀ x, ¬P x) -- -- variable (a b : ℝ) -- #check (le_of_not_gt : ¬a > b → a ≤ b) |
Demostraciones interactivas
Se puede interactuar con las demostraciones anteriores en Lean 4 Web.
Referencias
- J. Avigad y P. Massot. Mathematics in Lean, p. 33.
