--- Título: Si (∀ε > 0)[x ≤ ε], entonces x ≤ 0. Autor: José A. Alonso --- [mathjax] Demostrar con Lean4 que si \\((∀ε > 0)[x ≤ ε]\\), entonces \\(x ≤ 0\\). Para ello, completar la siguiente teoría de Lean4:

import Mathlib.Data.Real.Basic
variable (x : ℝ)

example
  (h : ∀ ε > 0, x ≤ ε)
  : x ≤ 0 :=
by sorry

Demostración en lenguaje natural Basta demostrar que \\(x ≯ 0\\). Para ello, supongamos que \\(x > 0\\) y vamos a demostrar que \\[ ¬(∀ε)[ε > 0 → x ≤ ε] \\tag{1} \\] que es una contradicción con la hipótesis. Interiorizando la negación, (1) es equivalente a \\[ (∃ε)[ε > 0 ∧ ε < x] \\tag{2} \\] Para demostrar (2), elegimos \\(ε = \\dfrac{x}{2}\\) ya que, como \\(x > 0\\), se tiene \\[ 0 < \\dfrac{x}{2} < x\\] Demostraciones con Lean4

import Mathlib.Data.Real.Basic

variable (x : ℝ)

-- 1ª demostración
-- ===============

example
  (h : ∀ ε > 0, x ≤ ε)
  : x ≤ 0 :=
by
  apply le_of_not_gt
  -- ⊢ ¬x > 0
  intro hx0
  -- hx0 : x > 0
  -- ⊢ False
  apply absurd h
  -- ⊢ ¬∀ (ε : ℝ), ε > 0 → x ≤ ε
  push_neg
  -- ⊢ ∃ ε, ε > 0 ∧ ε < x
  use x /2
  -- ⊢ x / 2 > 0 ∧ x / 2 < x
  constructor
  { show x / 2 > 0
    exact half_pos hx0 }
  { show x / 2 < x
    exact half_lt_self hx0 }

-- 2ª demostración
-- ===============

example
  (x : ℝ)
  (h : ∀ ε > 0, x ≤ ε)
  : x ≤ 0 :=
by
  contrapose! h
  -- ⊢ ∃ ε, ε > 0 ∧ ε < x
  use x / 2
  -- ⊢ x / 2 > 0 ∧ x / 2 < x
  constructor
  { show x / 2 > 0
    exact half_pos h }
  { show x / 2 < x
    exact half_lt_self h }

-- Lemas usados
-- ============

-- variable (a b : ℝ)
-- variable (p q : Prop)
-- #check (le_of_not_gt : ¬a > b → a ≤ b)
-- #check (half_lt_self : 0 < a → a / 2 < a)
-- #check (half_pos : 0 < a → 0 < a / 2)
-- #check (absurd : p → ¬p → q)

Demostraciones interactivas Se puede interactuar con las demostraciones anteriores en Lean 4 Web. Referencias

J. Avigad y P. Massot. Mathematics in Lean, p. 32.