Commit 2023-10-20 09:11 53ae52b4

View on Github →

fix(Order/Hom): coercion lemmas for lattice and complete lattice (#7796) These are a number of small fixes of coercions of lattices and complete lattices, made by Yaël Dillies in the context of a larger refactor of the branch frametopadjunction. Co-authored by: Yaël Dillies

Estimated changes

Modified Mathlib/Order/Hom/CompleteLattice.lean

added theorem CompleteLatticeHom.coe_mk

added theorem CompleteLatticeHom.coe_toBoundedLatticeHom

added theorem CompleteLatticeHom.coe_tosInfHom

added theorem CompleteLatticeHom.coe_tosSupHom

modified theorem CompleteLatticeHom.toFun_eq_coe

deleted theorem CompleteLatticeHom.toFun_eq_coe_aux

added theorem FrameHom.coe_mk

added theorem FrameHom.coe_toInfTopHom

added theorem FrameHom.coe_toLatticeHom

modified theorem FrameHom.toFun_eq_coe

deleted theorem FrameHom.toFun_eq_coe_aux

added theorem sInfHom.coe_mk

modified theorem sInfHom.toFun_eq_coe

added theorem sSupHom.coe_mk

modified theorem sSupHom.toFun_eq_coe

Modified Mathlib/Order/Hom/Lattice.lean

added theorem BoundedLatticeHom.coe_mk

added theorem BoundedLatticeHom.coe_toBoundedOrderHom

added theorem BoundedLatticeHom.coe_toInfTopHom

modified theorem BoundedLatticeHom.coe_toLatticeHom

added theorem BoundedLatticeHom.coe_toSupBotHom

modified theorem BoundedLatticeHom.toFun_eq_coe

added theorem InfHom.coe_mk

modified theorem InfHom.toFun_eq_coe

added theorem InfTopHom.coe_mk

modified theorem InfTopHom.coe_toInfHom

modified theorem InfTopHom.coe_toTopHom

modified theorem InfTopHom.toFun_eq_coe

added theorem LatticeHom.coe_mk

modified theorem LatticeHom.coe_toInfHom

modified theorem LatticeHom.coe_toSupHom

modified theorem LatticeHom.toFun_eq_coe

added theorem SupBotHom.coe_mk

modified theorem SupBotHom.coe_toBotHom

modified theorem SupBotHom.coe_toSupHom

modified theorem SupBotHom.toFun_eq_coe

added theorem SupHom.coe_mk

modified theorem SupHom.toFun_eq_coe