Skip to main content

Si a es una cota superior de s y a ≤ b, entonces b es una cota superior de s

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

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\)]} \newline &≤ 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

-- Demostración en lenguaje natural
-- ================================

-- Tenemos que demostrar que
--    (∀ x) [x ∈ s → x ≤ b]
-- Sea x tal que x ∈ s. Entonces,
--    x ≤ a   [porque a es una cota superior de s]
--      ≤ b
-- Por tanto, x ≤ b.

-- 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