fromLoop_apply

Mathlib.Topology.Homotopy.HomotopyGroup

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

English

The image under fromLoop of p evaluated at t equals p evaluated at t i and split at i.

Русский

Изображение через fromLoop для p, применённого к t, равно p(t i)(Cube.splitAt i t).snd.

LaTeX

$$fromLoop_apply(i,p,t) = p(t i)(Cube.splitAt i t).snd$$

Lean4

theorem fromLoop_apply (i : N) {p : Ω (Ω^ { j // j ≠ i } X x) const} {t : I^N} :
    fromLoop i p t = p (t i) (Cube.splitAt i t).snd :=
  rfl

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

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

Разделы

Аффилиация

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