Definition complete_lattice_from_glb {X : hSet} (L : lattice X) (H : ∏ (I : UU) (f : I → X), ∑ (x : X), is_greatest_lowerbound_lattice L f x) : is_complete_lattice L. Proof. intros I f. pose (lub := H (∑ (x : X), ∏ (i : I), Lle L (f i) x) pr1). refine (pr1 lub ,, _). split. - abstract (intros i ; use (pr22 lub) ; intros p ; exact (pr2 p i)). - abstract (intros x Hx ; exact (pr12 lub (x ,, Hx))). Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.OrderTheory.Lattice.Lattice. Require Import UniMath.OrderTheory.Lattice.Bounded. Require Import UniMath.OrderTheory.Lattice.Heyting.