instFinite

Mathlib.Combinatorics.SimpleGraph.Subgraph

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

English

If V is finite, then G.Subgraph is finite.

Русский

Если множество вершин V конечно, то подграф G.Subgraph конечно.

LaTeX

$$$ Finite V \Rightarrow Finite G.Subgraph $$$

Lean4

instance [Finite V] : Finite G.Subgraph := by classical cases nonempty_fintype V; infer_instance

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

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

Разделы

Аффилиация

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