Theorem IsUpperSet.inv

Modification history

2026-02-21 12:00

Mathlib/Algebra/Order/UpperLower.lean

chore: weaken `PartialOrder` to `Preorder` in `IsOrderedMonoid` hypothesis (#34295) …

Modified IsUpperSet.inv View on Github →

2023-02-10 16:26

Mathlib/Algebra/Order/UpperLower.lean

feat: port Algebra.Order.UpperLower (#2008) …

Added IsUpperSet.inv View on Github →