obj_eq

Mathlib.CategoryTheory.SmallObject.Iteration.ExtendToSucc

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

English

If i lies in Set.Iic j, then the extended object equals F.obj i.

Русский

Если i ∈ Set.Iic j, то расширенный объект равен F.obj i.

LaTeX

$$$\\text{obj}\\; F\\; X\\; ⟨i, i.2\\trans (Order.le_succ j)\\rangle = F.obj\\langle i.1, i.2\\rangle$ при $i.2$ и др.$$

Lean4

theorem obj_eq (i : Set.Iic j) : obj F X ⟨i, i.2.trans (Order.le_succ j)⟩ = F.obj i :=
  dif_pos i.2

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

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

Разделы

Аффилиация

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