21 noviembre 2022 – Calculemus

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

PorJosé A. Alonso 21 noviembre 202218 noviembre 2022

Demostrar 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 Lean:

import tactic

variables {α : Type*} [partial_order α]
variables s : set α
variables a b : α

-- (cota_superior s a) expresa que a es una cota superior de s.
def cota_superior (s : set α) (a : α) := ∀ {x}, x ∈ s → x ≤ a

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

import tactic

variables {α : Type*} [partial_order α]

variables s : set α

variables a b : α

-- (cota_superior s a) expresa que a es una cota superior de s.

def cota_superior (s : set α) (a : α) := ∀ {x}, x ∈ s → x ≤ a

example

(h1 : cota_superior s a)

(h2 : a ≤ b)

: cota_superior s b :=

sorry