feat(topology/algebra/order/basic): in a second-countable linear order, only countably many points are isolated to the right (#14564)

This makes it possible to remove a useless `densely_ordered` assumption in a lemma in `borel_space`.

Author: sgouezel

src/data/set/basic.lean

@@ -389,8 +389,7 @@ theorem eq_empty_of_is_empty [is_empty α] (s : set α) : s = ∅ :=
 eq_empty_of_subset_empty $ λ x hx, is_empty_elim x
 
 /-- There is exactly one set of a type that is empty. -/
--- TODO[gh-6025]: make this an instance once safe to do so
-def unique_empty [is_empty α] : unique (set α) :=
+instance unique_empty [is_empty α] : unique (set α) :=
 { default := ∅, uniq := eq_empty_of_is_empty }
 
 lemma not_nonempty_iff_eq_empty {s : set α} : ¬s.nonempty ↔ s = ∅ :=

src/data/set/countable.lean

@@ -187,6 +187,10 @@ countable_insert.2 h
 lemma finite.countable {s : set α} : s.finite → countable s
 | ⟨h⟩ := trunc.nonempty (by exactI fintype.trunc_encodable s)
 
+@[nontriviality] lemma countable.of_subsingleton [subsingleton α] (s : set α) :
+  countable s :=
+(finite.of_subsingleton s).countable
+
 lemma subsingleton.countable {s : set α} (hs : s.subsingleton) : countable s :=
 hs.finite.countable
 

src/data/set/finite.lean

@@ -337,6 +337,9 @@ section set_finite_constructors
 theorem finite.of_fintype [fintype α] (s : set α) : s.finite :=
 by { classical, apply finite_of_fintype }
 
+@[nontriviality] lemma finite.of_subsingleton [subsingleton α] (s : set α) : s.finite :=
+finite.of_fintype s
+
 theorem finite_univ [fintype α] : (@univ α).finite := finite_of_fintype _
 
 theorem finite.union {s t : set α} (hs : s.finite) (ht : t.finite) : (s ∪ t).finite :=

src/measure_theory/constructions/borel_space.lean

@@ -1136,7 +1136,7 @@ lemma ae_measurable_restrict_of_antitone_on [linear_order β] [order_closed_topo
   ae_measurable f (μ.restrict s) :=
 @ae_measurable_restrict_of_monotone_on αᵒᵈ β _ _ ‹_› _ _ _ _ _ ‹_› _ _ _ _ hs _ hf
 
-lemma measurable_set_of_mem_nhds_within_Ioi_aux [densely_ordered α]
+lemma measurable_set_of_mem_nhds_within_Ioi_aux
   {s : set α} (h : ∀ x ∈ s, s ∈ 𝓝[>] x) (h' : ∀ x ∈ s, ∃ y, x < y) :
   measurable_set s :=
 begin
@@ -1159,12 +1159,11 @@ begin
       have : x ∈ interior s :=
         mem_interior.2 ⟨Ioo x' (y x'), h'y _ hx'.1, is_open_Ioo, ⟨h', hz.1.trans h'z.2⟩⟩,
       exact false.elim (hx.2 this) } },
-  apply B.countable_of_is_open (λ x hx, is_open_Ioo) (λ x hx, _),
-  simpa using hy x hx.1
+  exact B.countable_of_Ioo (λ x hx, hy x hx.1),
 end
 
 /-- If a set is a right-neighborhood of all of its points, then it is measurable. -/
-lemma measurable_set_of_mem_nhds_within_Ioi [densely_ordered α] {s : set α}
+lemma measurable_set_of_mem_nhds_within_Ioi {s : set α}
   (h : ∀ x ∈ s, s ∈ 𝓝[>] x) : measurable_set s :=
 begin
   by_cases H : ∃ x ∈ s, is_top x,

src/measure_theory/integral/set_to_l1.lean

@@ -673,9 +673,7 @@ lemma set_to_simple_func_const (T : set α → F →L[ℝ] F') (hT_empty : T ∅
   simple_func.set_to_simple_func T (simple_func.const α x) = T univ x :=
 begin
   casesI hα : is_empty_or_nonempty α,
-  { have h_univ_empty : (univ : set α) = ∅,
-    { haveI : unique (set α) := unique_empty,
-      exact subsingleton.elim (univ : set α) (∅ : set α), },
+  { have h_univ_empty : (univ : set α) = ∅, from subsingleton.elim _ _,
     rw [h_univ_empty, hT_empty],
     simp only [set_to_simple_func, continuous_linear_map.zero_apply, sum_empty,
       range_eq_empty_of_is_empty], },

src/topology/algebra/order/basic.lean

@@ -1157,6 +1157,94 @@ lemma filter.eventually.exists_Ioo_subset [no_max_order α] [no_min_order α] {a
   ∃ l u, a ∈ Ioo l u ∧ Ioo l u ⊆ {x | p x} :=
 mem_nhds_iff_exists_Ioo_subset.1 hp
 
+/-- The set of points which are isolated on the right is countable when the space is
+second-countable. -/
+lemma countable_of_isolated_right [second_countable_topology α] :
+  set.countable {x : α | ∃ y, x < y ∧ Ioo x y = ∅} :=
+begin
+  nontriviality α,
+  let s := {x : α | ∃ y, x < y ∧ Ioo x y = ∅},
+  have : ∀ x ∈ s, ∃ y, x < y ∧ Ioo x y = ∅ := λ x, id,
+  choose! y hy h'y using this,
+  have Hy : ∀ x z, x ∈ s → z < y x → z ≤ x,
+  { assume x z xs hz,
+    have A : Ioo x (y x) = ∅ := h'y _ xs,
+    contrapose! A,
+    exact ne_empty_iff_nonempty.2 ⟨z, A, hz⟩ },
+  suffices H : ∀ (a : set α), is_open a → set.countable {x | x ∈ s ∧ x ∈ a ∧ y x ∉ a},
+  { have : s ⊆ ⋃ (a ∈ countable_basis α), {x | x ∈ s ∧ x ∈ a ∧ y x ∉ a},
+    { assume x hx,
+      rcases (is_basis_countable_basis α).exists_mem_of_ne (hy x hx).ne with ⟨a, ab, xa, ya⟩,
+      simp only [mem_set_of_eq, mem_Union],
+      exact ⟨a, ab, hx, xa, ya⟩ },
+    apply countable.mono this,
+    refine countable.bUnion (countable_countable_basis α) (λ a ha, H _ _),
+    exact is_open_of_mem_countable_basis ha },
+  assume a ha,
+  suffices H : set.countable {x | x ∈ s ∧ x ∈ a ∧ y x ∉ a ∧ ¬(is_bot x)},
+  { have : {x | x ∈ s ∧ x ∈ a ∧ y x ∉ a} ⊆
+      {x | x ∈ s ∧ x ∈ a ∧ y x ∉ a ∧ ¬(is_bot x)} ∪ {x | is_bot x},
+    { assume x hx,
+      by_cases h'x : is_bot x,
+      { simp only [h'x, mem_set_of_eq, mem_union_eq, not_true, and_false, false_or] },
+      { simpa only [h'x, hx.2.1, hx.2.2, mem_set_of_eq, mem_union_eq,
+          not_false_iff, and_true, or_false] using hx.left } },
+    exact countable.mono this (H.union (subsingleton_is_bot α).countable) },
+  let t := {x | x ∈ s ∧ x ∈ a ∧ y x ∉ a ∧ ¬(is_bot x)},
+  have : ∀ x ∈ t, ∃ z < x, Ioc z x ⊆ a,
+  { assume x hx,
+    apply exists_Ioc_subset_of_mem_nhds (ha.mem_nhds hx.2.1),
+    simpa only [is_bot, not_forall, not_le] using hx.right.right.right },
+  choose! z hz h'z using this,
+  have : pairwise_disjoint t (λ x, Ioc (z x) x),
+  { assume x xt x' x't hxx',
+    rcases lt_or_gt_of_ne hxx' with h'|h',
+    { refine disjoint_left.2 (λ u ux ux', xt.2.2.1 _),
+      refine h'z x' x't ⟨ux'.1.trans_le (ux.2.trans (hy x xt.1).le), _⟩,
+      by_contra' H,
+      exact false.elim (lt_irrefl _ ((Hy _ _ xt.1 H).trans_lt h')) },
+    { refine disjoint_left.2 (λ u ux ux', x't.2.2.1 _),
+      refine h'z x xt ⟨ux.1.trans_le (ux'.2.trans (hy x' x't.1).le), _⟩,
+      by_contra' H,
+      exact false.elim (lt_irrefl _ ((Hy _ _ x't.1 H).trans_lt h')) } },
+  refine this.countable_of_is_open (λ x hx, _) (λ x hx, ⟨x, hz x hx, le_rfl⟩),
+  suffices H : Ioc (z x) x = Ioo (z x) (y x),
+  { rw H, exact is_open_Ioo },
+  exact subset.antisymm (Ioc_subset_Ioo_right (hy x hx.1)) (λ u hu, ⟨hu.1, Hy _ _ hx.1 hu.2⟩),
+end
+
+/-- The set of points which are isolated on the left is countable when the space is
+second-countable. -/
+lemma countable_of_isolated_left [second_countable_topology α] :
+  set.countable {x : α | ∃ y, y < x ∧ Ioo y x = ∅} :=
+begin
+  convert @countable_of_isolated_right αᵒᵈ _ _ _ _,
+  have : ∀ (x y : α), Ioo x y = {z | z < y ∧ x < z},
+  { simp_rw [and_comm, Ioo], simp only [eq_self_iff_true, forall_2_true_iff] },
+  simp_rw [this],
+  refl
+end
+
+/-- Consider a disjoint family of intervals `(x, y)` with `x < y` in a second-countable space.
+Then the family is countable.
+This is not a straightforward consequence of second-countability as some of these intervals might be
+empty (but in fact this can happen only for countably many of them). -/
+lemma set.pairwise_disjoint.countable_of_Ioo [second_countable_topology α]
+  {y : α → α} {s : set α} (h : pairwise_disjoint s (λ x, Ioo x (y x))) (h' : ∀ x ∈ s, x < y x) :
+  countable s :=
+begin
+  let t := {x | x ∈ s ∧ (Ioo x (y x)).nonempty},
+  have t_count : countable t,
+  { have : t ⊆ s := λ x hx, hx.1,
+    exact (h.subset this).countable_of_is_open (λ x hx, is_open_Ioo) (λ x hx, hx.2) },
+  have : s ⊆ t ∪ {x : α | ∃ x', x < x' ∧ Ioo x x' = ∅},
+  { assume x hx,
+    by_cases h'x : (Ioo x (y x)).nonempty,
+    { exact or.inl ⟨hx, h'x⟩ },
+    { exact or.inr ⟨y x, h' x hx, not_nonempty_iff_eq_empty.1 h'x⟩ } },
+  exact countable.mono this (t_count.union countable_of_isolated_right),
+end
+
 section pi
 
 /-!

src/topology/separation.lean

@@ -318,6 +318,14 @@ begin
   exact is_closed_bUnion hs (λ i hi, is_closed_singleton)
 end
 
+lemma topological_space.is_topological_basis.exists_mem_of_ne
+  [t1_space α] {b : set (set α)} (hb : is_topological_basis b) {x y : α} (h : x ≠ y) :
+  ∃ a ∈ b, x ∈ a ∧ y ∉ a :=
+begin
+  rcases hb.is_open_iff.1 is_open_ne x h with ⟨a, ab, xa, ha⟩,
+  exact ⟨a, ab, xa, λ h, ha h rfl⟩,
+end
+
 lemma filter.coclosed_compact_le_cofinite [t1_space α] :
   filter.coclosed_compact α ≤ filter.cofinite :=
 λ s hs, compl_compl s ▸ hs.is_compact.compl_mem_coclosed_compact_of_is_closed hs.is_closed