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>

Author: mans0954

src/order/hom/complete_lattice.lean

@@ -626,3 +626,18 @@ See also `complete_lattice_hom.set_preimage`. -/
   right_inv := λ s, by simp only [← image_comp, equiv.self_comp_symm, id.def, image_id'],
   map_rel_iff' :=
     λ s t, ⟨λ h, by simpa using @monotone_image _ _ e.symm _ _ h, λ h, monotone_image h⟩ }
+
+section
+
+variables (α) [complete_lattice α]
+
+/-- The map `(a, b) ↦ a ⊓ b` as an `Inf_hom`. -/
+@[simps] def inf_Inf_hom : Inf_hom (α × α) α :=
+{ to_fun := λ x, x.1 ⊓ x.2,
+  map_Inf' := λ s, by simp_rw [prod.fst_Inf, prod.snd_Inf, Inf_image, infi_inf_eq], }
+
+/-- The map `(a, b) ↦ a ⊔ b` as a `Sup_hom`. -/
+@[simps] def sup_Sup_hom : Sup_hom (α × α) α :=
+{ to_fun := λ x, x.1 ⊔ x.2, map_Sup' := (inf_Inf_hom αᵒᵈ).map_Inf' }
+
+end