fac

Mathlib.CategoryTheory.SmallObject.Iteration.Basic

URI: https://scilib.ai/kg/mathlib#CategoryTheory.SmallObject.SuccStruct.prop.fac

English

For any hf: Φ.prop f, the original morphism f equals Φ.toSucc X followed by the necessary equality, i.e., f = Φ.toSucc X ≫ eqToHom hf.succ_eq.

Русский

Для hf: Φ.prop f выполняется равенство: f = Φ.toSucc X ∘ eqToHom hf.succ_eq.

LaTeX

$$fac hf : f = Φ.toSucc X ≫ eqToHom hf.succ_eq$$

Lean4

@[reassoc]
theorem fac {X Y : C} {f : X ⟶ Y} (hf : Φ.prop f) : f = Φ.toSucc X ≫ eqToHom hf.succ_eq :=
  by
  cases hf
  simp

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

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

Разделы

Аффилиация

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