Theorem IsLowerSet.isOpen

Modification history

2025-07-31 15:08
Mathlib/Topology/Order/Basic.lean
feat(Topology/Order/Basic): lower set in well-order is open (#26928) …
Added IsLowerSet.isOpenView on Github →