Theorem IsLowerSet.isClosed

Modification history

2025-12-05 15:16

Mathlib/Topology/Order/Basic.lean

chore: add `variable [OrderTopology α]` (#32452)

Modified IsLowerSet.isClosed View on Github →

2025-07-31 15:08

Mathlib/Topology/Order/Basic.lean

feat(Topology/Order/Basic): lower set in well-order is open (#26928) …

Added IsLowerSet.isClosed View on Github →