coneπApp_eq_id

Mathlib.CategoryTheory.Limits.Constructions.EventuallyConstant

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Functor.IsEventuallyConstantTo.coneπApp_eq_id

English

The cone map at i0 is the identity when restricted to i0.

Русский

Конусная карта на i0 равна тождественной на F.obj i0.

LaTeX

$$$h.coneπApp i_0 = \mathrm{id}_{F.obj i_0}$$$

Lean4

@[simp]
theorem coneπApp_eq_id : h.coneπApp i₀ = 𝟙 _ := by rw [h.coneπApp_eq i₀ i₀ (𝟙 _) (𝟙 _), h.isoMap_inv_hom_id]

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

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

Разделы

Аффилиация

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