Commit 2025-12-18 18:46 4e096a83
View on Github →feat(Order/Hom/Basic): use to_dual (#33036)
This PR uses to_dual for order homomorphisms. To make this work, instances of FunLike (α ↪o β) α β and FunLike (α ≃o β) α β have to be added, to override the RelEmbedding/RelIso instances.
Two declarations in other files were given a to_dual existing to make this work. These can be turned into to_dual in future PRs.
The theorems about Disjoint/Codisjoint are not tagged, because Disjoint/Codisjoint have not been tagged jet.