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

As well as the other analogous theorems.

Author: vihdzp

Mathlib/Order/UpperLower/Basic.lean

@@ -6,6 +6,7 @@ Authors: Yaël Dillies, Sara Rousta
 import Mathlib.Logic.Equiv.Set
 import Mathlib.Order.Interval.Set.OrderEmbedding
 import Mathlib.Order.SetNotation
+import Mathlib.Order.WellFounded
 
 /-!
 # Properties of unbundled upper/lower sets
@@ -353,4 +354,23 @@ theorem IsUpperSet.total (hs : IsUpperSet s) (ht : IsUpperSet t) : s ⊆ t ∨ t
 theorem IsLowerSet.total (hs : IsLowerSet s) (ht : IsLowerSet t) : s ⊆ t ∨ t ⊆ s :=
   hs.toDual.total ht.toDual
 
+theorem IsUpperSet.eq_empty_or_Ici [WellFoundedLT α] (h : IsUpperSet s) :
+    s = ∅ ∨ (∃ a, s = Set.Ici a) := by
+  refine or_iff_not_imp_left.2 fun ha ↦ ?_
+  obtain ⟨a, ha⟩ := Set.nonempty_iff_ne_empty.2 ha
+  exact ⟨_, Set.ext fun b ↦ ⟨wellFounded_lt.min_le, (h · <| wellFounded_lt.min_mem _ ⟨a, ha⟩)⟩⟩
+
+theorem IsLowerSet.eq_empty_or_Iic [WellFoundedGT α] (h : IsLowerSet s) :
+    s = ∅ ∨ (∃ a, s = Set.Iic a) :=
+  IsUpperSet.eq_empty_or_Ici (α := αᵒᵈ) h
+
+theorem IsLowerSet.eq_univ_or_Iio [WellFoundedLT α] (h : IsLowerSet s) :
+    s = .univ ∨ (∃ a, s = Set.Iio a) := by
+  simp_rw [← @compl_inj_iff _ s]
+  simpa using h.compl.eq_empty_or_Ici
+
+theorem IsUpperSet.eq_univ_or_Ioi [WellFoundedGT α] (h : IsUpperSet s) :
+    s = .univ ∨ (∃ a, s = Set.Ioi a) :=
+  IsLowerSet.eq_univ_or_Iio (α := αᵒᵈ) h
+
 end LinearOrder

Mathlib/Topology/Order/Basic.lean

@@ -448,6 +448,23 @@ theorem dense_of_exists_between [OrderTopology α] [Nontrivial α] {s : Set α}
   obtain ⟨x, xs, hx⟩ : ∃ x ∈ s, a < x ∧ x < b := h hab
   exact ⟨x, ⟨H hx, xs⟩⟩
 
+theorem IsUpperSet.isClosed [OrderTopology α] [WellFoundedLT α] {s : Set α} (h : IsUpperSet s) :
+    IsClosed s := by
+  obtain rfl | ⟨a, rfl⟩ := h.eq_empty_or_Ici
+  exacts [isClosed_empty, isClosed_Ici]
+
+theorem IsLowerSet.isClosed [OrderTopology α] [WellFoundedGT α] {s : Set α} (h : IsLowerSet s) :
+    IsClosed s :=
+  h.toDual.isClosed
+
+theorem IsLowerSet.isOpen [OrderTopology α] [WellFoundedLT α] {s : Set α} (h : IsLowerSet s) :
+    IsOpen s := by
+  simpa using h.compl.isClosed
+
+theorem IsUpperSet.isOpen [OrderTopology α] [WellFoundedGT α] {s : Set α} (h : IsUpperSet s) :
+    IsOpen s :=
+  h.toDual.isOpen
+
 /-- A set in a nontrivial densely linear ordered type is dense in the sense of topology if and only
 if for any `a < b` there exists `c ∈ s`, `a < c < b`. Each implication requires less typeclass
 assumptions. -/