Commit 2024-09-01 19:41 86684572

View on Github →

feat(Order/Hom/Lattice): add Subtype.val as lattice homs (#16270)

Estimated changes

Modified Mathlib/Order/Hom/Lattice.lean

added def BoundedLatticeHom.subtypeVal

added theorem BoundedLatticeHom.subtypeVal_apply

added theorem BoundedLatticeHom.subtypeVal_coe

added def InfHom.subtypeVal

added theorem InfHom.subtypeVal_apply

added theorem InfHom.subtypeVal_coe

added def InfTopHom.subtypeVal

added theorem InfTopHom.subtypeVal_apply

added theorem InfTopHom.subtypeVal_coe

added def LatticeHom.subtypeVal

added theorem LatticeHom.subtypeVal_apply

added theorem LatticeHom.subtypeVal_coe

added def SupBotHom.subtypeVal

added theorem SupBotHom.subtypeVal_apply

added theorem SupBotHom.subtypeVal_coe

added def SupHom.subtypeVal

added theorem SupHom.subtypeVal_apply

added theorem SupHom.subtypeVal_coe