mathlib
406719e9 - feat(order/hom/lattice): Composition of lattice homs (#11676)

Commit
3 years ago
feat(order/hom/lattice): Composition of lattice homs (#11676) Define `top_hom.comp`, `bot_hom.comp`, `sup_hom.comp`, `inf_hom.comp`, `lattice_hom.comp`, `bounded_lattice_hom.comp`, `order_hom.to_lattice_hom`.
Author
Parents
Loading