feat(topology/algebra/order): coe : ℚ → 𝕜 has dense range (#14635)

* add `rat.dense_range_cast`, use it in `rat.dense_embedding_coe_real`;
* rename `dense_iff_forall_lt_exists_mem` to `dense_iff_exists_between`;
* add `dense_of_exists_between`, use it in `dense_iff_exists_between`.

src/topology/algebra/order/archimedean.lean

@@ -0,0 +1,22 @@
+/-
+Copyright (c) 2022 Yury G. Kudryashov. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Yury G. Kudryashov
+-/
+import topology.algebra.order.basic
+import algebra.order.archimedean
+
+/-!
+# Rational numbers are dense in a linear ordered archimedean field
+
+In this file we prove that coercion from `ℚ` to a linear ordered archimedean field has dense range.
+This lemma is in a separate file because `topology.algebra.order.basic` does not import
+`algebra.order.archimedean`.
+-/
+
+variables {𝕜 : Type*} [linear_ordered_field 𝕜] [topological_space 𝕜] [order_topology 𝕜]
+  [archimedean 𝕜]
+
+/-- Rational numbers are dense in a linear ordered archimedean field. -/
+lemma rat.dense_range_cast : dense_range (coe : ℚ → 𝕜) :=
+dense_of_exists_between $ λ a b h, set.exists_range_iff.2 $ exists_rat_btwn h

src/topology/algebra/order/basic.lean

@@ -1074,6 +1074,22 @@ instance order_topology.to_order_closed_topology : order_closed_topology α :=
       let ⟨u, v, hu, hv, ha₁, ha₂, h⟩ := order_separated h in
       ⟨v, u, hv, hu, ha₂, ha₁, assume ⟨b₁, b₂⟩ ⟨h₁, h₂⟩, not_le_of_gt $ h b₂ h₂ b₁ h₁⟩ }
 
+lemma dense_of_exists_between [nontrivial α] {s : set α}
+  (h : ∀ ⦃a b⦄, a < b → ∃ c ∈ s, a < c ∧ c < b) : dense s :=
+begin
+  apply dense_iff_inter_open.2 (λ U U_open U_nonempty, _),
+  obtain ⟨a, b, hab, H⟩ : ∃ (a b : α), a < b ∧ Ioo a b ⊆ U := U_open.exists_Ioo_subset U_nonempty,
+  obtain ⟨x, xs, hx⟩ : ∃ (x : α) (H : x ∈ s), a < x ∧ x < b := h hab,
+  exact ⟨x, ⟨H hx, xs⟩⟩
+end
+
+/-- 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. -/
+lemma dense_iff_exists_between [densely_ordered α] [nontrivial α] {s : set α} :
+  dense s ↔ ∀ a b, a < b → ∃ c ∈ s, a < c ∧ c < b :=
+⟨λ h a b hab, h.exists_between hab, dense_of_exists_between⟩
+
 lemma order_topology.t2_space : t2_space α := by apply_instance
 
 @[priority 100] -- see Note [lower instance priority]
@@ -2650,21 +2666,6 @@ by rw [← comap_coe_Ioi_nhds_within_Ioi, tendsto_comap_iff]
   tendsto f l at_top ↔ tendsto (λ x, (f x : α)) l (𝓝[<] a) :=
 by rw [← comap_coe_Iio_nhds_within_Iio, tendsto_comap_iff]
 
-lemma dense_iff_forall_lt_exists_mem [nontrivial α] {s : set α} :
-  dense s ↔ ∀ a b, a < b → ∃ c ∈ s, a < c ∧ c < b :=
-begin
-  split,
-  { assume h a b hab,
-    obtain ⟨c, ⟨hc, cs⟩⟩ : ((Ioo a b) ∩ s).nonempty :=
-      dense_iff_inter_open.1 h (Ioo a b) is_open_Ioo (nonempty_Ioo.2 hab),
-    exact ⟨c, cs, hc⟩ },
-  { assume h,
-    apply dense_iff_inter_open.2 (λ U U_open U_nonempty, _),
-    obtain ⟨a, b, hab, H⟩ : ∃ (a b : α), a < b ∧ Ioo a b ⊆ U := U_open.exists_Ioo_subset U_nonempty,
-    obtain ⟨x, xs, hx⟩ : ∃ (x : α) (H : x ∈ s), a < x ∧ x < b := h a b hab,
-    exact ⟨x, ⟨H hx, xs⟩⟩ }
-end
-
 instance (x : α) [nontrivial α] : ne_bot (𝓝[≠] x) :=
 begin
   apply forall_mem_nonempty_iff_ne_bot.1 (λ s hs, _),

src/topology/basic.lean

@@ -1531,13 +1531,9 @@ lemma dense_range.exists_mem_open (hf : dense_range f) {s : set β} (ho : is_ope
 exists_range_iff.1 $ hf.exists_mem_open ho hs
 
 lemma dense_range.mem_nhds {f : κ → β} (h : dense_range f) {b : β} {U : set β}
-  (U_in : U ∈ nhds b) : ∃ a, f a ∈ U :=
-begin
-  rcases (mem_closure_iff_nhds.mp
-    ((dense_range_iff_closure_range.mp h).symm ▸ mem_univ b : b ∈ closure (range f)) U U_in)
-    with ⟨_, h, a, rfl⟩,
-  exact ⟨a, h⟩
-end
+  (U_in : U ∈ 𝓝 b) : ∃ a, f a ∈ U :=
+let ⟨a, ha⟩ := h.exists_mem_open is_open_interior ⟨b, mem_interior_iff_mem_nhds.2 U_in⟩
+in ⟨a, interior_subset ha⟩
 
 end dense_range
 

src/topology/instances/rat.lean

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Johannes Hölzl, Mario Carneiro
 -/
 import topology.metric_space.basic
+import topology.algebra.order.archimedean
 import topology.instances.int
 import topology.instances.nat
 import topology.instances.real
@@ -31,11 +32,7 @@ theorem uniform_embedding_coe_real : uniform_embedding (coe : ℚ → ℝ) :=
 uniform_embedding_comap rat.cast_injective
 
 theorem dense_embedding_coe_real : dense_embedding (coe : ℚ → ℝ) :=
-uniform_embedding_coe_real.dense_embedding $
-λ x, mem_closure_iff_nhds.2 $ λ t ht,
-let ⟨ε,ε0, hε⟩ := metric.mem_nhds_iff.1 ht in
-let ⟨q, h⟩ := exists_rat_near x ε0 in
-⟨_, hε (mem_ball'.2 h), q, rfl⟩
+uniform_embedding_coe_real.dense_embedding rat.dense_range_cast
 
 theorem embedding_coe_real : embedding (coe : ℚ → ℝ) := dense_embedding_coe_real.to_embedding