Theorem IsLowerSet.eq_univ_or_Iio

Modification history

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