Theorem Set.iSup_mulIndicator

Modification history

2025-12-08 05:19
Mathlib/Algebra/Order/Group/Indicator.lean
refactor: make `abbrev`s for `IsDirected α (· ≤ ·)` and `IsDirected α (· ≥ ·)` (#32462) …
Modified Set.iSup_mulIndicatorView on Github →
2024-10-07 17:59
Mathlib/Algebra/Order/Group/Indicator.lean
feat: supremum of directed indicators (#17467) …
Added Set.iSup_mulIndicatorView on Github →