23 octubre 2023 – Calculemus

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

PorJosé A. Alonso 23 octubre 202318 octubre 2023

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

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