English
If a locally constant map f factors through an injection g: α→β via h: LocallyConstant X β, then there exists a locally constant map from X to α with the same factoring, constructed by desc.
Русский
Если локально константное отображение f факторизуется через инъекцию g: α→β посредством h: LocallyConstant X β, тогда существует локально константное отображение из X в α, получаемое конструированием desc.
LaTeX
$$$ \\text{LocallyConstant.desc } f\th\ cond\ inj : LocallyConstant X α,\\text{ with } \\mathrm{coe} (\\text{desc } f\ h\ cond\ inj) = f $$$
Lean4
/-- If a locally constant function factors through an injection, then it factors through a locally
constant function. -/
def desc {X α β : Type*} [TopologicalSpace X] {g : α → β} (f : X → α) (h : LocallyConstant X β) (cond : g ∘ f = h)
(inj : Function.Injective g) : LocallyConstant X α
where
toFun := f
isLocallyConstant := IsLocallyConstant.desc _ g (cond.symm ▸ h.isLocallyConstant) inj
