feat(topology/separation): removing a finite set from a dense set preserves density (#10405)

Also add the fact that one can find a dense set containing neither top nor bottom in a nontrivial dense linear order.

Author: sgouezel

src/measure_theory/function/ae_measurable_order.lean

@@ -110,18 +110,12 @@ theorem ennreal.ae_measurable_of_exist_almost_disjoint_supersets
     {x | f x < p} ⊆ u ∧ {x | (q : ℝ≥0∞) < f x} ⊆ v ∧ μ (u ∩ v) = 0) :
   ae_measurable f μ :=
 begin
-  let s : set ℝ≥0∞ := {x | ∃ a : ℚ, x = ennreal.of_real a},
-  have s_count : countable s,
-  { have : s = range (λ (a : ℚ), ennreal.of_real a),
-      by { ext x, simp only [eq_comm, mem_range, mem_set_of_eq] },
-    rw this,
-    exact countable_range _ },
-  have s_dense : dense s,
-  { refine dense_iff_forall_lt_exists_mem.2 (λ c d hcd, _),
-    rcases ennreal.lt_iff_exists_rat_btwn.1 hcd with ⟨q, hq⟩,
-    exact ⟨ennreal.of_real q, ⟨q, rfl⟩, hq.2⟩ },
+  obtain ⟨s, s_count, s_dense, s_zero, s_top⟩ : ∃ s : set ℝ≥0∞, countable s ∧ dense s ∧
+    0 ∉ s ∧ ∞ ∉ s := ennreal.exists_countable_dense_no_zero_top,
+  have I : ∀ x ∈ s, x ≠ ∞ := λ x xs hx, s_top (hx ▸ xs),
   apply measure_theory.ae_measurable_of_exist_almost_disjoint_supersets μ s s_count s_dense _,
-  rintros _ ⟨p, rfl⟩ _ ⟨q, rfl⟩ hpq,
-  apply h,
-  simpa [ennreal.of_real] using hpq,
+  rintros p hp q hq hpq,
+  lift p to ℝ≥0 using I p hp,
+  lift q to ℝ≥0 using I q hq,
+  exact h p q (ennreal.coe_lt_coe.1 hpq),
 end

src/topology/algebra/ordered/basic.lean

@@ -2435,6 +2435,44 @@ begin
     exact ⟨x, ⟨H hx, xs⟩⟩ }
 end
 
+instance (x : α) [nontrivial α] : ne_bot (𝓝[{x}ᶜ] x) :=
+begin
+  apply forall_mem_nonempty_iff_ne_bot.1 (λ s hs, _),
+  obtain ⟨u, u_open, xu, us⟩ : ∃ (u : set α), is_open u ∧ x ∈ u ∧ u ∩ {x}ᶜ ⊆ s :=
+    mem_nhds_within.1 hs,
+  obtain ⟨a, b, a_lt_b, hab⟩ : ∃ (a b : α), a < b ∧ Ioo a b ⊆ u := u_open.exists_Ioo_subset ⟨x, xu⟩,
+  obtain ⟨y, hy⟩ : ∃ y, a < y ∧ y < b := exists_between a_lt_b,
+  rcases ne_or_eq x y with xy|rfl,
+  { exact ⟨y, us ⟨hab hy, xy.symm⟩⟩ },
+  obtain ⟨z, hz⟩ : ∃ z, a < z ∧ z < x := exists_between hy.1,
+  exact ⟨z, us ⟨hab ⟨hz.1, hz.2.trans hy.2⟩, hz.2.ne⟩⟩,
+end
+
+/-- Let `s` be a dense set in a nontrivial dense linear order `α`. If `s` is a
+separable space (e.g., if `α` has a second countable topology), then there exists a countable
+dense subset `t ⊆ s` such that `t` does not contain bottom/top elements of `α`. -/
+lemma dense.exists_countable_dense_subset_no_bot_top [nontrivial α]
+  {s : set α} [separable_space s] (hs : dense s) :
+  ∃ t ⊆ s, countable t ∧ dense t ∧ (∀ x, is_bot x → x ∉ t) ∧ (∀ x, is_top x → x ∉ t) :=
+begin
+  rcases hs.exists_countable_dense_subset with ⟨t, hts, htc, htd⟩,
+  refine ⟨t \ ({x | is_bot x} ∪ {x | is_top x}), _, _, _, _, _⟩,
+  { exact (diff_subset _ _).trans hts },
+  { exact htc.mono (diff_subset _ _) },
+  { exact htd.diff_finite ((subsingleton_is_bot α).finite.union (subsingleton_is_top α).finite) },
+  { assume x hx, simp [hx] },
+  { assume x hx, simp [hx] }
+end
+
+variable (α)
+/-- If `α` is a nontrivial separable dense linear order, then there exists a
+countable dense set `s : set α` that contains neither top nor bottom elements of `α`.
+For a dense set containing both bot and top elements, see
+`exists_countable_dense_bot_top`. -/
+lemma exists_countable_dense_no_bot_top [separable_space α] [nontrivial α] :
+  ∃ s : set α, countable s ∧ dense s ∧ (∀ x, is_bot x → x ∉ s) ∧ (∀ x, is_top x → x ∉ s) :=
+by simpa using dense_univ.exists_countable_dense_subset_no_bot_top
+
 end densely_ordered
 
 section complete_linear_order

src/topology/bases.lean

@@ -414,7 +414,8 @@ in ⟨coe '' t, image_subset_iff.2 $ λ x _, mem_preimage.2 $ subtype.coe_prop _
 /-- Let `s` be a dense set in a topological space `α` with partial order structure. If `s` is a
 separable space (e.g., if `α` has a second countable topology), then there exists a countable
 dense subset `t ⊆ s` such that `t` contains bottom/top element of `α` when they exist and belong
-to `s`. -/
+to `s`. For a dense subset containing neither bot nor top elements, see
+`dense.exists_countable_dense_subset_no_bot_top`. -/
 lemma dense.exists_countable_dense_subset_bot_top {α : Type*} [topological_space α]
   [partial_order α] {s : set α} [separable_space s] (hs : dense s) :
   ∃ t ⊆ s, countable t ∧ dense t ∧ (∀ x, is_bot x → x ∈ s → x ∈ t) ∧
@@ -435,7 +436,8 @@ instance separable_space_univ {α : Type*} [topological_space α] [separable_spa
 
 /-- If `α` is a separable topological space with a partial order, then there exists a countable
 dense set `s : set α` that contains those of both bottom and top elements of `α` that actually
-exist. -/
+exist. For a dense set containing neither bot nor top elements, see
+`exists_countable_dense_no_bot_top`. -/
 lemma exists_countable_dense_bot_top (α : Type*) [topological_space α] [separable_space α]
   [partial_order α] :
   ∃ s : set α, countable s ∧ dense s ∧ (∀ x, is_bot x → x ∈ s) ∧ (∀ x, is_top x → x ∈ s) :=

src/topology/basic.lean

@@ -936,7 +936,7 @@ space. -/
   closure {x}ᶜ = (univ : set α) :=
 (dense_compl_singleton x).closure_eq
 
-/-- If `x` is not an isolated point of a topological space, then the interior of `{x}ᶜ` is empty. -/
+/-- If `x` is not an isolated point of a topological space, then the interior of `{x}` is empty. -/
 @[simp] lemma interior_singleton (x : α) [ne_bot (𝓝[{x}ᶜ] x)] :
   interior {x} = (∅ : set α) :=
 interior_eq_empty_iff_dense_compl.2 (dense_compl_singleton x)

src/topology/instances/ennreal.lean

@@ -521,6 +521,14 @@ have Inf ((λb, ↑r - b) '' range b) = ↑r - (⨆i, b i),
     (ennreal.tendsto_coe_sub.comp (tendsto_id' inf_le_left)),
 by rw [eq, ←this]; simp [Inf_image, infi_range, -mem_range]; exact le_rfl
 
+lemma exists_countable_dense_no_zero_top :
+  ∃ (s : set ℝ≥0∞), countable s ∧ dense s ∧ 0 ∉ s ∧ ∞ ∉ s :=
+begin
+  obtain ⟨s, s_count, s_dense, hs⟩ : ∃ s : set ℝ≥0∞, countable s ∧ dense s ∧
+    (∀ x, is_bot x → x ∉ s) ∧ (∀ x, is_top x → x ∉ s) := exists_countable_dense_no_bot_top ℝ≥0∞,
+  exact ⟨s, s_count, s_dense, λ h, hs.1 0 (by simp) h, λ h, hs.2 ∞ (by simp) h⟩,
+end
+
 end topological_space
 
 section tsum

src/topology/separation.lean

@@ -304,7 +304,7 @@ begin
   apply is_closed_map.of_nonempty, intros s hs h2s, simp_rw [h2s.image_const, is_closed_singleton]
 end
 
-lemma finite.is_closed {α} [topological_space α] [t1_space α] {s : set α} (hs : set.finite s) :
+lemma finite.is_closed [t1_space α] {s : set α} (hs : set.finite s) :
   is_closed s :=
 begin
   rw ← bUnion_of_singleton s,
@@ -321,6 +321,33 @@ begin
   exact ⟨i, hi, λ h, hsub h rfl⟩
 end
 
+/-- Removing a non-isolated point from a dense set, one still obtains a dense set. -/
+lemma dense.diff_singleton [t1_space α] {s : set α} (hs : dense s) (x : α) [ne_bot (𝓝[{x}ᶜ] x)] :
+  dense (s \ {x}) :=
+hs.inter_of_open_right (dense_compl_singleton x) is_open_compl_singleton
+
+/-- Removing a finset from a dense set in a space without isolated points, one still
+obtains a dense set. -/
+lemma dense.diff_finset [t1_space α] [∀ (x : α), ne_bot (𝓝[{x}ᶜ] x)]
+  {s : set α} (hs : dense s) (t : finset α) :
+  dense (s \ t) :=
+begin
+  induction t using finset.induction_on with x s hxs ih hd,
+  { simpa using hs },
+  { rw [finset.coe_insert, ← union_singleton, ← diff_diff],
+    exact ih.diff_singleton _, }
+end
+
+/-- Removing a finite set from a dense set in a space without isolated points, one still
+obtains a dense set. -/
+lemma dense.diff_finite [t1_space α] [∀ (x : α), ne_bot (𝓝[{x}ᶜ] x)]
+  {s : set α} (hs : dense s) {t : set α} (ht : finite t) :
+  dense (s \ t) :=
+begin
+  convert hs.diff_finset ht.to_finset,
+  exact (finite.coe_to_finset _).symm,
+end
+
 /-- If a function to a `t1_space` tends to some limit `b` at some point `a`, then necessarily
 `b = f a`. -/
 lemma eq_of_tendsto_nhds [topological_space β] [t1_space β] {f : α → β} {a : α} {b : β}