chore(topology/urysohns_lemma): use bundled C(X, ℝ) (#8402)

src/measure_theory/continuous_map_dense.lean

@@ -119,7 +119,7 @@ begin
     abel },
   -- Apply Urysohn's lemma to get a continuous approximation to the characteristic function of
   -- the set `s`
-  obtain ⟨g, hg_cont, hgu, hgF, hg_range⟩ :=
+  obtain ⟨g, hgu, hgF, hg_range⟩ :=
     exists_continuous_zero_one_of_closed u_open.is_closed_compl F_closed this,
   -- Multiply this by `c` to get a continuous approximation to the function `f`; the key point is
   -- that this is pointwise bounded by the indicator of the set `u \ F`
@@ -145,8 +145,7 @@ begin
     rw snorm_indicator_const (u_open.sdiff F_closed).measurable_set hp₀.ne' hp,
     push_cast [← ennreal.coe_rpow_of_nonneg _ hp₀'],
     exact ennreal.mul_left_mono (ennreal.rpow_left_monotone_of_nonneg hp₀' h_μ_sdiff) },
-  have gc_cont : continuous (λ x, g x • c) :=
-    continuous_smul.comp (hg_cont.prod_mk continuous_const),
+  have gc_cont : continuous (λ x, g x • c) := g.continuous.smul continuous_const,
   have gc_mem_ℒp : mem_ℒp (λ x, g x • c) p μ,
   { have : mem_ℒp ((λ x, g x • c) - s.indicator (λ x, c)) p μ :=
     ⟨(gc_cont.ae_measurable μ).sub (measurable_const.indicator hs).ae_measurable,

src/topology/urysohns_lemma.lean

@@ -5,6 +5,7 @@ Authors: Yury G. Kudryashov
 -/
 import analysis.normed_space.add_torsor
 import linear_algebra.affine_space.ordered
+import topology.continuous_function.basic
 
 /-!
 # Urysohn's lemma
@@ -287,10 +288,10 @@ then there exists a continuous function `f : X → ℝ` such that
 -/
 lemma exists_continuous_zero_one_of_closed {s t : set X} (hs : is_closed s) (ht : is_closed t)
   (hd : disjoint s t) :
-  ∃ f : X → ℝ, continuous f ∧ eq_on f 0 s ∧ eq_on f 1 t ∧ ∀ x, f x ∈ Icc (0 : ℝ) 1 :=
+  ∃ f : C(X, ℝ), eq_on f 0 s ∧ eq_on f 1 t ∧ ∀ x, f x ∈ Icc (0 : ℝ) 1 :=
 begin
   -- The actual proof is in the code above. Here we just repack it into the expected format.
   set c : urysohns.CU X := ⟨s, tᶜ, hs, ht.is_open_compl, λ _, disjoint_left.1 hd⟩,
-  exact ⟨c.lim, c.continuous_lim, c.lim_of_mem_C,
+  exact ⟨⟨c.lim, c.continuous_lim⟩, c.lim_of_mem_C,
     λ x hx, c.lim_of_nmem_U _ (λ h, h hx), c.lim_mem_Icc⟩
 end