--- Título: Si f no es monótona, entonces ∃x∃y[x ≤ y ∧ f(y) < f(x)]. Autor: José A. Alonso --- [mathjax] Demostrar con Lean4 que si \\(f\\) no es monótona, entonces ()∃x∃y[x ≤ y ∧ f(y) < f(x)]\\). Para ello, completar la siguiente teoría de Lean4:

import Mathlib.Tactic
variable (f : ℝ → ℝ)

example
  (h : ¬Monotone f)
  : ∃ x y, x ≤ y ∧ f y < f x :=
by sorry

Demostración en lenguaje natural Usaremos los siguientes lemas: \\begin{align} &¬(∀x)P(x) ↔ (∃ x)¬P(x) \\tag{L1} \\\\ &¬(p → q) ↔ p ∧ ¬q \\tag{L2} \\\\ &(∀a, b ∈ ℝ)[¬b ≤ a → a < b] \\tag{L3} \\end{align} Por la definición de función monótona, \\[ ¬(∀x)(∀y)[x ≤ y → f(x) ≤ f(y)] \\] Aplicando L1 se tiene \\[ (∃x)¬(∀y)[x ≤ y → f(x) ≤ f(y)] \\] Sea \\(a\\) tal que \\[ ¬(∀y)[a ≤ y → f(a) ≤ f(y)] \\] Aplicando L1 se tiene \\[ (∃y)¬[a ≤ y → f(a) ≤ f(y)] \\] Sea \\(b\\) tal que \\[ ¬[a ≤ b → f(a) ≤ f(b)] \\] Aplicando L2 se tiene que \\[ a ≤ b ∧ ¬(f(a) ≤ f(b)) \\] Aplicando L3 se tiene que \\[ a ≤ b ∧ f(b) < f(a) \\] Por tanto, \\[ (∃x,y)[x ≤ y ∧ f(y) < f(x)] \\] Demostraciones con Lean4

import Mathlib.Tactic
variable (f : ℝ → ℝ)

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

example
  (h : ¬Monotone f)
  : ∃ x y, x ≤ y ∧ f y < f x :=
by
  have h1 : ¬∀ x y, x ≤ y → f x ≤ f y := h
  have h2 : ∃ x, ¬(∀ y, x ≤ y → f x ≤ f y) := not_forall.mp h1
  rcases h2 with ⟨a, ha : ¬∀ y, a ≤ y → f a ≤ f y⟩
  have h3 : ∃ y, ¬(a ≤ y → f a ≤ f y) := not_forall.mp ha
  rcases h3 with ⟨b, hb : ¬(a ≤ b → f a ≤ f b)⟩
  have h4 : a ≤ b ∧ ¬(f a ≤ f b) := not_imp.mp hb
  have h5 : a ≤ b ∧ f b < f a := ⟨h4.1, lt_of_not_le h4.2⟩
  use a, b
  -- ⊢ a ≤ b ∧ f b < f a
  exact h5

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

example
  (h : ¬Monotone f)
  : ∃ x y, x ≤ y ∧ f y < f x :=
by
  simp only [Monotone] at h
  -- h : ¬∀ ⦃a b : ℝ⦄, a ≤ b → f a ≤ f b
  push_neg at h
  -- h : Exists fun ⦃a⦄ => Exists fun ⦃b⦄ => a ≤ b ∧ f b < f a
  exact h

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

-- variable {α : Type _}
-- variable (P : α → Prop)
-- variable (p q : Prop)
-- variable (a b : ℝ)
-- #check (not_forall : (¬∀ x, P x) ↔ ∃ x, ¬P x)
-- #check (not_imp : ¬(p → q) ↔ p ∧ ¬q)
-- #check (lt_of_not_le : ¬b ≤ a → a < b)

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

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