Commit 2023-02-08 08:44 1171386d

View on Github →

feat: port Order.UpperLower.Hom (#2154)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Order/UpperLower/Hom.lean

added theorem LowerSet.coe_iicInfHom

added theorem LowerSet.coe_iicInfₛHom

added def LowerSet.iicInfHom

added theorem LowerSet.iicInfHom_apply

added def LowerSet.iicInfₛHom

added theorem LowerSet.iicInfₛHom_apply

added theorem UpperSet.coe_iciSupHom

added theorem UpperSet.coe_iciSupₛHom

added def UpperSet.iciSupHom

added theorem UpperSet.iciSupHom_apply

added def UpperSet.iciSupₛHom

added theorem UpperSet.iciSupₛHom_apply