∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {Z : Type u_6} (R : Type u_7)
  [inst_2 : Semiring R] [inst_3 : AddCommMonoid Z] [inst_4 : Module R Z] (f : C(X, Y)) (g : LocallyConstant Y Z)
  (a : X), ((LocallyConstant.comapₗ R f) g) a = g (f a)