mathlib3

4471de61 - feat(order/lattice): define a lattice structure using an injective map to another lattice (#10615)

feat(order/lattice): define a lattice structure using an injective map to another lattice (#10615) This is done similarly to `function.injective.group` etc. Co-authored-by: Rémy Degenne <remydegenne@gmail.com>