instFinite

Mathlib.Combinatorics.SimpleGraph.Maps

URI: https://scilib.ai/kg/mathlib#SimpleGraph.Hom.instFinite

English

If the vertex sets V and W are finite, then the set of graph homomorphisms G →g H is finite.

Русский

Если множества вершин V и W конечны, то множество граф-гомоморфизмов G →g H конечное.

LaTeX

$$$ [\\text{Finite } V] [\\text{Finite } W] : \\operatorname{Finite}(G \\to_g H) $$$

Lean4

instance [Finite V] [Finite W] : Finite (G →g H) :=
  DFunLike.finite _

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

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

Разделы

Аффилиация

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