apply

Mathlib.Topology.LocallyConstant.Basic

URI: https://scilib.ai/kg/mathlib#LocallyConstant.Simps.apply

English

The constant map to 1 is locally constant: IsLocallyConstant 1.

Русский

Константное отображение в единицу локально константно.

LaTeX

$$IsLocallyConstant 1$$

Lean4

/-- See Note [custom simps projections]. -/
def apply (f : LocallyConstant X Y) : X → Y :=
  f

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru