range_isFinite

Mathlib.CategoryTheory.Subpresheaf.Finite

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Subpresheaf.range_isFinite

← MathLib Explorer

English

If F is finite-presheaf, then for any morphism f, the range of f is finite.

Русский

Если F конечнопредпрешеф, то образ f конечен.

LaTeX

$$[PresheafIsFinite F] {F' : C^{op} ⥤ Type w} (f : F ⟶ F') : (Subpresheaf.range f).IsFinite$$

Lean4

theorem range_isFinite [PresheafIsFinite F] {F' : Cᵒᵖ ⥤ Type w} (f : F ⟶ F') : (Subpresheaf.range f).IsFinite :=
  ((presheafIsGeneratedBy_of_isFinite F).range f).isFinite

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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