obj — Mathlib

English

On objects, the extension coincides with F.obj below j, and sends the immediate successor of j to the fixed object X.

Русский

На объектах продолжение совпадает с F.obj для элементов i ≤ j и отправляет соседа j в заданный объект X.

LaTeX

$$$\\mathrm{obj}\\, F\\, X\\; ⟨i, \\_\\rangle = \\begin{cases} F.obj\\langle i, \\text{proof}\\rangle, & i \\le j \\\\ X, & \\text{otherwise} \\end{cases} $$$

Lean4

/-- `extendToSucc`, on objects: it coincides with `F.obj` for `i ≤ j`, and
it sends `Order.succ j` to the given object `X`. -/
def obj (i : Set.Iic (Order.succ j)) : C :=
  if hij : i.1 ≤ j then F.obj ⟨i.1, hij⟩ else X

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