mathlib3

c8a43b45 - feat(order/hom/complete_lattice): inf as an Inf_hom and sup as a Sup_hom (#18023)

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. Co-authored-by: Christopher Hoskin <mans0954@users.noreply.github.com>