Commit 2023-01-09 19:56 c8a43b45

feat(order/hom/complete_lattice): inf as an Inf_hom and sup as a Sup_hom (#18023) Introduces a new definition inf_Inf_hom on a complete lattice which is the map (a, b) ↦ a ⊓ b as an Inf_hom. This is required for #17426. For completeness we also include the equivalent sup definition.