Theorem IsLowerSet.eq_empty_or_Iic

Modification history

2026-02-21 12:45
Mathlib/Order/UpperLower/Basic.lean
chore(Order/UpperLower/Basic): use `to_dual` (#34640)
Deleted IsLowerSet.eq_empty_or_IicView on Github →
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_empty_or_IicView on Github →