extendToSucc_obj_eq

Mathlib.CategoryTheory.SmallObject.Iteration.ExtendToSucc

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

← MathLib Explorer

English

As before, the object value at i with i ≤ j matches F.obj i.

Русский

Опять же, значение объекта в i при i ≤ j равно F.obj i.

LaTeX

$$$ (extendToSucc hj F τ).obj ⟨i, hi.trans (Order.le_succ j)⟩ = F.obj ⟨i, hi⟩ $$$

Lean4

theorem extendToSucc_obj_eq (i : J) (hi : i ≤ j) :
    (extendToSucc hj F τ).obj ⟨i, hi.trans (Order.le_succ j)⟩ = F.obj ⟨i, hi⟩ :=
  extendToSucc.obj_eq F X ⟨i, hi⟩

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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