coe_toTopMap

Mathlib.AlgebraicTopology.TopologicalSimplex

URI: https://scilib.ai/kg/mathlib#SimplexCategory.coe_toTopMap

← MathLib Explorer

English

The evaluation of toTopMap at i is the sum of g over indices j with f(j)=i.

Русский

Значение toTopMap при i равно сумме g по тем j, где f(j)=i.

LaTeX

$$$\\text{toTopMap}(f,g)(i) = \\sum_{j \\in \\mathrm{univ},\\; f(j)=i} g(j)$$$

Lean4

@[simp]
theorem coe_toTopMap {x y : SimplexCategory} (f : x ⟶ y) (g : x.toTopObj) (i : ToType y) :
    toTopMap f g i = ∑ j ∈ Finset.univ.filter (f · = i), g j :=
  rfl

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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