--- Título: Si a es una cota superior de s y a ≤ b, entonces b es una cota superior de s Autor: José A. Alonso --- Demostrar con Lean4 que si \\(a\\) es una cota superior de \\(s\\) y \\(a ≤ b\\), entonces \\(b\\) es una cota superior de \\(s\\). Para ello, completar la siguiente teoría de Lean4:

import Mathlib.Tactic

variable {α : Type _} [PartialOrder α]
variable (s : Set α)
variable (a b : α)

-- (CotaSupConj s a) afirma que a es una cota superior del conjunto s.
def CotaSupConj (s : Set α) (a : α) :=
  ∀ {x}, x ∈ s → x ≤ a

example
  (h1 : CotaSupConj s a)
  (h2 : a ≤ b)
  : CotaSupConj s b :=
by sorry

Demostración en lenguaje natural [mathjax] Tenemos que demostrar que \\[ (∀ x) [x ∈ s → x ≤ b] \\] Sea \\(x\\) tal que \\(x ∈ s\\). Entonces, \\begin{align} x &≤ a &&\\text{[porque \\(a\\) es una cota superior de \\(s\\)]} \\\\ &≤ b \\end{align} Por tanto, \\(x ≤ b\\). Demostraciones con Lean4

import Mathlib.Tactic

variable {α : Type _} [PartialOrder α]
variable (s : Set α)
variable (a b : α)

-- (CotaSupConj s a) afirma que a es una cota superior del conjunto s.
def CotaSupConj (s : Set α) (a : α) :=
  ∀ {x}, x ∈ s → x ≤ a

-- 1ª demostración
example
  (h1 : CotaSupConj s a)
  (h2 : a ≤ b)
  : CotaSupConj s b :=
by
  intro x (xs : x ∈ s)
  have h3 : x ≤ a := h1 xs
  show x ≤ b
  exact le_trans h3 h2

-- 2ª demostración
example
  (h1 : CotaSupConj s a)
  (h2 : a ≤ b)
  : CotaSupConj s b :=
by
  intro x (xs : x ∈ s)
  calc x ≤ a := h1 xs
       _ ≤ b := h2
-
-- Lemas usados
-- ============

-- variable (c : α)
-- #check (le_trans : a ≤ b → b ≤ c → a ≤ c)

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

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