Si x es el supremo de A, entonces ∀ y, y < x → ∃ a ∈ A, y < a
En Lean se puede definir que x es una cota superior de A por
|
1 2 |
def cota_superior (A : set ℝ) (x : ℝ) := ∀ a ∈ A, a ≤ x |
y x es el supremo de A por
|
1 2 |
def es_supremo (A : set ℝ) (x : ℝ) := cota_superior A x ∧ ∀ y, cota_superior A y → x ≤ y |
Demostrar que si x es el supremo de A, entonces
|
1 |
∀ y, y < x → ∃ a ∈ A, y < a |
Para ello, completar la siguiente teoría de Lean:
|
1 2 3 4 5 6 7 8 9 10 11 12 13 14 |
import data.real.basic variable {A : set ℝ} variable {x : ℝ} def cota_superior (A : set ℝ) (x : ℝ) := ∀ a ∈ A, a ≤ x def es_supremo (A : set ℝ) (x : ℝ) := cota_superior A x ∧ ∀ y, cota_superior A y → x ≤ y example (hx : es_supremo A x) : ∀ y, y < x → ∃ a ∈ A, y < a := sorry |
[expand title=»Soluciones con Lean»]
|
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 |
import data.real.basic variable {A : set ℝ} variable {x : ℝ} def cota_superior (A : set ℝ) (x : ℝ) := ∀ a ∈ A, a ≤ x def es_supremo (A : set ℝ) (x : ℝ) := cota_superior A x ∧ ∀ y, cota_superior A y → x ≤ y -- 1ª demostración example (hx : es_supremo A x) : ∀ y, y < x → ∃ a ∈ A, y < a := begin intros y hy, by_contradiction, push_neg at h, have h1 : x ≤ y := hx.2 y h, replace h1 : ¬(y < x) := not_lt_of_le h1, exact h1 hy, end -- 2ª demostración example (hx : es_supremo A x) : ∀ y, y < x → ∃ a ∈ A, y < a := begin intros y hy, by_contradiction, push_neg at h, apply absurd hy, apply not_lt_of_le, apply hx.2 y, exact h, end -- 3ª demostración example (hx : es_supremo A x) : ∀ y, y < x → ∃ a ∈ A, y < a := begin intros y hy, by_contradiction, push_neg at h, exact absurd hy (not_lt_of_le (hx.2 y h)), end -- 4ª demostración example (hx : es_supremo A x) : ∀ y, y < x → ∃ a ∈ A, y < a := begin intros y hy, contrapose hy, push_neg at hy, push_neg, unfold es_supremo at hx, cases hx with h1 h2, apply h2 y, unfold cota_superior, exact hy, end -- 5ª demostración example (hx : es_supremo A x) : ∀ y, y < x → ∃ a ∈ A, y < a := begin intros y hy, contrapose hy, push_neg at hy, push_neg, cases hx with h1 h2, exact h2 y hy, end -- 6ª demostración example (hx : es_supremo A x) : ∀ y, y < x → ∃ a ∈ A, y < a := begin intros y hy, contrapose hy, push_neg at hy, push_neg, exact hx.right y hy, end -- 7ª demostración example (hx : es_supremo A x) : ∀ y, y < x → ∃ a ∈ A, y < a := begin intro y, contrapose!, exact hx.right y, end |
Se puede interactuar con la prueba anterior en esta sesión con Lean.
En los comentarios se pueden escribir otras soluciones, escribiendo el código entre una línea con <pre lang="lean"> y otra con </pre>
[/expand]
[expand title=»Soluciones con Isabelle/HOL»]
|
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 |
theory "Si_x_es_el_supremo_de_A_entonces_forall_y_y_lt_x_to_exists_a_in_A_y_lt_a" imports Main HOL.Real begin definition cota_superior :: "(real set) ⇒ real ⇒ bool" where "cota_superior A x ⟷ (∀a∈A. a ≤ x)" definition es_supremo :: "(real set) ⇒ real ⇒ bool" where "es_supremo A x ⟷ (cota_superior A x ∧ (∀ y. cota_superior A y ⟶ x ≤ y))" (* 1ª demostración *) lemma assumes "es_supremo A x" shows "∀y<x. ∃a∈A. y < a" proof (intro allI impI) fix y assume "y < x" show "∃a∈A. y < a" proof (rule ccontr) assume "¬ (∃a∈A. y < a)" then have "∀a∈A. a ≤ y" by auto then have "cota_superior A y" using cota_superior_def by simp then have "x ≤ y" using assms es_supremo_def by simp then have "x < x" using ‹y < x› by simp then show False by simp qed qed (* 2ª demostración *) lemma assumes "es_supremo A x" shows "∀y<x. ∃a∈A. y < a" proof (intro allI impI) fix y assume "y < x" show "∃a∈A. y < a" proof (rule ccontr) assume "¬ (∃a∈A. y < a)" then have "cota_superior A y" using cota_superior_def by auto then show "False" using assms es_supremo_def ‹y < x› by auto qed qed end |
En los comentarios se pueden escribir otras soluciones, escribiendo el código entre una línea con <pre lang="isar"> y otra con </pre>
[/expand]
