fact: Definition set_join_morphism d (L : completeLatticeType d) d' (L' : completeLatticeType d') (f : L -> L') : Prop := forall S, f (set_join S) = set_join (f @` S).
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype choice order) mathcomp(ssrnat bigop classical_sets)