Commit 2022-03-22 14:24 1f470163
View on Github →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.