Commit 2023-09-13 14:53 1bfcb2b7

View on Github →

feat: Linear order on upper/lower sets (#6816) Match https://github.com/leanprover-community/mathlib/pull/19068

Estimated changes

Modified Mathlib/Algebra/Order/UpperLower.lean

modified theorem IsLowerSet.div_left

modified theorem IsLowerSet.div_right

modified theorem IsLowerSet.mul_left

modified theorem IsLowerSet.mul_right

modified theorem IsLowerSet.smul

modified theorem IsUpperSet.smul

Modified Mathlib/Order/UpperLower/Basic.lean

added theorem IsLowerSet.total

added theorem IsUpperSet.total

Modified Mathlib/Topology/Algebra/Order/UpperLower.lean