toPreimages_finite

Mathlib.CategoryTheory.CofilteredSystem

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

English

If every F.obj j is finite, then every object (toPreimages s).obj j of the preimage subfunctor is finite.

Русский

Если все объекты F.obj j конечны, то каждый объект (toPreimages s).obj j конечен.

LaTeX

$$$\forall j,\ Finite\ (F.obj j)\Rightarrow\ Finite\ ((F.toPreimages s).obj j).$$$

Lean4

instance toPreimages_finite [∀ j, Finite (F.obj j)] : ∀ j, Finite ((F.toPreimages s).obj j) := fun _ => Subtype.finite

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

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

Разделы

Аффилиация

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