const_apply

Mathlib.Topology.Homotopy.HomotopyGroup

URI: https://scilib.ai/kg/mathlib#GenLoop.const_apply

English

The evaluation of the constant generalized loop at any input t yields the base point x.

Русский

Значение константного обобщённого цикла в любой точке равно x.

LaTeX

$$$\\text{const\_apply}: (\\text{GenLoop.const})\\;t = x$$$

Lean4

@[simp]
theorem const_apply {t} : (@const N X _ x) t = x :=
  rfl

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

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

Разделы

Аффилиация

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