feat: port Topology.Order.Basic (#2052)

Mathlib.lean

@@ -990,6 +990,7 @@ import Mathlib.Topology.Maps
 import Mathlib.Topology.NhdsSet
 import Mathlib.Topology.OmegaCompletePartialOrder
 import Mathlib.Topology.Order
+import Mathlib.Topology.Order.Basic
 import Mathlib.Topology.Paracompact
 import Mathlib.Topology.Separation
 import Mathlib.Topology.SubsetProperties

Mathlib/Data/Set/Countable.lean

@@ -221,6 +221,9 @@ theorem Countable.union {s t : Set α} (hs : s.Countable) (ht : t.Countable) : (
   countable_union.2 ⟨hs, ht⟩
 #align set.countable.union Set.Countable.union
 
+theorem Countable.of_diff {s t : Set α} (h : (s \ t).Countable) (ht : t.Countable) : s.Countable :=
+  (h.union ht).mono (subset_diff_union _ _)
+
 @[simp]
 theorem countable_insert {s : Set α} {a : α} : (insert a s).Countable ↔ s.Countable := by
   simp only [insert_eq, countable_union, countable_singleton, true_and_iff]

Mathlib/Order/Cover.lean

@@ -457,6 +457,15 @@ theorem Covby.eq_of_between {x : α} (hab : a ⋖ b) (hbc : b ⋖ c) (hax : a <
   le_antisymm (le_of_not_lt fun h => hbc.2 h hxc) (le_of_not_lt <| hab.2 hax)
 #align covby.eq_of_between Covby.eq_of_between
 
+/-- If `a < b` then there exist `a' > a` and `b' < b` such that `Set.Iio a'` is strictly to the left
+of `Set.Ioi b'`. -/
+lemma LT.lt.exists_disjoint_Iio_Ioi (h : a < b) :
+    ∃ a' > a, ∃ b' < b, ∀ x < a', ∀ y > b', x < y := by
+  by_cases h' : a ⋖ b
+  · exact ⟨b, h, a, h, fun x hx y hy => hx.trans_le <| h'.ge_of_gt hy⟩
+  · rcases h.exists_lt_lt h' with ⟨c, ha, hb⟩
+    exact ⟨c, ha, c, hb, fun _ h₁ _ => lt_trans h₁⟩
+
 end LinearOrder
 
 namespace Set

Mathlib/Topology/ContinuousOn.lean

@@ -119,12 +119,8 @@ theorem nhds_of_nhdsWithin_of_nhds {s t : Set α} {a : α} (h1 : s ∈ 𝓝 a) (
 #align nhds_of_nhds_within_of_nhds nhds_of_nhdsWithin_of_nhds
 
 theorem mem_nhdsWithin_iff_eventually {s t : Set α} {x : α} :
-    t ∈ 𝓝[s] x ↔ ∀ᶠ y in 𝓝 x, y ∈ s → y ∈ t := by
-  rw [mem_nhdsWithin_iff_exists_mem_nhds_inter]
-  constructor
-  · rintro ⟨u, hu, hut⟩
-    exact eventually_of_mem hu fun x hxu hxs => hut ⟨hxu, hxs⟩
-  · refine' fun h => ⟨_, h, fun y hy => hy.1 hy.2⟩
+    t ∈ 𝓝[s] x ↔ ∀ᶠ y in 𝓝 x, y ∈ s → y ∈ t :=
+  eventually_inf_principal
 #align mem_nhds_within_iff_eventually mem_nhdsWithin_iff_eventually
 
 theorem mem_nhdsWithin_iff_eventuallyEq {s t : Set α} {x : α} :
@@ -271,6 +267,10 @@ theorem nhdsWithin_inter_of_mem {a : α} {s t : Set α} (h : s ∈ 𝓝[t] a) :
   exact nhdsWithin_le_of_mem h
 #align nhds_within_inter_of_mem nhdsWithin_inter_of_mem
 
+-- porting note: new lemma
+theorem nhdsWithin_inter_of_mem' {a : α} {s t : Set α} (h : t ∈ 𝓝[s] a) : 𝓝[s ∩ t] a = 𝓝[s] a := by
+  rw [inter_comm, nhdsWithin_inter_of_mem h]
+
 @[simp]
 theorem nhdsWithin_singleton (a : α) : 𝓝[{a}] a = pure a := by
   rw [nhdsWithin, principal_singleton, inf_eq_right.2 (pure_le_nhds a)]