Menu Close

∃ x ∈ ℝ, 2 < x < 3

José A. Alonso

Demostrar que ∃ x ∈ ℝ, 2 < x < 3

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

import data.real.basic
 
example : ∃ x : ℝ, 2 < x ∧ x < 3 :=
sorry

Soluciones con Lean

import data.real.basic
 
-- 1ª demostración
-- ===============
 
example : ∃ x : ℝ, 2 < x ∧ x < 3 :=
begin
  have h : 2 < (5 : ℝ) / 2 ∧ (5 : ℝ) / 2 < 3,
    by norm_num,
  show ∃ x : ℝ, 2 < x ∧ x < 3,
    by exact Exists.intro (5 / 2) h,
end
 
-- 2ª demostración
-- ===============
 
example : ∃ x : ℝ, 2 < x ∧ x < 3 :=
begin
  have h : 2 < (5 : ℝ) / 2 ∧ (5 : ℝ) / 2 < 3,
    by norm_num,
  show ∃ x : ℝ, 2 < x ∧ x < 3,
    by exact ⟨5 / 2, h⟩,
end
 
-- 3ª demostración
-- ===============
 
example : ∃ x : ℝ, 2 < x ∧ x < 3 :=
begin
  use 5 / 2,
  norm_num
end
 
-- 4ª demostración
-- ===============
 
example : ∃ x : ℝ, 2 < x ∧ x < 3 :=
⟨5 / 2, by norm_num⟩

Se puede interactuar con la prueba anterior en esta sesión con Lean.

Referencias

Leave a Reply