toLoop_apply

Mathlib.Topology.Homotopy.HomotopyGroup

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

English

The value of toLoop i at p and t is p evaluated at the inserted point.

Русский

Значение toLoop i(p) при t равно p, применённому к точке, вставленной в i.

LaTeX

$$toLoop_apply(i,p,t,tn) = p(Cube.insertAt i ⟨t,tn⟩)$$

Lean4

theorem toLoop_apply (i : N) {p : Ω^ N X x} {t} {tn} : toLoop i p t tn = p (Cube.insertAt i ⟨t, tn⟩) :=
  rfl

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

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

Разделы

Аффилиация

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