mathlib
80591d65 - feat(order/hom/lattice): Finitary join-/meet-preserving maps (#12149)

Commit
3 years ago
feat(order/hom/lattice): Finitary join-/meet-preserving maps (#12149) Define `sup_bot_hom`, `inf_top_hom` and their associated class.
Author
Parents
Loading