instNonemptyOfIsFibrant

Mathlib.AlgebraicTopology.ModelCategory.BrownLemma

URI: https://scilib.ai/kg/mathlib#HomotopicalAlgebra.FibrantBrownFactorization.instNonemptyOfIsFibrant

English

If X and Y are IsFibrant, then there exists a FibrantBrownFactorization f.

Русский

Если X и Y удовлетворяют условию IsFibrant, то существует FibrantBrownFactorization f.

LaTeX

$$$[\IsFibrant X] [\IsFibrant Y] \Rightarrow \text{Nonempty } (\text{FibrantBrownFactorization } f)$$$

Lean4

instance [IsFibrant X] [IsFibrant Y] : Nonempty (FibrantBrownFactorization f) :=
  ⟨.mk' f (MorphismProperty.factorizationData _ _ _)⟩

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

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

Разделы

Аффилиация

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