metric space stuff

Stream: maths

[Ashvni Narayanan]

I am trying to prove that the space of locally constant functions are dense in the space of continuous functions. Things are rather open ended, in the sense that I am trying to work with the minimum amount of stuff needed. I don't understand why the last line gives me an error :

import measure_theory.integration
import algebra.group.hom
import ring_theory.int.basic
import data.padics.padic_integers
import set_theory.zfc
import topology.category.Profinite
import topology.locally_constant.algebra
import topology.algebra.continuous_functions
import topology.metric_space.basic

variables (X : Profinite)
open_locale big_operators

instance semi {R : Type*} [semiring R] : semimodule R (locally_constant X R) := sorry

variables {R : Type*} [ring R] {Γ₀   : Type*}  [linear_ordered_comm_group_with_zero Γ₀] (v : valuation R Γ₀)

instance uniform [topological_space R] : uniform_space C(X, R) := sorry

instance completeness [topological_space R] : complete_space C(X, R) := sorry

--topo ring assumption not really needed
def inclusion [topological_space R] [topological_ring R] : locally_constant X R → C(X,R) := sorry

lemma sub [topological_space R] [topological_ring R] : function.injective (@inclusion X R _ _ _) := sorry

instance topo_space :  topological_space (locally_constant ↥X R) := sorry

instance met [topological_space R] : metric_space C(X,R) := sorry

lemma dense_C [topological_space R] [topological_ring R] :
  @dense (C(X,R)) _ (set.range (inclusion X)) :=
begin
  rintros f,
  rw mem_closure_iff_cluster_pt,
  sorry,
end

Any help is appreciated, thank you!

[Ashvni Narayanan]

I figured it out, the topology did not match the one coming from the metric space, which was causing issues. Fixed now!