{X : Type u_5} →
  {α : Type u_6} →
    {β : Type u_7} →
      [inst : TopologicalSpace X] →
        {g : α → β} → (f : X → α) → (h : LocallyConstant X β) → g ∘ f = ⇑h → Function.Injective g → LocallyConstant X α