Density of locally constant functions

On a profinite space X, every continuous function to a uniform space is a uniform limit of locally constant functions: LocallyConstant.denseRange_toContinuousMap. This is the density statement used to extend functionals from locally constant test functions to all continuous ones, for instance to extend the coefficients of measures on profinite spaces.

ContinuousMap.intCastLocallyConstant casts integer-valued continuous functions to locally constant functions with values in any type with an integer cast.

theorem LocallyConstant.denseRange_toContinuousMap {X : Type u_1} {V : Type u_2} [TopologicalSpace X] [CompactSpace X] [T2Space X] [TotallyDisconnectedSpace X] [UniformSpace V] : DenseRange fun (f : LocallyConstant X V) => ↑f

On a profinite space, locally constant functions are dense in the continuous functions to a uniform space, for the topology of uniform convergence.

def ContinuousMap.intCastLocallyConstant {X : Type u_1} {R : Type u_2} [TopologicalSpace X] [IntCast R] (f : C(X, ℤ)) : LocallyConstant X R

Cast an integer-valued continuous function to a locally constant function.

@[simp]

theorem ContinuousMap.intCastLocallyConstant_apply {X : Type u_1} {R : Type u_2} [TopologicalSpace X] [IntCast R] (f : C(X, ℤ)) (x : X) : f.intCastLocallyConstant x = ↑(f x)

The locally constant integer cast agrees pointwise with the integer cast.