fact: Definition set_f_is_glb d (T : porderType d) (set_f : set T -> T) := forall S, lbound S (set_f S) /\ forall x, lbound S x -> x <= set_f S.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype choice order) mathcomp(ssrnat bigop classical_sets)