Theorem iSup_unique

Modification history

2026-09-24 15:23

Mathlib/Order/Bounds/Basic.lean

feat: `OrderSupSet` (#38328) …

Modified iSup_unique View on Github →

2024-07-23 12:07

Mathlib/Order/CompleteLattice.lean

refactor: Make `Frame` extend `HeytingAlgebra` (#10560) …

Added iSup_unique View on Github →