Menu Close

Día: 21 de noviembre de 2022

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

José A. Alonso-

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