P_σ

Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.EpiMono

URI: https://scilib.ai/kg/mathlib#SimplexCategoryGenRel.P_σ

Lean4

/-- Auxiliary predicate to express that a morphism is purely a composition of `σ i`s. -/
abbrev P_σ :=
  degeneracies.multiplicativeClosure

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

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

Разделы

Аффилиация

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