English
There is a natural lift of a locally constant function f along its discrete quotient to a locally constant map on the quotient, i.e., a function on X/∼ taking value f(x) on the class of x.
Русский
Существует естественный подъем локально константной функции f по её дискретному фактору на отображение на факторпространстве X/∼, т.е. функция на классе, принимающая значение f(x) на класс x.
LaTeX
$$$\\text{lift}: \\mathrm{LocallyConstant}\\, X \\alpha \\to \\mathrm{LocallyConstant}(X/\\sim_f)\\alpha$ такая, что $(\\mathrm{lift}\ f)\\, (\\mathrm{proj}\ x) = f(x)$$$
Lean4
/-- Any locally constant function induces a discrete quotient. -/
def discreteQuotient : DiscreteQuotient X where
toSetoid := .comap f ⊥
isOpen_setOf_rel _ := f.isLocallyConstant _
