exists_very_good

Mathlib.AlgebraicTopology.ModelCategory.PathObject

URI: https://scilib.ai/kg/mathlib#HomotopicalAlgebra.PathObject.exists_very_good

English

There exists a path object P for A that is very good.

Русский

Существуют путь-объект P для A, который очень хорош.

LaTeX

$$$\exists P : PathObject(A), IsVeryGood(P)$$$

Lean4

theorem exists_very_good : ∃ (P : PathObject A), P.IsVeryGood :=
  ⟨ofFactorizationData (MorphismProperty.factorizationData _ _ _), inferInstance⟩

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

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

Разделы

Аффилиация

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