Mathlib v3 is deprecated. Go to Mathlib v4

Def complete_lattice_hom.to_bounded_lattice_hom

Modification history

2022-03-01 02:55

src/order/hom/complete_lattice.lean

feat(order/category/CompleteLattice): The category of complete lattices (#12348) …

Added complete_lattice_hom.to_bounded_lattice_hom View on Github →