single₀_obj_zero — Mathlib

English

In the degree-zero part of the single₀ construction, the X-component is exactly the original object: the zero-th level recovers A.

Русский

В нулевом уровне конструкции single₀ компонент X совпадает с исходным объектом: нулевой уровень возвращает A.

LaTeX

$$$((\\mathrm{single}_0 V).\\mathrm{obj} A)_{0} = A$$$

Lean4

@[simp]
theorem single₀_obj_zero (A : V) : ((single₀ V).obj A).X 0 = A :=
  rfl

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