rev_map_δ

Mathlib.AlgebraicTopology.SimplexCategory.Rev

URI: https://scilib.ai/kg/mathlib#SimplexCategory.rev_map_δ

← MathLib Explorer

English

Under reversal, δ commutes with rev: rev.map (δ i) = δ i.rev.

Русский

При обращении карточки δ коммутирует с rev: rev.map(δ i) = δ i.rev.

LaTeX

$$$\\mathrm{rev.map}(\\delta_i) = \\delta_{i^{\\mathrm{rev}}}$$$

Lean4

@[simp]
theorem rev_map_δ {n : ℕ} (i : Fin (n + 2)) : rev.map (δ i) = δ i.rev :=
  by
  ext j : 3
  rw [rev_map_apply]
  dsimp [δ]
  rw [Fin.succAbove_rev_right, Fin.rev_rev]

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

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

Разделы

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

Аффилиация

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