precomp

Mathlib.CategoryTheory.Limits.Constructions.EventuallyConstant

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Functor.IsEventuallyConstantTo.precomp

English

For any j and morphism f: j → i0, F.IsEventuallyConstantTo j holds.

Русский

Для любого j и морфизма f: j → i0 верно, что F константен на j.

LaTeX

$$$\forall j \forall f: j \to i_0,\; F.IsEventuallyConstantTo\, j$$$

Lean4

theorem precomp {j : J} (f : j ⟶ i₀) : F.IsEventuallyConstantTo j := fun _ φ ↦ h.isIso_map φ f

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

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

Разделы

Аффилиация

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