QInfty_f

Mathlib.AlgebraicTopology.DoldKan.PInfty

URI: https://scilib.ai/kg/mathlib#AlgebraicTopology.DoldKan.QInfty_f

English

The naturality of QInfty with respect to morphisms f mirrors the corresponding naturality of PInfty.

Русский

Естественность QInfty по отношению к морфизмам f повторяет естественность PInfty.

LaTeX

$$$QInfty.f_n = (Q_n).f_n$$$

Lean4

theorem QInfty_f (n : ℕ) : (QInfty.f n : X _⦋n⦌ ⟶ X _⦋n⦌) = (Q n).f n :=
  rfl

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

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

Разделы

Аффилиация

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