const — Mathlib

English

There exists the constant locally constant map on X with value y ∈ Y; it sends every point of X to y.

Русский

Существует константная локально константная функция на X, принимающая значение y ∈ Y; она отправляет каждую точку X в y.

LaTeX

$$$\\mathrm{const}(X,y): \\mathrm{LocallyConstant}(X,Y)\\;\\text{defined by } x \\mapsto y$$$

Lean4

/-- The constant locally constant function on `X` with value `y : Y`. -/
def const (X : Type*) {Y : Type*} [TopologicalSpace X] (y : Y) : LocallyConstant X Y :=
  ⟨Function.const X y, IsLocallyConstant.const _⟩

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