mathlib

1f470163 - refactor(order/hom/complete_lattice): Fix the definition of `frame_hom` (#12855)

refactor(order/hom/complete_lattice): Fix the definition of `frame_hom` (#12855) I misread "preserves finite meet" as "preserves binary meet", meaning that currently a `frame_hom` does not have to preserve `⊤` (subtly, preserving arbitrary join does not imply that either). This fixes my mistake.