TheoremsbiInf_mem, biInf_mem_of_nonempty, codirectedOn, dual, finsetInf'_mem, finsetInf_mem, iInf_mem, iInf_mem_of_nonempty, image, infClosure_eq, insert_lowerBounds, insert_upperBounds, inter, preimage, prod, sInf_mem, sInf_mem_of_nonempty, supClosure, infClosed, dual, image, infClosed, inter, latticeClosure_eq, of_dual, preimage, prod, supClosed, IsSublattice_range, supClosed, infClosed, isSublattice, supClosed, infClosure, latticeClosure, supClosure, biSup_mem, biSup_mem_of_nonempty, directedOn, dual, finsetSup'_mem, finsetSup_mem, iSup_mem, iSup_mem_of_nonempty, image, infClosure, insert_lowerBounds, insert_upperBounds, inter, preimage, prod, sSup_mem, sSup_mem_of_nonempty, supClosure_eq, compl_image_latticeClosure, compl_image_latticeClosure_eq_of_compl_image_eq_self, finsetInf'_mem_infClosure, finsetSup'_mem_supClosure, image_latticeClosure, image_latticeClosure', infClosed_empty, infClosed_iInter, infClosed_infClosure, infClosed_pi, infClosed_preimage_ofDual, infClosed_preimage_toDual, infClosed_range, infClosed_sInter, infClosed_singleton, infClosed_univ, infClosure_empty, infClosure_eq_self, infClosure_idem, infClosure_isClosed, infClosure_min, infClosure_mono, infClosure_prod, infClosure_singleton, infClosure_supClosure, infClosure_univ, inf_mem_infClosure, isGLB_infClosure, isLUB_supClosure, isSublattice_empty, isSublattice_iInter, isSublattice_latticeClosure, isSublattice_pi, isSublattice_preimage_ofDual, isSublattice_preimage_toDual, isSublattice_sInter, isSublattice_singleton, isSublattice_univ, latticeClosure_empty, latticeClosure_eq_self, latticeClosure_idem, latticeClosure_isClosed, latticeClosure_min, latticeClosure_mono, latticeClosure_prod, latticeClosure_singleton, latticeClosure_sup_inf_induction, latticeClosure_univ, lowerBounds_infClosure, ofDual_preimage_latticeClosure, subset_infClosure, subset_latticeClosure, subset_supClosure, supClosed_empty, supClosed_iInter, supClosed_pi, supClosed_preimage_ofDual, supClosed_preimage_toDual, supClosed_range, supClosed_sInter, supClosed_singleton, supClosed_supClosure, supClosed_univ, supClosure_empty, supClosure_eq_self, supClosure_idem, supClosure_infClosure, supClosure_isClosed, supClosure_min, supClosure_mono, supClosure_prod, supClosure_singleton, supClosure_univ, sup_mem_supClosure, upperBounds_supClosure | 129 |