--- Título: La composición de dos funciones monótonas es monótona Autor: José A. Alonso --- Demostrar con Lean4 que la composición de dos funciones monótonas es monótona. Para ello, completar la siguiente teoría de Lean4: 
import Mathlib.Data.Real.Basic

variable (f g : ℝ → ℝ)

example
  (mf : Monotone f)
  (mg : Monotone g)
  : Monotone (f ∘ g) :=
by sorry
Demostración en lenguaje natural [mathjax] Sean \\(f\\) y \\(g\\) dos funciones monótonas de \\(ℝ\\) en \\(ℝ\\). Tenemos que demostrar que \\(f ∘ g\\) es monótona; es decir, que \\[ (∀ a, b ∈ ℝ) [a ≤ b → (f ∘ g)(a) ≤ (f ∘ g)(b)] \\] Sean \\(a, b ∈ ℝ\\) tales que \\(a ≤ b\\). Por ser \\(g\\) monótona, se tiene \\[ g(a) ≤ g(b) \\] y, por ser f monótona, se tiene \\[ f(g(a)) ≤ f(g(b)) \\] Finalmente, por la definición de composición, \\[ (f ∘ g)(a) ≤ (f ∘ g)(b) \\] que es lo que había que demostrar. Demostraciones con Lean4 
import Mathlib.Data.Real.Basic

variable (f g : ℝ → ℝ)

-- 1ª demostración
example
  (mf : Monotone f)
  (mg : Monotone g)
  : Monotone (f ∘ g) :=
by
  have h1 : ∀ a b, a ≤ b → (f ∘ g) a ≤ (f ∘ g) b
  { intros a b hab
    have h1 : g a ≤ g b := mg hab
    show (f ∘ g) a ≤ (f ∘ g) b
    exact mf h1 }
  show Monotone (f ∘ g)
  exact h1

-- 2ª demostración
example
  (mf : Monotone f)
  (mg : Monotone g)
  : Monotone (f ∘ g) :=
by
  have h1 : ∀ a b, a ≤ b → (f ∘ g) a ≤ (f ∘ g) b
  { intros a b hab
    show (f ∘ g) a ≤ (f ∘ g) b
    exact mf (mg hab) }
  show Monotone (f ∘ g)
  exact h1

-- 3ª demostración
example
  (mf : Monotone f)
  (mg : Monotone g)
  : Monotone (f ∘ g) :=
by
  -- a b : ℝ
  -- hab : a ≤ b
  intros a b hab
  -- (f ∘ g) a ≤ (f ∘ g) b
  apply mf
  -- g a ≤ g b
  apply mg
  -- a ≤ b
  apply hab

-- 4ª demostración
example (mf : Monotone f) (mg : Monotone g) :
  Monotone (f ∘ g) :=
λ _ _ hab ↦ mf (mg hab)
Demostraciones interactivas Se puede interactuar con las demostraciones anteriores en Lean 4 Web. Referencias