Commit 2023-06-14 01:28 b1701f82

View on Github →

chore: forward-port leanprover-community/mathlib#18949 (#3918) Match https://github.com/leanprover-community/mathlib/pull/18949 order.hom.lattice@9d684a893c52e1d6692a504a118bfccbae04feeb..7581030920af3dcb241d1df0e36f6ec8289dd6be

Estimated changes

Modified Mathlib/Order/Hom/Lattice.lean

added def InfHom.withBot'

added theorem InfHom.withBot_comp

added theorem InfHom.withBot_id

added def InfHom.withTop'

added theorem InfHom.withTop_comp

added theorem InfHom.withTop_id

added theorem LatticeHom.coe_withBot

added theorem LatticeHom.coe_withTop

added theorem LatticeHom.coe_withTopWithBot

added def LatticeHom.withBot'

added theorem LatticeHom.withBot_apply

added theorem LatticeHom.withBot_comp

added theorem LatticeHom.withBot_id

added def LatticeHom.withTop'

added def LatticeHom.withTopWithBot'

added def LatticeHom.withTopWithBot

added theorem LatticeHom.withTopWithBot_apply

added theorem LatticeHom.withTopWithBot_comp

added theorem LatticeHom.withTopWithBot_id

added theorem LatticeHom.withTop_apply

added theorem LatticeHom.withTop_comp

added theorem LatticeHom.withTop_id

added def SupHom.withBot'

added theorem SupHom.withBot_comp

added theorem SupHom.withBot_id

added def SupHom.withTop'

added theorem SupHom.withTop_comp

added theorem SupHom.withTop_id