ofObj_apply

Mathlib.CategoryTheory.ObjectProperty.Basic

URI: https://scilib.ai/kg/mathlib#CategoryTheory.ObjectProperty.ofObj_apply

English

For the indexing family X : ι → C, the value at i is the witness ⟨i⟩.

Русский

Для индексного семейства X : ι → C значение на i равно свидетелю ⟨i⟩.

LaTeX

$$$ ofObj X (X i) = ⟨i⟩ $$$

Lean4

@[simp]
theorem ofObj_apply (i : ι) : ofObj X (X i) :=
  ⟨i⟩

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

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

Разделы

Аффилиация

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