llp_eq_of_wfs

Mathlib.CategoryTheory.MorphismProperty.WeakFactorizationSystem

URI: https://scilib.ai/kg/mathlib#CategoryTheory.MorphismProperty.llp_eq_of_wfs

English

Similarly, W2.llp equals W1 in a Weak Factorization System.

Русский

Аналогично, W2.llp равно W1 в слабой факторизационной системе.

LaTeX

$$$ W_2.\mathrm{llp} = W_1 $$$

Lean4

theorem llp_eq_of_wfs : W₂.llp = W₁ :=
  IsWeakFactorizationSystem.llp

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

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

Разделы

Аффилиация

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