feat(Topology/Order): assorted lemmas (#10556)

* Add `upperBounds_closure`, `lowerBounds_closure`, `bddAbove_closure`, `bddBelow_closure`.
* Add `IsAntichain.interior_eq_empty`.
* Generalize `nhds_left'_le_nhds_ne` and `nhds_right'_le_nhds_ne` to a `Preorder`.

Partly forward-ports leanprover-community/mathlib3#16976

Mathlib/Data/Set/Intervals/UnorderedInterval.lean

@@ -7,7 +7,7 @@ import Mathlib.Data.Set.Intervals.Image
 import Mathlib.Order.Bounds.Basic
 import Mathlib.Tactic.Common
 
-#align_import data.set.intervals.unordered_interval from "leanprover-community/mathlib"@"4020ddee5b4580a409bfda7d2f42726ce86ae674"
+#align_import data.set.intervals.unordered_interval from "leanprover-community/mathlib"@"3ba15165bd6927679be7c22d6091a87337e3cd0c"
 
 /-!
 # Intervals without endpoints ordering

Mathlib/Order/Bounds/Basic.lean

@@ -7,7 +7,7 @@ import Mathlib.Data.Set.Intervals.Basic
 import Mathlib.Data.Set.NAry
 import Mathlib.Order.Directed
 
-#align_import order.bounds.basic from "leanprover-community/mathlib"@"ffde2d8a6e689149e44fd95fa862c23a57f8c780"
+#align_import order.bounds.basic from "leanprover-community/mathlib"@"b1abe23ae96fef89ad30d9f4362c307f72a55010"
 
 /-!
 # Upper / lower bounds
@@ -90,6 +90,12 @@ theorem mem_lowerBounds : a ∈ lowerBounds s ↔ ∀ x ∈ s, a ≤ x :=
   Iff.rfl
 #align mem_lower_bounds mem_lowerBounds
 
+lemma mem_upperBounds_iff_subset_Iic : a ∈ upperBounds s ↔ s ⊆ Iic a := Iff.rfl
+#align mem_upper_bounds_iff_subset_Iic mem_upperBounds_iff_subset_Iic
+
+lemma mem_lowerBounds_iff_subset_Ici : a ∈ lowerBounds s ↔ s ⊆ Ici a := Iff.rfl
+#align mem_lower_bounds_iff_subset_Ici mem_lowerBounds_iff_subset_Ici
+
 theorem bddAbove_def : BddAbove s ↔ ∃ x, ∀ y ∈ s, y ≤ x :=
   Iff.rfl
 #align bdd_above_def bddAbove_def

Mathlib/Topology/Algebra/Order/LeftRight.lean

@@ -63,6 +63,29 @@ instance nhdsWithin_Iic_self_neBot (a : α) : NeBot (𝓝[≤] a) :=
   nhdsWithin_Iic_neBot (le_refl a)
 #align nhds_within_Iic_self_ne_bot nhdsWithin_Iic_self_neBot
 
+theorem nhds_left'_le_nhds_ne (a : α) : 𝓝[<] a ≤ 𝓝[≠] a :=
+  nhdsWithin_mono a fun _ => ne_of_lt
+#align nhds_left'_le_nhds_ne nhds_left'_le_nhds_ne
+
+theorem nhds_right'_le_nhds_ne (a : α) : 𝓝[>] a ≤ 𝓝[≠] a :=
+  nhdsWithin_mono a fun _ => ne_of_gt
+#align nhds_right'_le_nhds_ne nhds_right'_le_nhds_ne
+
+-- TODO: add instances for `NeBot (𝓝[<] x)` on (indexed) product types
+
+lemma IsAntichain.interior_eq_empty [∀ x : α, (𝓝[<] x).NeBot] {s : Set α}
+    (hs : IsAntichain (· ≤ ·) s) : interior s = ∅ := by
+  refine eq_empty_of_forall_not_mem fun x hx ↦ ?_
+  have : ∀ᶠ y in 𝓝 x, y ∈ s := mem_interior_iff_mem_nhds.1 hx
+  rcases this.exists_lt with ⟨y, hyx, hys⟩
+  exact hs hys (interior_subset hx) hyx.ne hyx.le
+#align is_antichain.interior_eq_empty IsAntichain.interior_eq_empty
+
+lemma IsAntichain.interior_eq_empty' [∀ x : α, (𝓝[>] x).NeBot] {s : Set α}
+    (hs : IsAntichain (· ≤ ·) s) : interior s = ∅ :=
+  have : ∀ x : αᵒᵈ, NeBot (𝓝[<] x) := ‹_›
+  hs.to_dual.interior_eq_empty
+
 end Preorder
 
 section PartialOrder
@@ -79,14 +102,6 @@ theorem continuousWithinAt_Iio_iff_Iic {a : α} {f : α → β} :
   @continuousWithinAt_Ioi_iff_Ici αᵒᵈ _ _ _ _ _ f
 #align continuous_within_at_Iio_iff_Iic continuousWithinAt_Iio_iff_Iic
 
-theorem nhds_left'_le_nhds_ne (a : α) : 𝓝[<] a ≤ 𝓝[≠] a :=
-  nhdsWithin_mono a fun _ => ne_of_lt
-#align nhds_left'_le_nhds_ne nhds_left'_le_nhds_ne
-
-theorem nhds_right'_le_nhds_ne (a : α) : 𝓝[>] a ≤ 𝓝[≠] a :=
-  nhdsWithin_mono a fun _ => ne_of_gt
-#align nhds_right'_le_nhds_ne nhds_right'_le_nhds_ne
-
 end PartialOrder
 
 section TopologicalSpace

Mathlib/Topology/Algebra/Order/UpperLower.lean

@@ -6,7 +6,7 @@ Authors: Yaël Dillies
 import Mathlib.Algebra.Order.UpperLower
 import Mathlib.Topology.Algebra.Group.Basic
 
-#align_import topology.algebra.order.upper_lower from "leanprover-community/mathlib"@"c0c52abb75074ed8b73a948341f50521fbf43b4c"
+#align_import topology.algebra.order.upper_lower from "leanprover-community/mathlib"@"b1abe23ae96fef89ad30d9f4362c307f72a55010"
 
 /-!
 # Topological facts about upper/lower/order-connected sets

Mathlib/Topology/Order/OrderClosed.lean

@@ -96,9 +96,20 @@ theorem Dense.orderDual [TopologicalSpace α] {s : Set α} (hs : Dense s) :
   hs
 #align dense.order_dual Dense.orderDual
 
+section General
+variable [TopologicalSpace α] [Preorder α] {s : Set α}
+
+protected lemma BddAbove.of_closure : BddAbove (closure s) → BddAbove s :=
+  BddAbove.mono subset_closure
+
+protected lemma BddBelow.of_closure : BddBelow (closure s) → BddBelow s :=
+  BddBelow.mono subset_closure
+
+end General
+
 section ClosedIicTopology
 
-variable [TopologicalSpace α] [Preorder α] [t : ClosedIicTopology α]
+variable [TopologicalSpace α] [Preorder α] [ClosedIicTopology α] {s : Set α}
 
 instance : ClosedIciTopology αᵒᵈ where
   isClosed_ge' a := isClosed_le' (α := α) a
@@ -126,11 +137,23 @@ theorem le_of_tendsto' {f : β → α} {a b : α} {x : Filter β} [NeBot x] (lim
   le_of_tendsto lim (eventually_of_forall h)
 #align le_of_tendsto' le_of_tendsto'
 
+@[simp] lemma upperBounds_closure (s : Set α) : upperBounds (closure s : Set α) = upperBounds s :=
+  ext fun a ↦ by simp_rw [mem_upperBounds_iff_subset_Iic, isClosed_Iic.closure_subset_iff]
+#align upper_bounds_closure upperBounds_closure
+
+@[simp] lemma bddAbove_closure : BddAbove (closure s) ↔ BddAbove s := by
+  simp_rw [BddAbove, upperBounds_closure]
+#align bdd_above_closure bddAbove_closure
+
+protected alias ⟨_, BddAbove.closure⟩ := bddAbove_closure
+#align bdd_above.of_closure BddAbove.of_closure
+#align bdd_above.closure BddAbove.closure
+
 end ClosedIicTopology
 
 section ClosedIciTopology
 
-variable [TopologicalSpace α] [Preorder α] [t : ClosedIciTopology α]
+variable [TopologicalSpace α] [Preorder α] [ClosedIciTopology α] {s : Set α}
 
 instance : ClosedIicTopology αᵒᵈ where
   isClosed_le' a := isClosed_ge' (α := α) a
@@ -158,6 +181,18 @@ theorem ge_of_tendsto' {f : β → α} {a b : α} {x : Filter β} [NeBot x] (lim
   ge_of_tendsto lim (eventually_of_forall h)
 #align ge_of_tendsto' ge_of_tendsto'
 
+@[simp] lemma lowerBounds_closure (s : Set α) : lowerBounds (closure s : Set α) = lowerBounds s :=
+  ext fun a ↦ by simp_rw [mem_lowerBounds_iff_subset_Ici, isClosed_Ici.closure_subset_iff]
+#align lower_bounds_closure lowerBounds_closure
+
+@[simp] lemma bddBelow_closure : BddBelow (closure s) ↔ BddBelow s := by
+  simp_rw [BddBelow, lowerBounds_closure]
+#align bdd_below_closure bddBelow_closure
+
+protected alias ⟨_, BddBelow.closure⟩ := bddBelow_closure
+#align bdd_below.of_closure BddBelow.of_closure
+#align bdd_below.closure BddBelow.closure
+
 end ClosedIciTopology
 
 section OrderClosedTopology