ι_f_succ

Mathlib.CategoryTheory.Preadditive.Injective.Resolution

URI: https://scilib.ai/kg/mathlib#CategoryTheory.InjectiveResolution.ι_f_succ

English

The component ι.f at level n+1 is zero: ι.f(n+1) = 0.

Русский

Компонента ι.f на уровне n+1 равна нулю: ι.f(n+1) = 0.

LaTeX

$$$$I.\\!\\!\\iota.f(n+1) = 0.$$$$

Lean4

@[simp]
theorem ι_f_succ (n : ℕ) : I.ι.f (n + 1) = 0 :=
  (isZero_single_obj_X _ _ _ _ (by simp)).eq_of_src _ _

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

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

Разделы

Аффилиация

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