Si (∀ε > 0)[x ≤ ε], entonces x ≤ 0
Demostrar con Lean4 que si \((∀ε > 0)[x ≤ ε]\), entonces \(x ≤ 0\).
Para ello, completar la siguiente teoría de Lean4:
|
1 2 3 4 5 6 7 |
import Mathlib.Data.Real.Basic variable (x : ℝ) example (h : ∀ ε > 0, x ≤ ε) : x ≤ 0 := by sorry |