Commit 2023-02-10 16:26 6cc6f350

View on Github →

feat: port Algebra.Order.UpperLower (#2008) First theory port, please check carefully. All changes after the automated fixes: https://github.com/leanprover-community/mathlib4/pull/2008/files/897cd3a8249a80c9d8140b3e5a7e29fe7a8752df..8abfa80e1f79a24eaf0dc5bedb74afef732888ba.

Estimated changes

added theorem IsLowerSet.div_left
added theorem IsLowerSet.div_right
added theorem IsLowerSet.inv
added theorem IsLowerSet.mul_left
added theorem IsLowerSet.mul_right
added theorem IsLowerSet.smul
added theorem IsLowerSet.smul_subset
added theorem IsUpperSet.div_left
added theorem IsUpperSet.div_right
added theorem IsUpperSet.inv
added theorem IsUpperSet.mul_left
added theorem IsUpperSet.mul_right
added theorem IsUpperSet.smul
added theorem IsUpperSet.smul_subset
added theorem LowerSet.Iic_one
added theorem LowerSet.coe_div
added theorem LowerSet.coe_mul
added theorem Set.OrdConnected.smul
added theorem UpperSet.Ici_one
added theorem UpperSet.coe_div
added theorem UpperSet.coe_mul
added theorem UpperSet.coe_one
added theorem lowerClosure_mul
added theorem lowerClosure_one
added theorem lowerClosure_smul
added theorem mul_lowerClosure
added theorem mul_upperClosure
added theorem upperClosure_mul
added theorem upperClosure_one
added theorem upperClosure_smul