Proposition eq_lub {x y : X} (Hx : is_least_upperbound x) (Hy : is_least_upperbound y) : x = y. Proof. pose (x' := (x ,, Hx) : lub). pose (y' := (y ,, Hy) : lub). use (antisymm_PartialOrder PX). - apply (lub_is_least x' y'). exact (lub_is_upperbound y'). - apply (lub_is_least y' x'). exact (lub_is_upperbound x'). Qed.
Require Import UniMath.MoreFoundations.All. Require Import UniMath.OrderTheory.Posets.Basics. Require Import UniMath.OrderTheory.Posets.MonotoneFunctions. Require Import UniMath.OrderTheory.Posets.PointedPosets. Require Import UniMath.OrderTheory.DCPOs.Core.DirectedSets.