range_δ

Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex

URI: https://scilib.ai/kg/mathlib#SSet.stdSimplex.range_δ

← MathLib Explorer

English

The range of the cosimplicial δ at i equals the complement face of i.

Русский

Образ δ на i равен грани-Complement i.

LaTeX

$$range_δ {n} (i) : Subpresheaf.range (stdSimplex.δ i) = face.{u} { i }ᶜ$$

Lean4

@[simp]
theorem range_δ {n : ℕ} (i : Fin (n + 2)) : Subpresheaf.range (stdSimplex.δ i) = face.{u} { i }ᶜ :=
  by
  rw [Subcomplex.range_eq_ofSimplex]
  exact ofSimplex_yonedaEquiv_δ i

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

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

Разделы

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

Аффилиация

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