KanComplex

Mathlib.AlgebraicTopology.SimplicialSet.KanComplex

URI: https://scilib.ai/kg/mathlib#SSet.KanComplex

Lean4

/-- A simplicial set `S` is a Kan complex if it is fibrant, which means that
the projection `S ⟶ ⊤_ _` has the right lifting property with respect to horn inclusions. -/
abbrev KanComplex (S : SSet.{u}) : Prop :=
  HomotopicalAlgebra.IsFibrant S

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

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

Разделы

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

Аффилиация

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