No para toda f : ℝ → ℝ monótona, (∀a,b)[f(a) ≤ f(b) → a ≤ b]
Demostrar con Lean4 que no para toda \(f : ℝ → ℝ\) monótona, \((∀a,b)[f(a) ≤ f(b) → a ≤ b]\).
Para ello, completar la siguiente teoría de Lean4:
|
1 2 3 4 5 |
import Mathlib.Data.Real.Basic example : ¬∀ {f : ℝ → ℝ}, Monotone f → ∀ {a b}, f a ≤ f b → a ≤ b := by sorry |
Demostración en lenguaje natural
Supongamos que
\[ (∀f)[f \text{ es monótona } → (∀a, b)[f(a) ≤ f(b) → a ≤ b]] \tag{1} \]
Sea \(f : ℝ → ℝ\) la función constante igual a cero; es decir,
\[ (∀x ∈ ℝ)[f(x) = 0] \]
Entonces, \(f\) es monótona y \(f(1) ≤ f(0)\) (ya que \(f(1) = 0 ≤ 0 = f(0)\)). Luego, por (1), \(1 ≤ 0\) que es una contradicción.
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 |
import Mathlib.Data.Real.Basic -- 1ª demostración -- =============== example : ¬∀ {f : ℝ → ℝ}, Monotone f → ∀ {a b}, f a ≤ f b → a ≤ b := by intro h1 -- h1 : ∀ {f : ℝ → ℝ}, Monotone f → ∀ {a b : ℝ}, f a ≤ f b → a ≤ b -- ⊢ False let f := fun _ : ℝ ↦ (0 : ℝ) have h2 : Monotone f := monotone_const have h3 : f 1 ≤ f 0 := le_refl 0 have h4 : 1 ≤ 0 := h1 h2 h3 linarith -- Lemas usados -- ============ -- variable (a c : ℝ) -- #check (le_refl a : a ≤ a) -- #check (monotone_const : Monotone fun _ : ℝ ↦ c) |
Demostraciones interactivas
Se puede interactuar con las demostraciones anteriores en Lean 4 Web.
Referencias
- J. Avigad y P. Massot. Mathematics in Lean, p. 32.
