lift — Mathlib

English

The lift of a locally constant function f along its discrete quotient is itself a locally constant function on the quotient space.

Русский

Подъем локально константной функции вдоль дискретного факторинга образует локально константную функцию на факторпространстве.

LaTeX

$$$\\mathrm{lift}: \\mathrm{LocallyConstant}\, X\\alpha \\to \\mathrm{LocallyConstant}\, (X/\\sim_f)\\alpha$ is locally constant on the quotient.$$

Lean4

/-- The (locally constant) function from the discrete quotient associated to a locally constant
function. -/
def lift : LocallyConstant f.discreteQuotient α :=
  ⟨fun a => Quotient.liftOn' a f fun _ _ => id, fun _ => isOpen_discrete _⟩

Похожие утверждения