image_isFinite

Mathlib.CategoryTheory.Subpresheaf.Finite

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

English

If G is finite, then its image under any morphism f is finite.

Русский

Если G конечен, то образ подмножества G под действием любой морфизмы f конечен.

LaTeX

$$$G.IsFinite \Rightarrow (G.image f).IsFinite$$$

Lean4

theorem image_isFinite [G.IsFinite] {F' : Cᵒᵖ ⥤ Type w} (f : F ⟶ F') : (G.image f).IsFinite :=
  ((isGeneratedBy_of_isFinite G).image f).isFinite

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

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

Разделы

Аффилиация

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