mathlib3

20aae835 - feat(order/hom/lattice): Lattice homomorphisms (#11610)

feat(order/hom/lattice): Lattice homomorphisms (#11610) This defines (bounded) lattice homomorphisms using the `fun_like` along with weaker homomorphisms that only preserve `sup`, `inf`, `top`, `bot`.