Mathlib v3 is deprecated. Go to Mathlib v4

Def complete_lattice_hom.to_Inf_hom

Modification history

2022-03-22 14:24
src/order/hom/complete_lattice.lean
refactor(order/hom/complete_lattice): Fix the definition of `frame_hom` (#12855) …
Deleted complete_lattice_hom.to_Inf_homView on Github →
2022-01-31 14:14
src/order/hom/complete_lattice.lean
feat(order/hom/complete_lattice): Complete lattice homomorphisms (#11741) …
Added complete_lattice_hom.to_Inf_homView on Github →