Commit 2025-07-31 15:08 53fafe9f

View on Github →

feat(Topology/Order/Basic): lower set in well-order is open (#26928) As well as the other analogous theorems.

Estimated changes

Modified Mathlib/Order/UpperLower/Basic.lean

added theorem IsLowerSet.eq_empty_or_Iic

added theorem IsLowerSet.eq_univ_or_Iio

added theorem IsUpperSet.eq_empty_or_Ici

added theorem IsUpperSet.eq_univ_or_Ioi

Modified Mathlib/Topology/Order/Basic.lean

added theorem IsLowerSet.isClosed

added theorem IsLowerSet.isOpen

added theorem IsUpperSet.isClosed

added theorem IsUpperSet.isOpen